From: Andrew Reynolds Date: Thu, 7 Apr 2022 13:07:39 +0000 (-0500) Subject: Eliminate SmtSolver dependency on SolverEngineState (#8581) X-Git-Tag: cvc5-1.0.1~288 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e51c4d62523d160058f0f06cb15fef75771f3ceb;p=cvc5.git Eliminate SmtSolver dependency on SolverEngineState (#8581) This is in preparation for making SmtSolver able to be deep reset (reconstructed) within in a SolverEngine instance. --- diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp index 4b9fb40ce..fe68e418c 100644 --- a/src/proof/proof_checker.cpp +++ b/src/proof/proof_checker.cpp @@ -93,6 +93,12 @@ ProofChecker::ProofChecker(bool eagerCheck, { } +void ProofChecker::reset() +{ + d_checker.clear(); + d_plevel.clear(); +} + Node ProofChecker::check(ProofNode* pn, Node expected) { return check(pn->getRule(), pn->getChildren(), pn->getArguments(), expected); diff --git a/src/proof/proof_checker.h b/src/proof/proof_checker.h index 2c69588ab..652ec0cf1 100644 --- a/src/proof/proof_checker.h +++ b/src/proof/proof_checker.h @@ -109,6 +109,8 @@ class ProofChecker uint32_t pclevel = 0, rewriter::RewriteDb* rdb = nullptr); ~ProofChecker() {} + /** Reset, which clears the rule checkers */ + void reset(); /** * Return the formula that is proven by proof node pn, or null if pn is not * well-formed. If expected is non-null, then we return null if pn does not diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index f1670cc92..bd23ff353 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -15,6 +15,7 @@ #include "smt/smt_solver.h" +#include "options/base_options.h" #include "options/main_options.h" #include "options/smt_options.h" #include "prop/prop_engine.h" @@ -35,11 +36,9 @@ namespace cvc5::internal { namespace smt { SmtSolver::SmtSolver(Env& env, - SolverEngineState& state, AbstractValues& abs, SolverEngineStatistics& stats) - : d_env(env), - d_state(state), + : EnvObj(env), d_pp(env, abs, stats), d_stats(stats), d_theoryEngine(nullptr), @@ -65,6 +64,9 @@ void SmtSolver::finishInit() ProofNodeManager* pnm = d_env.getProofNodeManager(); if (pnm) { + // reset the rule checkers + pnm->getChecker()->reset(); + // add rule checkers from the theory engine d_theoryEngine->initializeProofChecker(pnm->getChecker()); } Trace("smt-debug") << "Making prop engine..." << std::endl; @@ -116,13 +118,8 @@ Result SmtSolver::checkSatisfiability(Assertions& as, const std::vector& assumptions) { Result result; - - bool hasAssumptions = !assumptions.empty(); - try { - // update the state to indicate we are about to run a check-sat - d_state.notifyCheckSat(hasAssumptions); // then, initialize the assertions as.initializeCheckSat(assumptions); @@ -208,19 +205,13 @@ Result SmtSolver::checkSatisfiability(Assertions& as, // set the filename on the result const std::string& filename = d_env.getOptions().driver.filename; - result = Result(result, filename); - - // notify our state of the check-sat result - d_state.notifyCheckSatResult(hasAssumptions, result); - - return result; + return Result(result, filename); } void SmtSolver::processAssertions(Assertions& as) { TimerStat::CodeTimer paTimer(d_stats.d_processAssertionsTime); d_env.getResourceManager()->spendResource(Resource::PreprocessStep); - Assert(d_state.isFullyReady()); preprocessing::AssertionPipeline& ap = as.getAssertionPipeline(); diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index 429d7ee21..78d11ef2a 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -21,6 +21,8 @@ #include #include "expr/node.h" +#include "smt/assertions.h" +#include "smt/env_obj.h" #include "smt/preprocessor.h" #include "theory/logic_info.h" #include "util/result.h" @@ -43,7 +45,6 @@ class QuantifiersEngine; namespace smt { -class Assertions; class SolverEngineState; struct SolverEngineStatistics; @@ -61,11 +62,10 @@ struct SolverEngineStatistics; * models) can be queries using other classes that examine the state of the * TheoryEngine directly, which can be accessed via getTheoryEngine. */ -class SmtSolver +class SmtSolver : protected EnvObj { public: SmtSolver(Env& env, - SolverEngineState& state, AbstractValues& abs, SolverEngineStatistics& stats); ~SmtSolver(); @@ -114,10 +114,6 @@ class SmtSolver //------------------------------------------ end access methods private: - /** Reference to the environment */ - Env& d_env; - /** Reference to the state of the SolverEngine */ - SolverEngineState& d_state; /** The preprocessor of this SMT solver */ Preprocessor d_pp; /** Reference to the statistics of SolverEngine */ diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 46b30206b..5ae8bd08f 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -117,7 +117,7 @@ SolverEngine::SolverEngine(NodeManager* nm, const Options* optr) // make statistics d_stats.reset(new SolverEngineStatistics()); // make the SMT solver - d_smtSolver.reset(new SmtSolver(*d_env, *d_state, *d_absValues, *d_stats)); + d_smtSolver.reset(new SmtSolver(*d_env, *d_absValues, *d_stats)); // make the SyGuS solver d_sygusSolver.reset(new SygusSolver(*d_env.get(), *d_smtSolver)); // make the quantifier elimination solver @@ -750,17 +750,24 @@ Result SolverEngine::checkSat(const std::vector& assumptions) Result SolverEngine::checkSatInternal(const std::vector& assumptions) { - Result r; - SolverEngineScope smts(this); finishInit(); Trace("smt") << "SolverEngine::checkSat(" << assumptions << ")" << endl; + // update the state to indicate we are about to run a check-sat + bool hasAssumptions = !assumptions.empty(); + d_state->notifyCheckSat(hasAssumptions); + + // state should be fully ready now + Assert(d_state->isFullyReady()); + // check the satisfiability with the solver object - r = d_smtSolver->checkSatisfiability(*d_asserts.get(), assumptions); + Result r = d_smtSolver->checkSatisfiability(*d_asserts.get(), assumptions); Trace("smt") << "SolverEngine::checkSat(" << assumptions << ") => " << r << endl; + // notify our state of the check-sat result + d_state->notifyCheckSatResult(hasAssumptions, r); // Check that SAT results generate a model correctly. if (d_env->getOptions().smt.checkModels)