klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
SolverImpl.h
Go to the documentation of this file.
1 //===-- SolverImpl.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_SOLVERIMPL_H
11 #define KLEE_SOLVERIMPL_H
12 
13 #include <vector>
14 
15 namespace klee {
16  class Array;
17  class ExecutionState;
18  class Expr;
19  struct Query;
20 
22  class SolverImpl {
23  // DO NOT IMPLEMENT.
24  SolverImpl(const SolverImpl&);
25  void operator=(const SolverImpl&);
26 
27  public:
29  virtual ~SolverImpl();
30 
39 
60  virtual bool computeValidity(const Query& query, Solver::Validity &result);
61 
77  virtual bool computeTruth(const Query& query, bool &isValid) = 0;
78 
84  virtual bool computeValue(const Query& query, ref<Expr> &result) = 0;
85 
87  virtual bool computeInitialValues(const Query& query,
88  const std::vector<const Array*>
89  &objects,
90  std::vector< std::vector<unsigned char> >
91  &values,
92  bool &hasSolution) = 0;
93 
96 
99  static const char* getOperationStatusString(SolverRunStatus statusCode);
100 
101  virtual char *getConstraintLog(const Query& query) {
102  // dummy
103  return(NULL);
104  }
105 
106  virtual void setCoreSolverTimeout(double timeout) {};
107 };
108 
109 }
110 
111 #endif
void operator=(const SolverImpl &)
#define Expr
Definition: STPBuilder.h:19
SolverImpl - Abstract base clase for solver implementations.
Definition: SolverImpl.h:22
virtual ~SolverImpl()
Definition: Solver.cpp:70
virtual void setCoreSolverTimeout(double timeout)
Definition: SolverImpl.h:106
virtual bool computeValidity(const Query &query, Solver::Validity &result)
Definition: Solver.cpp:73
virtual bool computeInitialValues(const Query &query, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)=0
virtual SolverRunStatus getOperationStatusCode()=0
getOperationStatusCode - get the status of the last solver operation
virtual bool computeTruth(const Query &query, bool &isValid)=0
virtual char * getConstraintLog(const Query &query)
Definition: SolverImpl.h:101
virtual bool computeValue(const Query &query, ref< Expr > &result)=0
static const char * getOperationStatusString(SolverRunStatus statusCode)
Definition: Solver.cpp:87