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