Description
Interface to the Yices Satisfiability Modulo Theory (SMT) Solver.
ROSE should be configured with –with-yices in order for the satisfiable() virtual method to work (otherwise, the YicesSolver class is still available but will fail an assertion when instantiated).
Yices provides two interfaces: an executable named "yices", and a library. The choice of which linkage to use to answer satisfiability questions is made at runtime (see set_linkage()).
Definition at line 27 of file YicesSolver.h.
#include <YicesSolver.h>
Public Member Functions | |
| virtual Ptr | create () const override |
| Virtual constructor. More... | |
| virtual void | reset () override |
| Reset solver state. More... | |
| virtual void | clearEvidence () override |
| Clears evidence information. More... | |
| virtual std::vector< std::string > | evidenceNames () override |
| Names of items for which satisfiability evidence exists. More... | |
| virtual SymbolicExpr::Ptr | evidenceForName (const std::string &) override |
| Evidence of satisfiability for a variable or memory address. More... | |
| virtual void | timeout (boost::chrono::duration< double >) override |
| Set the timeout for the solver. More... | |
| void | varForSet (const SymbolicExpr::InteriorPtr &set, const SymbolicExpr::LeafPtr &var) |
| SymbolicExpr::LeafPtr | varForSet (const SymbolicExpr::InteriorPtr &set) |
 Public Member Functions inherited from Rose::BinaryAnalysis::SmtSolver | |
