1 #ifndef ROSE_BinaryAnalysis_YicesSolver_H
2 #define ROSE_BinaryAnalysis_YicesSolver_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
6 #include <Rose/BinaryAnalysis/SmtSolver.h>
7 #include <Sawyer/Map.h>
8 #include <boost/serialization/access.hpp>
9 #include <boost/serialization/base_object.hpp>
10 #include <boost/serialization/export.hpp>
12 #ifdef ROSE_HAVE_LIBYICES
17 namespace BinaryAnalysis {
29 typedef std::map<std::string, std::pair<
size_t, uint64_t> >
Evidence;
32 #ifdef ROSE_HAVE_LIBYICES
33 yices_context context;
39 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
41 friend class boost::serialization::access;
44 void serialize(S &s,
const unsigned ) {
45 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
SmtSolver);
58 #ifdef ROSE_HAVE_LIBYICES
92 virtual void reset()
override;
96 virtual void timeout(boost::chrono::duration<double>)
override;
101 virtual std::string
getCommand(
const std::string &config_name)
override;
115 Type most_type(
const std::vector<SExprTypePair>&);
116 std::vector<SExprTypePair> out_exprs(
const std::vector<SymbolicExpr::Ptr>&);
117 std::vector<SExprTypePair> out_cast(
const std::vector<SExprTypePair>&,
Type toType);
118 void out_comments(std::ostream&,
const std::vector<SymbolicExpr::Ptr>&);
119 void out_common_subexpressions(std::ostream&,
const std::vector<SymbolicExpr::Ptr>&);
120 void out_define(std::ostream&,
const std::vector<SymbolicExpr::Ptr>&,
Definitions*);
123 SExprTypePair out_cast(
const SExprTypePair&,
Type toType);
125 SExprTypePair out_unary(
const char *opname,
const SExprTypePair&,
Type rettype = NO_TYPE);
130 SExprTypePair out_la(
const char *opname,
const std::vector<SExprTypePair>&,
Type rettype = NO_TYPE);
144 #ifdef ROSE_HAVE_LIBYICES
145 typedef std::pair<yices_expr, Type> YExprTypePair;
150 typedef yices_expr (*UnaryAPI)(yices_context, yices_expr operand);
151 typedef yices_expr (*BinaryAPI)(yices_context, yices_expr operand1, yices_expr operand2);
152 typedef yices_expr (*NaryAPI)(yices_context, yices_expr *operands,
unsigned n_operands);
153 typedef yices_expr (*ShiftAPI)(yices_context, yices_expr,
unsigned amount);
155 Type most_type(
const std::vector<YExprTypePair>&);
156 void ctx_common_subexpressions(
const std::vector<SymbolicExpr::Ptr>&);
157 void ctx_define(
const std::vector<SymbolicExpr::Ptr>&,
Definitions*);
159 std::vector<YExprTypePair> ctx_exprs(
const std::vector<SymbolicExpr::Ptr>&);
160 YExprTypePair ctx_cast(
const YExprTypePair&,
Type toType);
161 std::vector<YExprTypePair> ctx_cast(
const std::vector<YExprTypePair>&,
Type toType);
163 YExprTypePair ctx_unary(UnaryAPI,
const YExprTypePair&,
Type rettype = NO_TYPE);
168 YExprTypePair ctx_la(BinaryAPI,
const std::vector<YExprTypePair>&,
Type rettype = NO_TYPE);
170 YExprTypePair ctx_la(NaryAPI,
const std::vector<YExprTypePair>&,
Type rettype = NO_TYPE);
189 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
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...
static unsigned availableLinkages()
Returns a bit vector of linkage capabilities.
virtual void generateFile(std::ostream &, const std::vector< SymbolicExpr::Ptr > &exprs, Definitions *) override
Generates an input file for for the solver.
LinkMode
Bit flags to indicate the kind of solver interface.
Main namespace for the ROSE library.
std::set< uint64_t > Definitions
Free variables that have been defined.
virtual SymbolicExpr::Ptr evidenceForName(const std::string &) override
Evidence of satisfiability for a variable or memory address.
Satisfiable
Satisfiability constants.
virtual void parseEvidence() override
Parses evidence of satisfiability.
bool memoization() const
Property: Perform memoization.
virtual void clearEvidence() override
Clears evidence information.
virtual std::vector< std::string > evidenceNames() override
Names of items for which satisfiability evidence exists.
SmtSolver(const std::string &name, unsigned linkages)
Construct with name and linkage.
Interface to the Yices Satisfiability Modulo Theory (SMT) Solver.
static Ptr instance(unsigned linkages=LM_ANY)
Constructs object to communicate with Yices solver.
virtual void timeout(boost::chrono::duration< double >) override
Set the timeout for the solver.
virtual void reset() override
Reset solver state.
virtual Satisfiable checkLib() override
Check satisfiability using a library API.
Type
Type (sort) of expression.
Interface to Satisfiability Modulo Theory (SMT) solvers.
virtual Ptr create() const override
Virtual constructor.
Evidence evidence()
All evidence of satisfiability.