klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
IncompleteSolver.cpp
Go to the documentation of this file.
1 //===-- IncompleteSolver.cpp ----------------------------------------------===//
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 #include "klee/IncompleteSolver.h"
11 
12 #include "klee/Constraints.h"
13 
14 using namespace klee;
15 using namespace llvm;
16 
17 /***/
18 
21  switch(pv) {
22  default: assert(0 && "invalid partial validity");
23  case MustBeTrue: return MustBeFalse;
24  case MustBeFalse: return MustBeTrue;
25  case MayBeTrue: return MayBeFalse;
26  case MayBeFalse: return MayBeTrue;
27  case TrueOrFalse: return TrueOrFalse;
28  }
29 }
30 
33  PartialValidity trueResult = computeTruth(query);
34 
35  if (trueResult == MustBeTrue) {
36  return MustBeTrue;
37  } else {
38  PartialValidity falseResult = computeTruth(query.negateExpr());
39 
40  if (falseResult == MustBeTrue) {
41  return MustBeFalse;
42  } else {
43  bool trueCorrect = trueResult != None,
44  falseCorrect = falseResult != None;
45 
46  if (trueCorrect && falseCorrect) {
47  return TrueOrFalse;
48  } else if (trueCorrect) { // ==> trueResult == MayBeFalse
49  return MayBeFalse;
50  } else if (falseCorrect) { // ==> falseResult == MayBeFalse
51  return MayBeTrue;
52  } else {
53  return None;
54  }
55  }
56  }
57 }
58 
59 /***/
60 
62  Solver *_secondary)
63  : primary(_primary),
64  secondary(_secondary) {
65 }
66 
68  delete primary;
69  delete secondary;
70 }
71 
72 bool StagedSolverImpl::computeTruth(const Query& query, bool &isValid) {
74 
75  if (trueResult != IncompleteSolver::None) {
76  isValid = (trueResult == IncompleteSolver::MustBeTrue);
77  return true;
78  }
79 
80  return secondary->impl->computeTruth(query, isValid);
81 }
82 
84  Solver::Validity &result) {
85  bool tmp;
86 
87  switch(primary->computeValidity(query)) {
89  result = Solver::True;
90  break;
92  result = Solver::False;
93  break;
95  result = Solver::Unknown;
96  break;
98  if (!secondary->impl->computeTruth(query, tmp))
99  return false;
100  result = tmp ? Solver::True : Solver::Unknown;
101  break;
103  if (!secondary->impl->computeTruth(query.negateExpr(), tmp))
104  return false;
105  result = tmp ? Solver::False : Solver::Unknown;
106  break;
107  default:
108  if (!secondary->impl->computeValidity(query, result))
109  return false;
110  break;
111  }
112 
113  return true;
114 }
115 
117  ref<Expr> &result) {
118  if (primary->computeValue(query, result))
119  return true;
120 
121  return secondary->impl->computeValue(query, result);
122 }
123 
124 bool
126  const std::vector<const Array*>
127  &objects,
128  std::vector< std::vector<unsigned char> >
129  &values,
130  bool &hasSolution) {
131  if (primary->computeInitialValues(query, objects, values, hasSolution))
132  return true;
133 
134  return secondary->impl->computeInitialValues(query, objects, values,
135  hasSolution);
136 }
137 
140 }
141 
143  return secondary->impl->getConstraintLog(query);
144 }
145 
148 }
149 
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 &)
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.
virtual void setCoreSolverTimeout(double timeout)
Definition: SolverImpl.h:106
static PartialValidity negatePartialValidity(PartialValidity pv)
Query negateExpr() const
negateExpr - Return a copy of the query with the expression negated.
Definition: Solver.h:42
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
The query is provably false.
SolverImpl * impl
Definition: Solver.h:64
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)
virtual SolverRunStatus getOperationStatusCode()=0
getOperationStatusCode - get the status of the last solver operation
virtual bool computeTruth(const Query &query, bool &isValid)=0
bool computeValue(const Query &, ref< Expr > &result)
virtual char * getConstraintLog(const Query &query)
Definition: SolverImpl.h:101
SolverRunStatus getOperationStatusCode()
getOperationStatusCode - get the status of the last solver operation
virtual bool computeValue(const Query &query, ref< Expr > &result)=0