| LinkMode | linkage () const |
| Property: How ROSE communicates with the solver. More... | |
| void | requireLinkage (LinkMode) const |
| Assert required linkage. More... | |
| Sawyer::Optional< SymbolicExpr::Hash > | latestMemoizationId () const |
| Id for latest memoized result, or zero. More... | |
| virtual void | clearMemoization () |
| Clear memoization table. More... | |
| virtual size_t | memoizationNEntries () const |
| Size of memoization table. More... | |
| virtual Satisfiable | triviallySatisfiable (const std::vector< SymbolicExpr::Ptr > &exprs) |
| Determines if expressions are trivially satisfiable or unsatisfiable. 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 std::vector< SymbolicExpr::Ptr > | assertions () const |
| All assertions. More... | |
| virtual std::vector< SymbolicExpr::Ptr > | 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... | |
| Evidence | evidence () |
| All evidence of satisfiability. More... | |
| virtual SymbolicExpr::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 | 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... | |
| bool | memoization () const |
| Property: Perform memoization. More... | |
| void | memoization (bool b) |
| Property: Perform memoization. More... | |
| virtual Satisfiable | satisfiable (const SymbolicExpr::Ptr &) |
| Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown. More... | |
| virtual Satisfiable | satisfiable (const std::vector< SymbolicExpr::Ptr > &) |
| 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 SymbolicExpr::Ptr &) |
| Insert assertions. More... | |
| virtual void | insert (const std::vector< SymbolicExpr::Ptr > &) |
| Insert assertions. More... | |
| virtual SymbolicExpr::Ptr | evidenceForVariable (const SymbolicExpr::Ptr &var) |
| Evidence of satisfiability for a bitvector variable. More... | |
| virtual SymbolicExpr::Ptr | evidenceForVariable (uint64_t varno) |
| Evidence of satisfiability for a bitvector variable. More... | |
Static Public Member Functions | |
| static Ptr | instance (unsigned linkages=LM_ANY) |
| Constructs object to communicate with Yices solver. More... | |
| static unsigned | availableLinkages () |
| Returns a bit vector of linkage capabilities. More... | |
| Static Public Member Functions inherited from Rose::BinaryAnalysis::SmtSolver | |
| 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... | |
Protected Types | |
| typedef std::map< std::string, std::pair< size_t, uint64_t > > | Evidence |
| typedef std::pair< yices_expr, Type > | YExprTypePair |
| typedef Sawyer::Container::Map< SymbolicExpr::Ptr, YExprTypePair > | TermExprs |
| typedef yices_expr(* | UnaryAPI) (yices_context, yices_expr operand) |
| typedef yices_expr(* | BinaryAPI) (yices_context, yices_expr operand1, yices_expr operand2) |
| typedef yices_expr(* | NaryAPI) (yices_context, yices_expr *operands, unsigned n_operands) |
| typedef yices_expr(* | ShiftAPI) (yices_context, yices_expr, unsigned amount) |
Protected Member Functions | |
| YicesSolver (unsigned linkages=LM_ANY) | |
| virtual Satisfiable | checkLib () override |
| Check satisfiability using a library API. More... | |
| virtual void | generateFile (std::ostream &, const std::vector< SymbolicExpr::Ptr > &exprs, Definitions *) override |
| Generates an input file for for the solver. More... | |
| virtual std::string | getCommand (const std::string &config_name) override |
| Given the name of a configuration file, return the command that is needed to run the solver. More... | |
| virtual void | parseEvidence () override |
| Parses evidence of satisfiability. More... | |
| Type | most_type (const std::vector< SExprTypePair > &) |
| std::vector< SExprTypePair > | out_exprs (const std::vector< SymbolicExpr::Ptr > &) |
| std::vector< SExprTypePair > | out_cast (const std::vector< SExprTypePair > &, Type toType) |
| void | out_comments (std::ostream &, const std::vector< SymbolicExpr::Ptr > &) |
| void | out_common_subexpressions (std::ostream &, const std::vector< SymbolicExpr::Ptr > &) |
| void | out_define (std::ostream &, const std::vector< SymbolicExpr::Ptr > &, Definitions *) |
| void | out_assert (std::ostream &, const SymbolicExpr::Ptr &) |
| void | out_number (std::ostream &, const SymbolicExpr::Ptr &) |
| SExprTypePair | out_cast (const SExprTypePair &, Type toType) |
| SExprTypePair | out_expr (const SymbolicExpr::Ptr &) |
| SExprTypePair | out_unary (const char *opname, const SExprTypePair &, Type rettype=NO_TYPE) |
| SExprTypePair | out_binary (const char *opname, const SymbolicExpr::InteriorPtr &, Type rettype=NO_TYPE) |
| SExprTypePair | out_ite (const SymbolicExpr::InteriorPtr &) |
| SExprTypePair | out_set (const SymbolicExpr::InteriorPtr &) |
| SExprTypePair | out_la (const char *opname, const SymbolicExpr::InteriorPtr &, Type rettype=NO_TYPE) |
| SExprTypePair | out_la (const char *opname, const std::vector< SExprTypePair > &, Type rettype=NO_TYPE) |
| SExprTypePair | out_extract (const SymbolicExpr::InteriorPtr &) |
| SExprTypePair | out_sext (const SymbolicExpr::InteriorPtr &) |
| SExprTypePair | out_uext (const SymbolicExpr::InteriorPtr &) |
| SExprTypePair | out_shift (const char *opname, const SymbolicExpr::InteriorPtr &, bool newbits) |
| SExprTypePair | out_asr (const SymbolicExpr::InteriorPtr &) |
| SExprTypePair | out_zerop (const SymbolicExpr::InteriorPtr &) |
| SExprTypePair | out_mult (const SymbolicExpr::InteriorPtr &) |
| SExprTypePair | out_read (const SymbolicExpr::InteriorPtr &) |
| SExprTypePair | out_write (const SymbolicExpr::InteriorPtr &) |
| Type | most_type (const std::vector< YExprTypePair > &) |
| void | ctx_common_subexpressions (const std::vector< SymbolicExpr::Ptr > &) |
| void | ctx_define (const std::vector< SymbolicExpr::Ptr > &, Definitions *) |
| void | ctx_assert (const SymbolicExpr::Ptr &) |
| std::vector< YExprTypePair > | ctx_exprs (const std::vector< SymbolicExpr::Ptr > &) |
| YExprTypePair | ctx_cast (const YExprTypePair &, Type toType) |
| std::vector< YExprTypePair > | ctx_cast (const std::vector< YExprTypePair > &, Type toType) |
| YExprTypePair | ctx_expr (const SymbolicExpr::Ptr &) |
| YExprTypePair | ctx_unary (UnaryAPI, const YExprTypePair &, Type rettype=NO_TYPE) |
| YExprTypePair | ctx_binary (BinaryAPI, const SymbolicExpr::InteriorPtr &, Type rettype=NO_TYPE) |
| YExprTypePair | ctx_ite (const SymbolicExpr::InteriorPtr &) |
| YExprTypePair | ctx_set (const SymbolicExpr::InteriorPtr &) |
| YExprTypePair | ctx_la (BinaryAPI, const SymbolicExpr::InteriorPtr &, Type rettype=NO_TYPE) |
| YExprTypePair | ctx_la (BinaryAPI, const std::vector< YExprTypePair > &, Type rettype=NO_TYPE) |
| YExprTypePair | ctx_la (NaryAPI, const SymbolicExpr::InteriorPtr &, Type rettype=NO_TYPE) |
| YExprTypePair | ctx_la (NaryAPI, const std::vector< YExprTypePair > &, Type rettype=NO_TYPE) |
| YExprTypePair | ctx_extract (const SymbolicExpr::InteriorPtr &) |
| YExprTypePair | ctx_sext (const SymbolicExpr::InteriorPtr &) |
| YExprTypePair | ctx_uext (const SymbolicExpr::InteriorPtr &) |
| YExprTypePair | ctx_shift (ShiftAPI, const SymbolicExpr::InteriorPtr &) |
| YExprTypePair | ctx_asr (const SymbolicExpr::InteriorPtr &) |
| YExprTypePair | ctx_zerop (const SymbolicExpr::InteriorPtr &) |
| YExprTypePair | ctx_mult (const SymbolicExpr::InteriorPtr &) |
| YExprTypePair | ctx_read (const SymbolicExpr::InteriorPtr &) |
| YExprTypePair | ctx_write (const SymbolicExpr::InteriorPtr &) |
| Protected Member Functions inherited from Rose::BinaryAnalysis::SmtSolver | |
| 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 std::string | getErrorMessage (int exitStatus) |
| Error message from running a solver executable. More... | |
| virtual void | findVariables (const SymbolicExpr::Ptr &, VariableSet &) |
| Return all variables that need declarations. More... | |
| std::vector< SExpr::Ptr > | parseSExpressions (const std::string &) |
| Parse all SExprs from the specified string. More... | |
Protected Attributes | |
| Evidence | evidence |
| TermExprs | termExprs |
| Protected Attributes inherited from Rose::BinaryAnalysis::SmtSolver | |
| LinkMode | linkage_ |
| std::string | outputText_ |
| Additional output obtained by satisfiable(). More... | |
| std::vector< SExpr::Ptr > | parsedOutput_ |
| TermNames | termNames_ |
| Memoization | memoization_ |
| bool | doMemoization_ |
| Sawyer::Optional< SymbolicExpr::Hash > | latestMemoizationId_ |
| SymbolicExpr::ExprExprHashMap | latestMemoizationRewrite_ |
| Stats | stats |
Additional Inherited Members | |
| Public Types inherited from Rose::BinaryAnalysis::SmtSolver | |
| 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 | Ptr = SmtSolverPtr |
| Reference counting pointer for SMT solvers. More... | |
| typedef std::map< std::string, bool > | Availability |
| Solver availability map. More... | |
| typedef std::pair< std::string, Type > | StringTypePair |
| Maps expression nodes to term names. More... | |
| typedef Sawyer::Container::Map< SymbolicExpr::Ptr, StringTypePair > | TermNames |
| typedef Sawyer::Container::Map< SymbolicExpr::Ptr, SymbolicExpr::Ptr > | ExprExprMap |
| Maps one symbolic expression to another. More... | |
| typedef Sawyer::Container::Set< SymbolicExpr::LeafPtr, CompareLeavesByName > | VariableSet |
| Set of variables. More... | |
| typedef std::set< uint64_t > | Definitions |
| Free variables that have been defined. More... | |
| typedef std::pair< SExpr::Ptr, Type > | SExprTypePair |
| typedef boost::unordered_map< SymbolicExpr::Hash, Satisfiable > | Memoization |
| using | Evidence = Sawyer::Container::Map< std::string, SymbolicExpr::Ptr > |
| Evidence of satisfiability. More... | |
| Static Public Attributes inherited from Rose::BinaryAnalysis::SmtSolver | |
| static Sawyer::Message::Facility | mlog |
| Diagnostic facility. More... | |
| Static Protected Member Functions inherited from Rose::BinaryAnalysis::SmtSolver | |
| static void | printSExpression (std::ostream &, const SExpr::Ptr &) |
| Print an S-Expr for debugging. More... | |
| static std::vector< SymbolicExpr::Ptr > | normalizeVariables (const std::vector< SymbolicExpr::Ptr > &, SymbolicExpr::ExprExprHashMap &index) |
| Normalize expressions by renaming variables. More... | |
| static std::vector< SymbolicExpr::Ptr > | undoNormalization (const std::vector< SymbolicExpr::Ptr > &, const SymbolicExpr::ExprExprHashMap &index) |
| Undo the normalizations that were performed earlier. More... | |
| Static Protected Attributes inherited from Rose::BinaryAnalysis::SmtSolver | |
| static boost::mutex | classStatsMutex |
| static Stats | classStats |
Member Function Documentation
Constructs object to communicate with Yices solver.
The solver will be named "Yices" (see Naming tips property) and will use the library linkage if the Yices library is present, otherwise the executable linkage. If neither is available then an SmtSolver::Exception is thrown.
Definition at line 70 of file YicesSolver.h.
|
overridevirtual |
Virtual constructor.
Create a new solver just like this one.
Implements Rose::BinaryAnalysis::SmtSolver.
|
static |
Returns a bit vector of linkage capabilities.
Returns a vector of LinkMode bits that say what possible modes of communicating with the Yices SMT solver are available. A return value of zero means the Yices solver is not supported in this configuration of ROSE.
|
overridevirtual |
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 from Rose::BinaryAnalysis::SmtSolver.
|
overridevirtual |
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 from Rose::BinaryAnalysis::SmtSolver.
|
overridevirtual |
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.
Reimplemented from Rose::BinaryAnalysis::SmtSolver.
|
overridevirtual |
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.
Reimplemented from Rose::BinaryAnalysis::SmtSolver.
|
overridevirtual |
Set the timeout for the solver.
This sets the maximum time that the solver will try to find a solution before returning "unknown".
Implements Rose::BinaryAnalysis::SmtSolver.
|
overrideprotectedvirtual |
Check satisfiability using a library API.
Reimplemented from Rose::BinaryAnalysis::SmtSolver.
|
overrideprotectedvirtual |
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.
Implements Rose::BinaryAnalysis::SmtSolver.
|
overrideprotectedvirtual |
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".
Implements Rose::BinaryAnalysis::SmtSolver.
|
overrideprotectedvirtual |
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 from Rose::BinaryAnalysis::SmtSolver.
The documentation for this class was generated from the following file:
