#include <SMTSolver.h>
Inheritance diagram for SMTSolver:
The purpose of an SMT solver is to determine if an expression is satisfiable. Although the SMTSolver class was originally designed to be used by SymbolicExpressionSemantics policy (see SymbolicExpressionSemantics::Policy::set_solver()), but it can also be used independently.
Public Types | |
| typedef std::set< uint64_t > | Definitions |
| Free variables that have been defined. | |
Public Member Functions | |
| SMTSolver () | |
| virtual | ~SMTSolver () |
| virtual bool | satisfiable (const InsnSemanticsExpr::TreeNode *expr) |
| Determines if the specified expression is satisfiable. | |
| virtual bool | satisfiable (const std::vector< const InsnSemanticsExpr::TreeNode * > &exprs) |
| Determines if the specified collection of expressions is satisfiable. | |
| void | set_debug (FILE *f) |
| Turns debugging on or off. | |
| FILE * | get_debug () const |
| Obtain current debugging setting. | |
| virtual InsnSemanticsExpr::TreeNode * | get_definition (uint64_t varno) |
| Evidence of satisfiability. | |
| virtual InsnSemanticsExpr::TreeNode * | get_definition (const InsnSemanticsExpr::LeafNode *var) |
| Evidence of satisfiability. | |
Static Public Member Functions | |
| static size_t | get_ncalls () |
| Returns the number of times satisfiable() was called. | |
Protected Member Functions | |
| virtual void | generate_file (std::ostream &, const std::vector< const InsnSemanticsExpr::TreeNode * > &exprs, Definitions *)=0 |
| Generates an input file for for the solver. | |
| virtual std::string | get_command (const std::string &config_name)=0 |
| Given the name of a configuration file, return the command that is needed to run the solver. | |
| virtual void | parse_evidence () |
| Parses evidence of satisfiability. | |
Protected Attributes | |
| std::vector< std::string > | output_text |
| Additional output obtained by satisfiable(). | |
Static Protected Attributes | |
| static size_t | total_calls |
| Tracks the number of times an SMT solver was called. | |
Private Attributes | |
| FILE * | debug |
Classes | |
| struct | Exception |
| typedef std::set<uint64_t> SMTSolver::Definitions |
Free variables that have been defined.
| SMTSolver::SMTSolver | ( | ) | [inline] |
| virtual SMTSolver::~SMTSolver | ( | ) | [inline, virtual] |
| virtual bool SMTSolver::satisfiable | ( | const InsnSemanticsExpr::TreeNode * | expr | ) | [virtual] |
Determines if the specified expression is satisfiable.
Throws Exception if satisfiability cannot be determined.
Reimplemented in YicesSolver.
| virtual bool SMTSolver::satisfiable | ( | const std::vector< const InsnSemanticsExpr::TreeNode * > & | exprs | ) | [virtual] |
Determines if the specified collection of expressions is satisfiable.
Throws Exception if satisfiability cannot be determined.
Reimplemented in YicesSolver.
| virtual InsnSemanticsExpr::TreeNode* SMTSolver::get_definition | ( | uint64_t | varno | ) | [inline, virtual] |
Evidence of satisfiability.
If an expression is satisfiable, this function will return information about which values should be bound to variables to make the expression satisfiable. Not all SMT solvers can return this information.
Reimplemented in YicesSolver.
| virtual InsnSemanticsExpr::TreeNode* SMTSolver::get_definition | ( | const InsnSemanticsExpr::LeafNode * | var | ) | [inline, virtual] |
Evidence of satisfiability.
If an expression is satisfiable, this function will return information about which values should be bound to variables to make the expression satisfiable. Not all SMT solvers can return this information.
Reimplemented in YicesSolver.
| void SMTSolver::set_debug | ( | FILE * | f | ) | [inline] |
Turns debugging on or off.
| FILE* SMTSolver::get_debug | ( | ) | const [inline] |
Obtain current debugging setting.
| static size_t SMTSolver::get_ncalls | ( | ) | [inline, static] |
Returns the number of times satisfiable() was called.
This is a class method that returns the total number of SMT solver calls across all SMT solvers.
| virtual void SMTSolver::generate_file | ( | std::ostream & | , | |
| const std::vector< const InsnSemanticsExpr::TreeNode * > & | exprs, | |||
| Definitions * | ||||
| ) | [protected, pure virtual] |
Generates an input file for for the solver.
Usually the input file will be SMT-LIB format, but subclasses might override this to generate some other kind of input. Throws Excecption if the solver does not support an operation that is necessary to determine the satisfiability.
| virtual std::string SMTSolver::get_command | ( | const std::string & | config_name | ) | [protected, pure virtual] |
Given the name of a configuration file, return the command that is needed to run the solver.
The first line of stdout emitted by the solver should be the word "sat" or "unsat".
Implemented in YicesSolver.
| virtual void SMTSolver::parse_evidence | ( | ) | [inline, protected, virtual] |
Parses evidence of satisfiability.
Some solvers can emit information about what variable bindings satisfy the expression. This information is parsed by this function and added to a mapping of variable to value.
Reimplemented in YicesSolver.
std::vector<std::string> SMTSolver::output_text [protected] |
Additional output obtained by satisfiable().
size_t SMTSolver::total_calls [static, protected] |
Tracks the number of times an SMT solver was called.
Actually, the number of calls to satisfiable()
FILE* SMTSolver::debug [private] |
1.4.7