klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
IncompleteSolver.h
Go to the documentation of this file.
1 //===-- IncompleteSolver.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_INCOMPLETESOLVER_H
11 #define KLEE_INCOMPLETESOLVER_H
12 
13 #include "klee/Solver.h"
14 #include "klee/SolverImpl.h"
15 
16 namespace klee {
17 
26 public:
32 
35 
38  MayBeTrue = 2,
39 
42  MayBeFalse = -2,
43 
46 
48  None = 3
49  };
50 
52 
53 public:
55  virtual ~IncompleteSolver() {}
56 
65 
70 
72  virtual bool computeValue(const Query&, ref<Expr> &result) = 0;
73 
77  virtual bool computeInitialValues(const Query&,
78  const std::vector<const Array*>
79  &objects,
80  std::vector< std::vector<unsigned char> >
81  &values,
82  bool &hasSolution) = 0;
83 };
84 
88 class StagedSolverImpl : public SolverImpl {
89 private:
92 
93 public:
94  StagedSolverImpl(IncompleteSolver *_primary, Solver *_secondary);
96 
97  bool computeTruth(const Query&, bool &isValid);
98  bool computeValidity(const Query&, Solver::Validity &result);
99  bool computeValue(const Query&, ref<Expr> &result);
100  bool computeInitialValues(const Query&,
101  const std::vector<const Array*> &objects,
102  std::vector< std::vector<unsigned char> > &values,
103  bool &hasSolution);
105  char *getConstraintLog(const Query&);
106  void setCoreSolverTimeout(double timeout);
107 };
108 
109 }
110 
111 #endif
The validity of the query is unknown.
char * getConstraintLog(const Query &)
IncompleteSolver * primary
virtual IncompleteSolver::PartialValidity computeTruth(const Query &)=0
StagedSolverImpl(IncompleteSolver *_primary, Solver *_secondary)
virtual IncompleteSolver::PartialValidity computeValidity(const Query &)
SolverImpl - Abstract base clase for solver implementations.
Definition: SolverImpl.h:22
virtual bool computeInitialValues(const Query &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)=0
bool computeValidity(const Query &, Solver::Validity &result)
void setCoreSolverTimeout(double timeout)
The query is provably true.
static PartialValidity negatePartialValidity(PartialValidity pv)
The query is provably false.
The query is known to have both true and false assignments.
virtual bool computeValue(const Query &, ref< Expr > &result)=0
computeValue - Attempt to compute a value for the given expression.
bool computeInitialValues(const Query &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)
bool computeTruth(const Query &, bool &isValid)
bool computeValue(const Query &, ref< Expr > &result)
SolverRunStatus getOperationStatusCode()
getOperationStatusCode - get the status of the last solver operation