diff options
Diffstat (limited to 'lib/Solver/Solver.cpp')
-rw-r--r-- | lib/Solver/Solver.cpp | 40 |
1 files changed, 0 insertions, 40 deletions
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index e596d37d..07e8b8a0 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -276,46 +276,6 @@ std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) { ConstantExpr::create(max, width)); } - -/***/ - -class DummySolverImpl : public SolverImpl { -public: - DummySolverImpl() {} - - bool computeValidity(const Query&, Solver::Validity &result) { - ++stats::queries; - // FIXME: We should have stats::queriesFail; - return false; - } - bool computeTruth(const Query&, bool &isValid) { - ++stats::queries; - // FIXME: We should have stats::queriesFail; - return false; - } - bool computeValue(const Query&, ref<Expr> &result) { - ++stats::queries; - ++stats::queryCounterexamples; - return false; - } - bool computeInitialValues(const Query&, - const std::vector<const Array*> &objects, - std::vector< std::vector<unsigned char> > &values, - bool &hasSolution) { - ++stats::queries; - ++stats::queryCounterexamples; - return false; - } - SolverRunStatus getOperationStatusCode() { - return SOLVER_RUN_STATUS_FAILURE; - } - -}; - -Solver *klee::createDummySolver() { - return new Solver(new DummySolverImpl()); -} - /***/ class STPSolverImpl : public SolverImpl { |