klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Solver.h
Go to the documentation of this file.
1 //===-- Solver.h ------------------------------------------------*- C++ -*-===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 #ifndef KLEE_SOLVER_H
11 #define KLEE_SOLVER_H
12 
13 #include "klee/Expr.h"
14 
15 #include <vector>
16 
17 namespace klee {
18  class ConstraintManager;
19  class Expr;
20  class SolverImpl;
21 
22  struct Query {
23  public:
26 
27  Query(const ConstraintManager& _constraints, ref<Expr> _expr)
28  : constraints(_constraints), expr(_expr) {
29  }
30 
32  Query withExpr(ref<Expr> _expr) const {
33  return Query(constraints, _expr);
34  }
35 
37  Query withFalse() const {
39  }
40 
42  Query negateExpr() const {
44  }
45  };
46 
47  class Solver {
48  // DO NOT IMPLEMENT.
49  Solver(const Solver&);
50  void operator=(const Solver&);
51 
52  public:
53  enum Validity {
54  True = 1,
55  False = -1,
56  Unknown = 0
57  };
58 
59  public:
61  static const char *validity_to_str(Validity v);
62 
63  public:
65 
66  public:
67  Solver(SolverImpl *_impl) : impl(_impl) {}
68  virtual ~Solver();
69 
83  bool evaluate(const Query&, Validity &result);
84 
101  bool mustBeTrue(const Query&, bool &result);
102 
119  bool mustBeFalse(const Query&, bool &result);
120 
138  bool mayBeTrue(const Query&, bool &result);
139 
157  bool mayBeFalse(const Query&, bool &result);
158 
165  bool getValue(const Query&, ref<ConstantExpr> &result);
166 
178  //
179  // FIXME: This API is lame. We should probably just provide an API which
180  // returns an Assignment object, then clients can get out whatever values
181  // they want. This also allows us to optimize the representation.
182  bool getInitialValues(const Query&,
183  const std::vector<const Array*> &objects,
184  std::vector< std::vector<unsigned char> > &result);
185 
194  //
195  // FIXME: This should go into a helper class, and should handle failure.
196  virtual std::pair< ref<Expr>, ref<Expr> > getRange(const Query&);
197 
198  virtual char *getConstraintLog(const Query& query);
199  virtual void setCoreSolverTimeout(double timeout);
200  };
201 
203  class STPSolver : public Solver {
204  public:
211  STPSolver(bool useForkedSTP, bool optimizeDivides = true);
212 
215  virtual char *getConstraintLog(const Query&);
216 
219  virtual void setCoreSolverTimeout(double timeout);
220  };
221 
222 
223 #ifdef SUPPORT_METASMT
224 
225  template<typename SolverContext>
226  class MetaSMTSolver : public Solver {
227  public:
228  MetaSMTSolver(bool useForked, bool optimizeDivides);
229  virtual ~MetaSMTSolver();
230 
231  virtual char *getConstraintLog(const Query&);
232  virtual void setCoreSolverTimeout(double timeout);
233 };
234 
235 #endif /* SUPPORT_METASMT */
236 
237  /* *** */
238 
246  Solver *createValidatingSolver(Solver *s, Solver *oracle);
247 
252  Solver *createCachingSolver(Solver *s);
253 
260  Solver *createCexCachingSolver(Solver *s);
261 
267  Solver *createFastCexSolver(Solver *s);
268 
274  Solver *createIndependentSolver(Solver *s);
275 
278  Solver *createPCLoggingSolver(Solver *s, std::string path,
279  int minQueryTimeToLog);
280 
283  Solver *createSMTLIBLoggingSolver(Solver *s, std::string path,
284  int minQueryTimeToLog);
285 
286 
289  Solver *createDummySolver();
290 
291 }
292 
293 #endif
virtual ~Solver()
Definition: Solver.cpp:120
Solver * createSMTLIBLoggingSolver(Solver *s, std::string path, int minQueryTimeToLog)
static const char * validity_to_str(Validity v)
validity_to_str - Return the name of given Validity enum value.
Definition: Solver.cpp:112
bool getValue(const Query &, ref< ConstantExpr > &result)
Definition: Solver.cpp:176
#define Expr
Definition: STPBuilder.h:19
bool evaluate(const Query &, Validity &result)
Definition: Solver.cpp:132
SolverImpl - Abstract base clase for solver implementations.
Definition: SolverImpl.h:22
Solver * createFastCexSolver(Solver *s)
ref< Expr > expr
Definition: Solver.h:25
void operator=(const Solver &)
Query withFalse() const
withFalse - Return a copy of the query with a false expression.
Definition: Solver.h:37
Solver * createCachingSolver(Solver *s)
bool mustBeTrue(const Query &, bool &result)
Definition: Solver.cpp:144
Query negateExpr() const
negateExpr - Return a copy of the query with the expression negated.
Definition: Solver.h:42
bool mustBeFalse(const Query &, bool &result)
Definition: Solver.cpp:156
virtual char * getConstraintLog(const Query &)
Definition: Solver.cpp:570
bool mayBeTrue(const Query &, bool &result)
Definition: Solver.cpp:160
static ref< Expr > createIsZero(ref< Expr > e)
Definition: Expr.cpp:305
const ConstraintManager & constraints
Definition: Solver.h:24
Query withExpr(ref< Expr > _expr) const
withExpr - Return a copy of the query with the given expression.
Definition: Solver.h:32
bool mayBeFalse(const Query &, bool &result)
Definition: Solver.cpp:168
virtual char * getConstraintLog(const Query &query)
Definition: Solver.cpp:124
Query(const ConstraintManager &_constraints, ref< Expr > _expr)
Definition: Solver.h:27
SolverImpl * impl
Definition: Solver.h:64
virtual void setCoreSolverTimeout(double timeout)
Definition: Solver.cpp:574
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:398
STPSolver(bool useForkedSTP, bool optimizeDivides=true)
Definition: Solver.cpp:565
virtual void setCoreSolverTimeout(double timeout)
Definition: Solver.cpp:128
Solver * createIndependentSolver(Solver *s)
bool getInitialValues(const Query &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &result)
Definition: Solver.cpp:193
Solver * createValidatingSolver(Solver *s, Solver *oracle)
Definition: Solver.cpp:450
static const Width Bool
Definition: Expr.h:97
Solver(SolverImpl *_impl)
Definition: Solver.h:67
Solver * createPCLoggingSolver(Solver *s, std::string path, int minQueryTimeToLog)
Solver(const Solver &)
Solver * createDummySolver()
Definition: Solver.cpp:489
Solver * createCexCachingSolver(Solver *s)
STPSolver - A complete solver based on STP.
Definition: Solver.h:203
virtual std::pair< ref< Expr >, ref< Expr > > getRange(const Query &)
Definition: Solver.cpp:206