Gymbo

Namespaces | Functions
smt.h File Reference

Core implementation of gradient-based smt solver. More...

`#include "gd.h"`
`#include "sat.h"`
Include dependency graph for smt.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

## Namespaces
| gymbo

## Functions
void | gymbo::initialize_params (std::unordered_map< int, float > &params, SymState &state, bool ignore_memory)
| Initialize Parameter Values from Memory. More...
void | gymbo::smt_union_solver (bool &is_sat, SymState &state, std::unordered_map< int, float > &params, GDOptimizer &optimizer, int max_num_trials, bool ignore_memory)
| SMT Solver with Unified Loss Function. More...
void | gymbo::smt_dpll_solver (bool &is_sat, SymState &state, std::unordered_map< int, float > &params, GDOptimizer &optimizer, int max_num_trials, bool ignore_memory)
| SMT Solver using DPLL as its backend. More...

## Detailed Description

Core implementation of gradient-based smt solver.

Author
  Hideaki Takahashi