1 //===-- DummySolver.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/Solver/Solver.h"
11 #include "klee/Solver/SolverImpl.h"
12 #include "klee/Solver/SolverStats.h"
13
14 namespace klee {
15
16 class DummySolverImpl : public SolverImpl {
17 public:
18 DummySolverImpl();
19
20 bool computeValidity(const Query &, Solver::Validity &result);
21 bool computeTruth(const Query &, bool &isValid);
22 bool computeValue(const Query &, ref<Expr> &result);
23 bool computeInitialValues(const Query &,
24 const std::vector<const Array *> &objects,
25 std::vector<std::vector<unsigned char> > &values,
26 bool &hasSolution);
27 SolverRunStatus getOperationStatusCode();
28 };
29
DummySolverImpl()30 DummySolverImpl::DummySolverImpl() {}
31
computeValidity(const Query &,Solver::Validity & result)32 bool DummySolverImpl::computeValidity(const Query &, Solver::Validity &result) {
33 ++stats::queries;
34 // FIXME: We should have stats::queriesFail;
35 return false;
36 }
37
computeTruth(const Query &,bool & isValid)38 bool DummySolverImpl::computeTruth(const Query &, bool &isValid) {
39 ++stats::queries;
40 // FIXME: We should have stats::queriesFail;
41 return false;
42 }
43
computeValue(const Query &,ref<Expr> & result)44 bool DummySolverImpl::computeValue(const Query &, ref<Expr> &result) {
45 ++stats::queries;
46 ++stats::queryCounterexamples;
47 return false;
48 }
49
computeInitialValues(const Query &,const std::vector<const Array * > & objects,std::vector<std::vector<unsigned char>> & values,bool & hasSolution)50 bool DummySolverImpl::computeInitialValues(
51 const Query &, const std::vector<const Array *> &objects,
52 std::vector<std::vector<unsigned char> > &values, bool &hasSolution) {
53 ++stats::queries;
54 ++stats::queryCounterexamples;
55 return false;
56 }
57
getOperationStatusCode()58 SolverImpl::SolverRunStatus DummySolverImpl::getOperationStatusCode() {
59 return SOLVER_RUN_STATUS_FAILURE;
60 }
61
createDummySolver()62 Solver *createDummySolver() { return new Solver(new DummySolverImpl()); }
63 }
64