Description
Interface to Satisfiability Modulo Theory (SMT) solvers.
The purpose of an SMT solver is to determine if an expression is satisfiable. Solvers are reference counted objects that are allocated with instance static methods or create virtual constructors and should not be explicitly deleted.
Definition at line 39 of file SmtSolver.h.
#include <Rose/BinaryAnalysis/SmtSolver.h>
Classes | |
| struct | Exception |
| Exceptions for all things SMT related. More... | |
| class | Memoizer |
| Memoizes calls to an SMT solver. More... | |
| struct | ParseError |
| Exception for parse errors when reading SMT solver output. More... | |
| class | SExpr |
| S-Expr parsed from SMT solver text output. More... | |
| struct | Stats |
| SMT solver statistics. More... | |
| class | Transaction |
| RAII guard for solver stack. More... | |
Public Types | |
| enum | LinkMode { LM_NONE = 0x0000, LM_LIBRARY = 0x0001, LM_EXECUTABLE = 0x0002, LM_ANY = 0x0003 } |
| Bit flags to indicate the kind of solver interface. More... | |
| enum | Type { NO_TYPE, BOOLEAN, BIT_VECTOR, MEM_STATE } |
| Type (sort) of expression. More... | |
| enum | Satisfiable { SAT_NO =0, SAT_YES, SAT_UNKNOWN } |
| Satisfiability constants. More... | |
| using | ExprList = std::vector< SymbolicExpression::Ptr > |
| Ordered list of expressions. More... | |
| using | Ptr = SmtSolverPtr |
| Reference counting pointer for SMT solvers. More... | |
| using | Availability = std::map< std::string, bool > |
| Solver availability map. More... | |
| using | StringTypePair = std::pair< std::string, Type > |
| Maps expression nodes to term names. More... | |
| using | TermNames = Sawyer::Container::Map< SymbolicExpression::Ptr, StringTypePair > |
| using | ExprExprMap = Sawyer::Container::Map< SymbolicExpression::Ptr, SymbolicExpression::Ptr > |
| Maps one symbolic expression to another. More... | |
| using | VariableSet = Sawyer::Container::Set< SymbolicExpression::LeafPtr, CompareLeavesByName > |
| Set of variables. More... | |
| using | Definitions = std::set< uint64_t > |
| Free variables that have been defined. More... | |
| using | SExprTypePair = std::pair< SExpr::Ptr, Type > |
| using | Evidence = Sawyer::Container::Map< std::string, SymbolicExpression::Ptr > |
| Evidence of satisfiability. More... | |
Public Member Functions | |
| virtual Ptr | create () const =0 |
| Virtual constructor. More... | |
| LinkMode | linkage () const |
| Property: How ROSE communicates with the solver. More... | |
| void | requireLinkage (LinkMode) const |
| Assert required linkage. More... | |
| virtual void | timeout (boost::chrono::duration< double > seconds)=0 |
| Set the timeout for the solver. More... | |
| virtual Satisfiable | triviallySatisfiable (const ExprList &exprs) |
| Determines if expressions are trivially satisfiable or unsatisfiable. More... | |
| virtual void | reset () |
| Reset solver state. More... | |
| virtual void | push () |
| Create a backtracking point. More... | |
| virtual void | pop () |
| Pop a backtracking point. More... | |
| virtual size_t | nLevels () const |
| Number of backtracking levels. More... | |
| virtual size_t | nAssertions (size_t backtrackingLevel) |
| Number of assertions at a specific backtracking level. More... | |
| virtual size_t | nAssertions () const |
| Total number of assertions across all backtracking levels. More... | |
| virtual ExprList | assertions () const |
| All assertions. More... | |
| virtual const ExprList & | assertions (size_t level) const |
| Assertions for a particular level. More... | |
| virtual Satisfiable | check () |
| Check satisfiability of current stack. More... | |
| virtual Satisfiable | checkTrivial () |
| Check whether the stack of assertions is trivially satisfiable. More... | |
| virtual std::vector< std::string > | evidenceNames () const |
| Names of items for which satisfiability evidence exists. More... | |
| virtual SymbolicExpression::Ptr | evidenceForName (const std::string &) const |
| Evidence of satisfiability for a variable or memory address. More... | |
| virtual void | clearEvidence () |
| Clears evidence information. More... | |
| virtual SymbolicExpression::Ptr | evidenceForAddress (uint64_t addr) |
| Evidence of satisfiability for a memory address. More... | |
| const Stats & | statistics () const |
| Property: Statistics for this solver. More... | |
| void | resetStatistics () |
| Resets statistics for this solver. More... | |
| virtual void | generateFile (std::ostream &, const ExprList &exprs, Definitions *)=0 |
| Generates an input file for for the solver. More... | |
| virtual void | selfTest () |
| Unit tests. More... | |
| const std::string & | name () const |
| Property: Name of solver for debugging. More... | |
| void | name (const std::string &s) |
| Property: Name of solver for debugging. More... | |
| Memoizer::Ptr | memoizer () const |
| Property: Memoizer. More... | |
| void | memoizer (const Memoizer::Ptr &) |
| Property: Memoizer. More... | |
| virtual Satisfiable | satisfiable (const SymbolicExpression::Ptr &) |
| Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown. More... | |
| virtual Satisfiable | satisfiable (const ExprList &) |
| Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown. More... | |
| bool | errorIfReset () const |
| Property: Throw an exception if the solver is reset. More... | |
| void | errorIfReset (bool b) |
| Property: Throw an exception if the solver is reset. More... | |
| virtual void | insert (const SymbolicExpression::Ptr &) |
| Insert assertions. More... | |
| virtual void | insert (const ExprList &) |
| Insert assertions. More... | |
| Evidence | evidenceByName () const |
| All evidence of satisfiability. More... | |
| ExprExprMap | evidence () const |
| All evidence of satisfiability. More... | |
| virtual SymbolicExpression::Ptr | evidenceForVariable (const SymbolicExpression::Ptr &var) |
| Evidence of satisfiability for a bitvector variable. More... | |
| virtual SymbolicExpression::Ptr | evidenceForVariable (uint64_t varno) |
| Evidence of satisfiability for a bitvector variable. More... | |
| Progress::Ptr | progress () const |
| Progress reporting object. More... | |
| void | progress (const Progress::Ptr &progress) |
| Progress reporting object. More... | |
Static Public Member Functions | |
| static Availability | availability () |
| Availability of all known solvers. More... | |
| static Ptr | instance (const std::string &name) |
| Allocate a new solver by name. More... | |
| static Ptr | bestAvailable () |
| Best available solver. More... | |
| static LinkMode | bestLinkage (unsigned linkages) |
| Given a bit vector of linkages, return the best one. More... | |
| static Stats | classStatistics () |
| Property: Statistics across all solvers. More... | |
| static void | resetClassStatistics () |
| Resets statistics for the class. More... | |
| static void | initDiagnostics () |
| Initialize diagnostic output facilities. More... | |
Static Public Attributes | |
| static Sawyer::Message::Facility | mlog |
| Diagnostic facility. More... | |
Protected Member Functions | |
| SmtSolver (const std::string &name, unsigned linkages) | |
| Construct with name and linkage. More... | |
| virtual Satisfiable | checkExe () |
| Check satisfiability using text files and an executable. More... | |
| virtual Satisfiable | checkLib () |
| Check satisfiability using a library API. More... | |
| virtual std::string | getErrorMessage (int exitStatus) |
| Error message from running a solver executable. More... | |
| virtual void | findVariables (const SymbolicExpression::Ptr &, VariableSet &) |
| Return all variables that need declarations. More... | |
| virtual std::string | getCommand (const std::string &config_name)=0 |
| Given the name of a configuration file, return the command that is needed to run the solver. More... | |
| std::vector< SExpr::Ptr > | parseSExpressions (const std::string &) |
| Parse all SExprs from the specified string. More... | |
| virtual void | parseEvidence () |
| Parses evidence of satisfiability. More... | |
Static Protected Member Functions | |
| static void | printSExpression (std::ostream &, const SExpr::Ptr &) |
| Print an S-Expr for debugging. More... | |
| static ExprList | normalizeVariables (const ExprList &, SymbolicExpression::ExprExprHashMap &index) |
| Normalize expressions by renaming variables. More... | |
| static ExprList | undoNormalization (const ExprList &, const SymbolicExpression::ExprExprHashMap &index) |
| Undo the normalizations that were performed earlier. More... | |
Protected Attributes | |
| LinkMode | linkage_ |
| std::string | outputText_ |
| Additional output obtained by satisfiable(). More... | |
| std::vector< SExpr::Ptr > | parsedOutput_ |
| ExprExprMap | evidence_ |
| TermNames | termNames_ |
| Memoizer::Ptr | memoizer_ |
| Progress::Ptr | progress_ |
| Stats | stats |
Static Protected Attributes | |
| static boost::mutex | classStatsMutex |
| static Stats | classStats |
Member Typedef Documentation
| using Rose::BinaryAnalysis::SmtSolver::ExprList = std::vector<SymbolicExpression::Ptr> |
Ordered list of expressions.
Definition at line 42 of file SmtSolver.h.
Reference counting pointer for SMT solvers.
Definition at line 45 of file SmtSolver.h.
| using Rose::BinaryAnalysis::SmtSolver::Availability = std::map<std::string, bool> |
Solver availability map.
Definition at line 48 of file SmtSolver.h.
| using Rose::BinaryAnalysis::SmtSolver::StringTypePair = std::pair<std::string, Type> |
Maps expression nodes to term names.
This map is populated for common subexpressions.
Definition at line 66 of file SmtSolver.h.
| using Rose::BinaryAnalysis::SmtSolver::ExprExprMap = Sawyer::Container::Map<SymbolicExpression::Ptr, SymbolicExpression::Ptr> |
Maps one symbolic expression to another.
Definition at line 70 of file SmtSolver.h.
| using Rose::BinaryAnalysis::SmtSolver::VariableSet = Sawyer::Container::Set<SymbolicExpression::LeafPtr, CompareLeavesByName> |
Set of variables.
Definition at line 178 of file SmtSolver.h.
| using Rose::BinaryAnalysis::SmtSolver::Definitions = std::set<uint64_t> |
Free variables that have been defined.
Definition at line 180 of file SmtSolver.h.
| using Rose::BinaryAnalysis::SmtSolver::Evidence = Sawyer::Container::Map<std::string , SymbolicExpression::Ptr > |
Evidence of satisfiability.
Definition at line 566 of file SmtSolver.h.
Member Enumeration Documentation
Bit flags to indicate the kind of solver interface.
| Enumerator | |
|---|---|
| LM_NONE |
No available linkage. |
| LM_LIBRARY |
A runtime library is available. |
| LM_EXECUTABLE |
An executable is available. |
| LM_ANY |
Any available mode. |
Definition at line 51 of file SmtSolver.h.
Type (sort) of expression.
ROSE uses bit constants "#b1" and "#b0" (in SMT-LIB syntax) to represent Boolean true and false, but most solvers distinguish between bit vector and Boolean types and don't allow them to be mixed (e.g., "(and #b1 true)" is an error).
Definition at line 63 of file SmtSolver.h.
Satisfiability constants.
| Enumerator | |
|---|---|
| SAT_NO |
Provably unsatisfiable. |
| SAT_YES |
Satisfiable and evidence of satisfiability may be available. |
| SAT_UNKNOWN |
Could not be proved satisfiable or unsatisfiable. |
Definition at line 87 of file SmtSolver.h.
Constructor & Destructor Documentation
|
inlineprotected |
Construct with name and linkage.
Every solver should have a name that will appear in diagnostic messages, such as "z3", and a linkage mode that describes how ROSE communicates with the solver. The linkage mode is chosen as the least significant set bit of linkages, therefore the subclass should ensure that linkages contains only valid bits. If linkages is zero then the constructed object will be useless since it has no way to communicate with the solver. You can check for this situation by reading the linkage property, or just wait for one of the other methods to throw an SmtSolver::Exception.
Definition at line 359 of file SmtSolver.h.
Member Function Documentation
|
pure virtual |
Virtual constructor.
The new solver will have the same settings as the source solver.
Implemented in Rose::BinaryAnalysis::Z3Solver, and Rose::BinaryAnalysis::SmtlibSolver.
|
static |
Availability of all known solvers.
Returns a map whose keys are the names of the SMT solver APIs and whose value is true if the solver is avilable or false if not available.
|
static |
Allocate a new solver by name.
Create a new solver using one of the names returned by availability. The special name "" means no solver (return null) and "best" means return bestAvailable (which might also be null). It may be possible to create solvers by name that are not available, but attempting to use such a solver will fail loudly by calling requireLinkage. If an invalid name is supplied then an SmtSolver::Exception is thrown.
|
static |
Best available solver.
Returns a new solver, an instance of the best available solver. If no solver is possible then returns null.
|
inline |
Property: Name of solver for debugging.
This name gets printed in various diagnostic messages. It's initialized to something reasonable by constructors, but can be changed at any time by the user.
Definition at line 404 of file SmtSolver.h.
|
inline |
Property: Name of solver for debugging.
This name gets printed in various diagnostic messages. It's initialized to something reasonable by constructors, but can be changed at any time by the user.
Definition at line 405 of file SmtSolver.h.
|
inline |
Property: How ROSE communicates with the solver.
The linkage is set when the solver object is created, and is read-only.
Definition at line 411 of file SmtSolver.h.
| void Rose::BinaryAnalysis::SmtSolver::requireLinkage | ( | LinkMode | ) | const |
Assert required linkage.
If the specified linkage is not available, then throw an exception.
|
static |
Given a bit vector of linkages, return the best one.
"Best" is defined as that with the best performance, which is usually direct calls to the solver's API.
| Memoizer::Ptr Rose::BinaryAnalysis::SmtSolver::memoizer | ( | ) | const |
Property: Memoizer.
The value of this property is a pointer to the object that caches the memoization for this solver. Setting it to a non-null pointer turns on memoization (using that object) and setting it to a null pointer turns off memoization. Memoization can be turned on or off at any time, and multiple SMT solvers can share the same memoizer.
| void Rose::BinaryAnalysis::SmtSolver::memoizer | ( | const Memoizer::Ptr & | ) |
Property: Memoizer.
The value of this property is a pointer to the object that caches the memoization for this solver. Setting it to a non-null pointer turns on memoization (using that object) and setting it to a null pointer turns off memoization. Memoization can be turned on or off at any time, and multiple SMT solvers can share the same memoizer.
|
pure virtual |
Set the timeout for the solver.
This sets the maximum time that the solver will try to find a solution before returning "unknown".
Implemented in Rose::BinaryAnalysis::Z3Solver, and Rose::BinaryAnalysis::SmtlibSolver.
|
virtual |
Determines if expressions are trivially satisfiable or unsatisfiable.
If all expressions are known 1-bit values that are true, then this function returns SAT_YES. If any expression is a known 1-bit value that is false, then this function returns SAT_NO. Otherwise this function returns SAT_UNKNOWN.
This is a high-level abstraction that resets this object state so it contains a single assertion set on its stack, and clears evidence of satisfiability.
|
virtual |
Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown.
This is a high-level abstraction that starts a new SMT solver session. For text-based interfaces, this solver object is reset, a temporary text file is created, the solver is run with the file as input, text output is read, and the evidence of satisfiability is parsed and stored in this object.
|
virtual |
Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown.
This is a high-level abstraction that starts a new SMT solver session. For text-based interfaces, this solver object is reset, a temporary text file is created, the solver is run with the file as input, text output is read, and the evidence of satisfiability is parsed and stored in this object.
|
virtual |
Reset solver state.
Resets the solver to an initial state containing no assertions. The evidence of satisfiability is cleared. For API-based solvers, this function might also create a new solver and/or solver context.
Reimplemented in Rose::BinaryAnalysis::Z3Solver, and Rose::BinaryAnalysis::SmtlibSolver.
|
inline |
Property: Throw an exception if the solver is reset.
This is used mostly for debugging solvers that are intending to use transactions. If the solver is ever reset, say by accidentally invoking its satisfiable method, then an exception is thrown.
Definition at line 485 of file SmtSolver.h.
|
inline |
Property: Throw an exception if the solver is reset.
This is used mostly for debugging solvers that are intending to use transactions. If the solver is ever reset, say by accidentally invoking its satisfiable method, then an exception is thrown.
Definition at line 488 of file SmtSolver.h.
|
virtual |
Create a backtracking point.
Pushes a new, empty set of assertions onto the solver stack.
Note that although text-based solvers (executables) accept push and pop methods, they have no effect on the speed of the solver because ROSE invokes the executable in batch mode. In this case the push and pop apply to the stack within this solver object in ROSE.
See also, pop.
|
virtual |
Pop a backtracking point.
Pops the top set of assertions from the solver stack. It is not legal to call pop when the assertion stack is only one level deep; use reset in that case instead.
Reimplemented in Rose::BinaryAnalysis::Z3Solver.
|
inlinevirtual |
Number of backtracking levels.
This is the number of sets of assertions. The push and pop increment and decrement this number. The return valued is always positive.
Definition at line 516 of file SmtSolver.h.
|
virtual |
Number of assertions at a specific backtracking level.
Backtracking levels are numbered starting at zero up to one less than the value returned by nLevels.
|
virtual |
Total number of assertions across all backtracking levels.
|
virtual |
Insert assertions.
Inserts assertions into the set of assertions at the top of the backtracking stack.
|
virtual |
Insert assertions.
Inserts assertions into the set of assertions at the top of the backtracking stack.
|
virtual |
All assertions.
Returns the list of all assertions across all backtracking points.
|
virtual |
Assertions for a particular level.
Returns the assertions associated with a particular level of the stack. Level zero is the oldest entry in the stack; all smt objects have a level zero. See also, nLevels.
|
virtual |
Check satisfiability of current stack.
Checks whether all assertions in the entire stack of assertion sets are satisfiable. A set of no assertions is trivially satisfiable. Errors are emitted on mlog once per error message and returned as SAT_UNKNOWN.
|
virtual |
Check whether the stack of assertions is trivially satisfiable.
This function returns true if all assertions have already been simplified in ROSE to the single bit "1", and returns true if so; false otherwise. If no assertions are present, this function returns true. This function does not invoke any functions in the underlying SMT solver.
|
virtual |
Names of items for which satisfiability evidence exists.
Returns a vector of strings (variable names or memory addresses) that can be passed to evidenceForName. Not all SMT solvers can return this information, in which case they return an empty vector.
The returned names are only for those variables and addresses whose evidence of satisfiability can be parsed by ROSE. The subclasses provide additional methods for obtaining more detailed information.
|
virtual |
Evidence of satisfiability for a variable or memory address.
If the string starts with the letter 'v' then variable evidence is returned, otherwise the string must be an address. Valid strings are those returned by the evidenceNames method; other strings result in a null return value. Subclasses might define additional methods for obtaining evidence of satisfiability.
Referenced by evidenceForVariable().
| Evidence Rose::BinaryAnalysis::SmtSolver::evidenceByName | ( | ) | const |
All evidence of satisfiability.
The version that returns a map indexed by variable name is the same as calling evidenceNames and then evidenceForName for each of those names.
The version that returns a map indexed by symbolic expression returns all the evidence in symbolic form. The keys for that return value are symbolic expressions that are simply variables.
Evidence is only returned if the previous check was satisfiable. Otherwise the return value is an empty map.
| ExprExprMap Rose::BinaryAnalysis::SmtSolver::evidence | ( | ) | const |
All evidence of satisfiability.
The version that returns a map indexed by variable name is the same as calling evidenceNames and then evidenceForName for each of those names.
The version that returns a map indexed by symbolic expression returns all the evidence in symbolic form. The keys for that return value are symbolic expressions that are simply variables.
Evidence is only returned if the previous check was satisfiable. Otherwise the return value is an empty map.
|
virtual |
Clears evidence information.
Evidence of satisfiability is cleared by calling this function or by calling any function that changes the state of the solver, such as pushing or popping assertion sets, inserting new assertions, or checking satisfiability. Checking satisfiability re-initializes the evidence.
Reimplemented in Rose::BinaryAnalysis::Z3Solver.
|
inlinevirtual |
Evidence of satisfiability for a bitvector variable.
If an expression is satisfiable, this function will return a value for the specified bitvector variable that satisfies the expression in conjunction with the other evidence. Not all SMT solvers can return this information. Returns the null pointer if no evidence is available for the variable.
Definition at line 617 of file SmtSolver.h.
|
inlinevirtual |
Evidence of satisfiability for a bitvector variable.
If an expression is satisfiable, this function will return a value for the specified bitvector variable that satisfies the expression in conjunction with the other evidence. Not all SMT solvers can return this information. Returns the null pointer if no evidence is available for the variable.
Definition at line 622 of file SmtSolver.h.
References evidenceForName().
|
virtual |
Evidence of satisfiability for a memory address.
If an expression is satisfiable, this function will return a value for the specified memory address that satisfies the expression in conjunction with the other evidence. Not all SMT solvers can return this information. Returns the null pointer if no evidence is available for the memory address.
|
inline |
Property: Statistics for this solver.
The statistics are not reset by this call, but continue to accumulate.
Definition at line 645 of file SmtSolver.h.
|
static |
Property: Statistics across all solvers.
The class statistics are updated whenever a solver is destroyed or its resetStatistics method is invoked. However, the nSolversCreated member is updated as soon as a solver is created.
The statistics are not reset by this call, but continue to accumulate.
| void Rose::BinaryAnalysis::SmtSolver::resetStatistics | ( | ) |
Resets statistics for this solver.
|
static |
Resets statistics for the class.
Statistics are reset to initial values for the class as a whole. Resetting statistics for the class does not affect statistics of any particular SMT solver object.
| Progress::Ptr Rose::BinaryAnalysis::SmtSolver::progress | ( | ) | const |
Progress reporting object.
If non-null, certain types of actions are reported to this progress object by pushing subtask progress objects.
| void Rose::BinaryAnalysis::SmtSolver::progress | ( | const Progress::Ptr & | progress | ) |
Progress reporting object.
If non-null, certain types of actions are reported to this progress object by pushing subtask progress objects.
|
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.
This function is also useful for debugging because it will convert ROSE's symbolic expressions to whatever format is used by the SMT solver.
|
protectedvirtual |
Check satisfiability using text files and an executable.
|
protectedvirtual |
Check satisfiability using a library API.
Reimplemented in Rose::BinaryAnalysis::Z3Solver.
|
protectedvirtual |
Error message from running a solver executable.
Given the solver exit status and (implicitly) the output of the solver, either return an error message or the empty string. This can be overridden by subclasses because some solvers exit with non-zero status if you try to get the model when (check-sat) returns not-satisfiable.
Reimplemented in Rose::BinaryAnalysis::SmtlibSolver.
|
inlineprotectedvirtual |
Return all variables that need declarations.
Reimplemented in Rose::BinaryAnalysis::SmtlibSolver.
Definition at line 703 of file SmtSolver.h.
|
staticprotected |
Print an S-Expr for debugging.
A null pointer is printed as "nil" and an empty list is printed as "()" in order to distinguish the two cases. There should be no null pointers though in well-formed S-Exprs.
|
protectedpure 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 Rose::BinaryAnalysis::SmtlibSolver.
|
protected |
Parse all SExprs from the specified string.
|
inlineprotectedvirtual |
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 Rose::BinaryAnalysis::Z3Solver, and Rose::BinaryAnalysis::SmtlibSolver.
Definition at line 720 of file SmtSolver.h.
|
staticprotected |
Normalize expressions by renaming variables.
This is used during memoization to rename all the variables. It performs a depth-first search and renames each variable it encounters. The variables are renumbered starting at zero. The return value is a vector new new expressions, some of which may be the unmodified original expressions if there were no variables. The index is also a return value which indicates how original variables were mapped to new variables.
|
staticprotected |
Undo the normalizations that were performed earlier.
Each of the specified expressions are rewritten by undoing the variable renaming that was done by normalizeVariables. The index is the same index as returned by normalizeVariables, although the input expressions need not be those same expressions. For each input expression, the expression is rewritten by substituting the inverse of the index. That is, a depth first search is performed on the expression and if the subexpression matches a value of the index, then it's replaced by the corresponding key.
|
virtual |
Unit tests.
Reimplemented in Rose::BinaryAnalysis::Z3Solver.
|
static |
Initialize diagnostic output facilities.
Called when the ROSE library is initialized.
Member Data Documentation
|
protected |
Additional output obtained by satisfiable().
Definition at line 313 of file SmtSolver.h.
|
static |
Diagnostic facility.
Definition at line 327 of file SmtSolver.h.
The documentation for this class was generated from the following file:
