From: Andrew Reynolds Date: Thu, 13 Aug 2020 20:22:59 +0000 (-0500) Subject: Split SmtSolver from SmtEngine (#4880) X-Git-Tag: cvc5-1.0.0~3004 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=02fa1dea5a8335a6bd5a1f3e8718796a9489ac8e;p=cvc5.git Split SmtSolver from SmtEngine (#4880) This class is responsible for maintaining TheoryEngine and PropEngine and implementing the check-sat command. It also has an interface for processing/pushing the current assertions into the PropEngine. This class will be used directly by other extension solvers (for abduction, interpolation, qe, sygus, etc.). --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 77c363317..1f7f68289 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -267,6 +267,8 @@ libcvc4_add_sources( smt/smt_engine_stats.h smt/smt_mode.cpp smt/smt_mode.h + smt/smt_solver.cpp + smt/smt_solver.h smt/smt_statistics_registry.cpp smt/smt_statistics_registry.h smt/term_formula_removal.cpp diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 492f3e105..4da13f108 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -504,7 +504,9 @@ bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions) Debug("smt") << " assertions : " << assertions.size() << endl; // before ppRewrite check if only core theory for BV theory - d_smt.d_theoryEngine->staticInitializeBVOptions(assertions.ref()); + TheoryEngine* te = d_smt.getTheoryEngine(); + Assert(te != nullptr); + te->staticInitializeBVOptions(assertions.ref()); // Theory preprocessing bool doEarlyTheoryPp = !options::arithRewriteEq(); @@ -735,7 +737,7 @@ Node ProcessAssertions::expandDefinitions( { // do not do any theory stuff if expandOnly is true - theory::Theory* t = d_smt.d_theoryEngine->theoryOf(node); + theory::Theory* t = d_smt.getTheoryEngine()->theoryOf(node); Assert(t != NULL); TrustNode trn = t->expandDefinition(n); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7374c8ca9..e709406d8 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -79,7 +79,6 @@ #include "proof/proof_manager.h" #include "proof/theory_proof.h" #include "proof/unsat_core.h" -#include "prop/prop_engine.h" #include "smt/abduction_solver.h" #include "smt/abstract_values.h" #include "smt/assertions.h" @@ -96,6 +95,7 @@ #include "smt/smt_engine_scope.h" #include "smt/smt_engine_state.h" #include "smt/smt_engine_stats.h" +#include "smt/smt_solver.h" #include "smt/term_formula_removal.h" #include "smt/update_ostream.h" #include "smt_util/boolean_simplification.h" @@ -202,8 +202,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_dumpm(new DumpManager(getUserContext())), d_routListener(new ResourceOutListener(*this)), d_snmListener(new SmtNodeManagerListener(*d_dumpm.get())), - d_theoryEngine(nullptr), - d_propEngine(nullptr), + d_smtSolver(nullptr), d_proofManager(nullptr), d_rewriter(new theory::Rewriter()), d_definedFunctions(nullptr), @@ -253,7 +252,10 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_resourceManager->registerListener(d_routListener.get()); // make statistics d_stats.reset(new SmtEngineStatistics()); - + // make the SMT solver + d_smtSolver.reset( + new SmtSolver(*this, *d_state, d_resourceManager.get(), *d_pp, *d_stats)); + // The ProofManager is constructed before any other proof objects such as // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are // initialized in TheoryEngine and PropEngine respectively. @@ -286,6 +288,16 @@ context::UserContext* SmtEngine::getUserContext() } context::Context* SmtEngine::getContext() { return d_state->getContext(); } +TheoryEngine* SmtEngine::getTheoryEngine() +{ + return d_smtSolver->getTheoryEngine(); +} + +prop::PropEngine* SmtEngine::getPropEngine() +{ + return d_smtSolver->getPropEngine(); +} + void SmtEngine::finishInit() { if (d_state->isFullyInited()) @@ -313,37 +325,7 @@ void SmtEngine::finishInit() d_optm->finishInit(d_logic, d_isInternalSubsolver); Trace("smt-debug") << "SmtEngine::finishInit" << std::endl; - // We have mutual dependency here, so we add the prop engine to the theory - // engine later (it is non-essential there) - d_theoryEngine.reset(new TheoryEngine(getContext(), - getUserContext(), - getResourceManager(), - d_pp->getTermFormulaRemover(), - const_cast(d_logic))); - - // Add the theories - for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { - TheoryConstructor::addTheory(getTheoryEngine(), id); - //register with proof engine if applicable -#ifdef CVC4_PROOF - ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine->theoryOf(id)); -#endif - } - - Trace("smt-debug") << "Making decision engine..." << std::endl; - - Trace("smt-debug") << "Making prop engine..." << std::endl; - /* force destruction of referenced PropEngine to enforce that statistics - * are unregistered by the obsolete PropEngine object before registered - * again by the new PropEngine object */ - d_propEngine.reset(nullptr); - d_propEngine.reset(new PropEngine( - getTheoryEngine(), getContext(), getUserContext(), getResourceManager())); - - Trace("smt-debug") << "Setting up theory engine..." << std::endl; - d_theoryEngine->setPropEngine(getPropEngine()); - Trace("smt-debug") << "Finishing init for theory engine..." << std::endl; - d_theoryEngine->finishInit(); + d_smtSolver->finishInit(const_cast(d_logic)); // global push/pop around everything, to ensure proper destruction // of context-dependent data structures @@ -377,14 +359,16 @@ void SmtEngine::finishInit() PROOF( ProofManager::currentPM()->setLogic(d_logic); ); PROOF({ - for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { - ProofManager::currentPM()->getTheoryProofEngine()-> - finishRegisterTheory(d_theoryEngine->theoryOf(id)); - } - }); + TheoryEngine* te = d_smtSolver->getTheoryEngine(); + for (TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) + { + ProofManager::currentPM()->getTheoryProofEngine()->finishRegisterTheory( + te->theoryOf(id)); + } + }); d_pp->finishInit(); - AlwaysAssert(d_propEngine->getAssertionLevel() == 0) + AlwaysAssert(getPropEngine()->getAssertionLevel() == 0) << "The PropEngine has pushed but the SmtEngine " "hasn't finished initializing!"; @@ -398,14 +382,7 @@ void SmtEngine::finishInit() void SmtEngine::shutdown() { d_state->shutdown(); - if (d_propEngine != nullptr) - { - d_propEngine->shutdown(); - } - if (d_theoryEngine != nullptr) - { - d_theoryEngine->shutdown(); - } + d_smtSolver->shutdown(); } SmtEngine::~SmtEngine() @@ -444,8 +421,7 @@ SmtEngine::~SmtEngine() d_exprNames.reset(nullptr); d_dumpm.reset(nullptr); - d_theoryEngine.reset(nullptr); - d_propEngine.reset(nullptr); + d_smtSolver.reset(nullptr); d_stats.reset(nullptr); d_private.reset(nullptr); @@ -925,40 +901,6 @@ bool SmtEngine::isDefinedFunction( Expr func ){ return d_definedFunctions->find(nf) != d_definedFunctions->end(); } -Result SmtEngine::check() { - Assert(d_state->isFullyReady()); - - Trace("smt") << "SmtEngine::check()" << endl; - - const std::string& filename = d_state->getFilename(); - if (d_resourceManager->out()) - { - Result::UnknownExplanation why = d_resourceManager->outOfResources() - ? Result::RESOURCEOUT - : Result::TIMEOUT; - return Result(Result::ENTAILMENT_UNKNOWN, why, filename); - } - d_resourceManager->beginCall(); - - // Make sure the prop layer has all of the assertions - Trace("smt") << "SmtEngine::check(): processing assertions" << endl; - processAssertionsInternal(); - Trace("smt") << "SmtEngine::check(): done processing assertions" << endl; - - TimerStat::CodeTimer solveTimer(d_stats->d_solveTime); - - Chat() << "solving..." << endl; - Trace("smt") << "SmtEngine::check(): running check" << endl; - Result result = d_propEngine->checkSat(); - - d_resourceManager->endCall(); - Trace("limit") << "SmtEngine::check(): cumulative millis " - << d_resourceManager->getTimeUsage() << ", resources " - << d_resourceManager->getResourceUsage() << endl; - - return Result(result, filename); -} - Result SmtEngine::quickCheck() { Assert(d_state->isFullyInited()); Trace("smt") << "SMT quickCheck()" << endl; @@ -993,7 +935,9 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const throw ModalException(ss.str().c_str()); } - TheoryModel* m = d_theoryEngine->getBuiltModel(); + TheoryEngine* te = d_smtSolver->getTheoryEngine(); + Assert(te != nullptr); + TheoryModel* m = te->getBuiltModel(); if (m == nullptr) { @@ -1007,71 +951,46 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const return m; } -void SmtEngine::notifyPushPre() { processAssertionsInternal(); } +void SmtEngine::notifyPushPre() { d_smtSolver->processAssertions(*d_asserts); } + void SmtEngine::notifyPushPost() { TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); - d_propEngine->push(); + Assert(getPropEngine() != nullptr); + getPropEngine()->push(); } + void SmtEngine::notifyPopPre() { TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); - d_propEngine->pop(); + PropEngine* pe = getPropEngine(); + Assert(pe != nullptr); + pe->pop(); } -void SmtEngine::notifyPostSolvePre() { d_propEngine->resetTrail(); } -void SmtEngine::notifyPostSolvePost() { d_theoryEngine->postsolve(); } -void SmtEngine::processAssertionsInternal() +void SmtEngine::notifyPostSolvePre() { - TimerStat::CodeTimer paTimer(d_stats->d_processAssertionsTime); - d_resourceManager->spendResource(ResourceManager::Resource::PreprocessStep); - Assert(d_state->isFullyReady()); - - AssertionPipeline& ap = d_asserts->getAssertionPipeline(); - - if (ap.size() == 0) - { - // nothing to do - return; - } - - // process the assertions with the preprocessor - bool noConflict = d_pp->process(*d_asserts); - - //notify theory engine new preprocessed assertions - d_theoryEngine->notifyPreprocessedAssertions(ap.ref()); - - // Push the formula to decision engine - if (noConflict) - { - Chat() << "pushing to decision engine..." << endl; - d_propEngine->addAssertionsToDecisionEngine(ap); - } - - // end: INVARIANT to maintain: no reordering of assertions or - // introducing new ones - - d_pp->postprocess(*d_asserts); - - // Push the formula to SAT - { - Chat() << "converting to CNF..." << endl; - TimerStat::CodeTimer codeTimer(d_stats->d_cnfConversionTime); - for (const Node& assertion : ap.ref()) - { - Chat() << "+ " << assertion << std::endl; - d_propEngine->assertFormula(assertion); - } - } + PropEngine* pe = getPropEngine(); + Assert(pe != nullptr); + pe->resetTrail(); +} - // clear the current assertions - d_asserts->clearCurrent(); +void SmtEngine::notifyPostSolvePost() +{ + TheoryEngine* te = getTheoryEngine(); + Assert(te != nullptr); + te->postsolve(); } Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore) { Dump("benchmark") << CheckSatCommand(assumption); - return checkSatisfiability(Node::fromExpr(assumption), inUnsatCore, false); + std::vector assump; + if (!assumption.isNull()) + { + assump.push_back(Node::fromExpr(assumption)); + } + return checkSatInternal(assump, inUnsatCore, false); } Result SmtEngine::checkSat(const vector& assumptions, bool inUnsatCore) @@ -1089,17 +1008,17 @@ Result SmtEngine::checkSat(const vector& assumptions, bool inUnsatCore) { assumps.push_back(Node::fromExpr(e)); } - return checkSatisfiability(assumps, inUnsatCore, false); + return checkSatInternal(assumps, inUnsatCore, false); } Result SmtEngine::checkEntailed(const Expr& node, bool inUnsatCore) { Dump("benchmark") << QueryCommand(node, inUnsatCore); - return checkSatisfiability(node.isNull() - ? std::vector() - : std::vector{Node::fromExpr(node)}, - inUnsatCore, - true) + return checkSatInternal(node.isNull() + ? std::vector() + : std::vector{Node::fromExpr(node)}, + inUnsatCore, + true) .asEntailmentResult(); } @@ -1110,22 +1029,12 @@ Result SmtEngine::checkEntailed(const vector& nodes, bool inUnsatCore) { ns.push_back(Node::fromExpr(e)); } - return checkSatisfiability(ns, inUnsatCore, true).asEntailmentResult(); + return checkSatInternal(ns, inUnsatCore, true).asEntailmentResult(); } -Result SmtEngine::checkSatisfiability(const Node& node, - bool inUnsatCore, - bool isEntailmentCheck) -{ - return checkSatisfiability( - node.isNull() ? std::vector() : std::vector{node}, - inUnsatCore, - isEntailmentCheck); -} - -Result SmtEngine::checkSatisfiability(const vector& assumptions, - bool inUnsatCore, - bool isEntailmentCheck) +Result SmtEngine::checkSatInternal(const vector& assumptions, + bool inUnsatCore, + bool isEntailmentCheck) { try { @@ -1135,46 +1044,9 @@ Result SmtEngine::checkSatisfiability(const vector& assumptions, Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "checkEntailed" : "checkSat") << "(" << assumptions << ")" << endl; - // update the state to indicate we are about to run a check-sat - bool hasAssumptions = !assumptions.empty(); - d_state->notifyCheckSat(hasAssumptions); - - // then, initialize the assertions - d_asserts->initializeCheckSat(assumptions, inUnsatCore, isEntailmentCheck); - - // make the check - Result r = check(); - - if ((options::solveRealAsInt() || options::solveIntAsBV() > 0) - && r.asSatisfiabilityResult().isSat() == Result::UNSAT) - { - r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); - } - // flipped if we did a global negation - if (d_asserts->isGlobalNegated()) - { - Trace("smt") << "SmtEngine::process global negate " << r << std::endl; - if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) - { - r = Result(Result::SAT); - } - else if (r.asSatisfiabilityResult().isSat() == Result::SAT) - { - // only if satisfaction complete - if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV)) - { - r = Result(Result::UNSAT); - } - else - { - r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); - } - } - Trace("smt") << "SmtEngine::global negate returned " << r << std::endl; - } - - // notify our state of the check-sat result - d_state->notifyCheckSatResult(hasAssumptions, r); + // check the satisfiability with the solver object + Result r = d_smtSolver->checkSatisfiability( + *d_asserts.get(), assumptions, inUnsatCore, isEntailmentCheck); Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat") << "(" << assumptions << ") => " << r << endl; @@ -1456,7 +1328,7 @@ Result SmtEngine::checkSynth() throw ModalException( "Cannot make check-synth commands when incremental solving is enabled"); } - Expr query; + std::vector query; if (d_private->d_sygusConjectureStale) { // build synthesis conjecture from asserted constraints and declared @@ -1500,10 +1372,10 @@ Result SmtEngine::checkSynth() d_private->d_sygusConjectureStale = false; // TODO (project #7): if incremental, we should push a context and assert - query = body.toExpr(); + query.push_back(body); } - Result r = checkSatisfiability(query, true, false); + Result r = checkSatInternal(query, true, false); // Check that synthesis solutions satisfy the conjecture if (options::checkSynthSol() @@ -1526,7 +1398,7 @@ Node SmtEngine::simplify(const Node& ex) finishInit(); d_state->doPendingPops(); // ensure we've processed assertions - processAssertionsInternal(); + d_smtSolver->processAssertions(*d_asserts); return d_pp->simplify(ex); } @@ -1715,7 +1587,9 @@ Model* SmtEngine::getModel() { // Since model m is being returned to the user, we must ensure that this // model object remains valid with future check-sat calls. Hence, we set // the theory engine into "eager model building" mode. TODO #2648: revisit. - d_theoryEngine->setEagerModelBuilding(); + TheoryEngine* te = getTheoryEngine(); + Assert(te != nullptr); + te->setEagerModelBuilding(); if (options::modelCoresMode() != options::ModelCoresMode::NONE) { @@ -1956,7 +1830,9 @@ void SmtEngine::checkModel(bool hardFailure) { // Check individual theory assertions if (options::debugCheckModels()) { - d_theoryEngine->checkTheoryAssertionsWithModel(hardFailure); + TheoryEngine* te = getTheoryEngine(); + Assert(te != nullptr); + te->checkTheoryAssertionsWithModel(hardFailure); } // Output the model @@ -2161,8 +2037,10 @@ void SmtEngine::checkSynthSolution() NodeManager* nm = NodeManager::currentNM(); Notice() << "SmtEngine::checkSynthSolution(): checking synthesis solution" << endl; std::map> sol_map; + TheoryEngine* te = getTheoryEngine(); + Assert(te != nullptr); /* Get solutions and build auxiliary vectors for substituting */ - if (!d_theoryEngine->getSynthSolutions(sol_map)) + if (!te->getSynthSolutions(sol_map)) { InternalError() << "SmtEngine::checkSynthSolution(): No solution to check!"; return; @@ -2353,11 +2231,9 @@ void SmtEngine::printInstantiations( std::ostream& out ) { out << "% SZS output start Proof for " << d_state->getFilename() << std::endl; } - if( d_theoryEngine ){ - d_theoryEngine->printInstantiations( out ); - }else{ - Assert(false); - } + TheoryEngine* te = getTheoryEngine(); + Assert(te != nullptr); + te->printInstantiations(out); if (options::instFormatMode() == options::InstFormatMode::SZS) { out << "% SZS output end Proof for " << d_state->getFilename() << std::endl; @@ -2367,11 +2243,9 @@ void SmtEngine::printInstantiations( std::ostream& out ) { void SmtEngine::printSynthSolution( std::ostream& out ) { SmtScope smts(this); finishInit(); - if( d_theoryEngine ){ - d_theoryEngine->printSynthSolution( out ); - }else{ - Assert(false); - } + TheoryEngine* te = getTheoryEngine(); + Assert(te != nullptr); + te->printSynthSolution(out); } bool SmtEngine::getSynthSolutions(std::map& sol_map) @@ -2379,9 +2253,10 @@ bool SmtEngine::getSynthSolutions(std::map& sol_map) SmtScope smts(this); finishInit(); std::map> sol_mapn; - Assert(d_theoryEngine != nullptr); + TheoryEngine* te = getTheoryEngine(); + Assert(te != nullptr); // fail if the theory engine does not have synthesis solutions - if (!d_theoryEngine->getSynthSolutions(sol_mapn)) + if (!te->getSynthSolutions(sol_mapn)) { return false; } @@ -2413,7 +2288,10 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) TypeNode t = NodeManager::currentNM()->booleanType(); Node n_attr = NodeManager::currentNM()->mkSkolem("qe", t, "Auxiliary variable for qe attr."); std::vector< Node > node_values; - d_theoryEngine->setUserAttribute( doFull ? "quant-elim" : "quant-elim-partial", n_attr, node_values, ""); + TheoryEngine* te = getTheoryEngine(); + Assert(te != nullptr); + te->setUserAttribute( + doFull ? "quant-elim" : "quant-elim-partial", n_attr, node_values, ""); n_attr = NodeManager::currentNM()->mkNode(kind::INST_ATTRIBUTE, n_attr); n_attr = NodeManager::currentNM()->mkNode(kind::INST_PATTERN_LIST, n_attr); std::vector< Node > e_children; @@ -2424,7 +2302,7 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) Node nn_e = NodeManager::currentNM()->mkNode( kind::EXISTS, e_children ); Trace("smt-qe-debug") << "Query for quantifier elimination : " << nn_e << std::endl; Assert(nn_e.getNumChildren() == 3); - Result r = checkSatisfiability(nn_e.toExpr(), true, true); + Result r = checkSatInternal(std::vector{nn_e}, true, true); Trace("smt-qe") << "Query returned " << r << std::endl; if(r.asSatisfiabilityResult().isSat() != Result::UNSAT ) { if( r.asSatisfiabilityResult().isSat() != Result::SAT && doFull ){ @@ -2435,7 +2313,7 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) return e; } std::vector< Node > inst_qs; - d_theoryEngine->getInstantiatedQuantifiedFormulas( inst_qs ); + te->getInstantiatedQuantifiedFormulas(inst_qs); Assert(inst_qs.size() <= 1); Node ret_n; if( inst_qs.size()==1 ){ @@ -2443,7 +2321,7 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) //Node top_q = Rewriter::rewrite( nn_e ).negate(); Assert(top_q.getKind() == kind::FORALL); Trace("smt-qe") << "Get qe for " << top_q << std::endl; - ret_n = d_theoryEngine->getInstantiatedConjunction( top_q ); + ret_n = te->getInstantiatedConjunction(top_q); Trace("smt-qe") << "Returned : " << ret_n << std::endl; if (n_e.getKind() == kind::EXISTS) { @@ -2495,45 +2373,43 @@ bool SmtEngine::getAbduct(const Node& conj, Node& abd) void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ) { SmtScope smts(this); - if( d_theoryEngine ){ - std::vector< Node > qs_n; - d_theoryEngine->getInstantiatedQuantifiedFormulas( qs_n ); - for( unsigned i=0; i qs_n; + te->getInstantiatedQuantifiedFormulas(qs_n); + for (std::size_t i = 0, n = qs_n.size(); i < n; i++) + { + qs.push_back(qs_n[i].toExpr()); } } void SmtEngine::getInstantiations( Expr q, std::vector< Expr >& insts ) { SmtScope smts(this); - if( d_theoryEngine ){ - std::vector< Node > insts_n; - d_theoryEngine->getInstantiations( Node::fromExpr( q ), insts_n ); - for( unsigned i=0; i insts_n; + te->getInstantiations(Node::fromExpr(q), insts_n); + for (std::size_t i = 0, n = insts_n.size(); i < n; i++) + { + insts.push_back(insts_n[i].toExpr()); } } void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs ) { SmtScope smts(this); Assert(options::trackInstLemmas()); - if( d_theoryEngine ){ - std::vector< std::vector< Node > > tvecs_n; - d_theoryEngine->getInstantiationTermVectors( Node::fromExpr( q ), tvecs_n ); - for( unsigned i=0; i tvec; - for( unsigned j=0; j> tvecs_n; + te->getInstantiationTermVectors(Node::fromExpr(q), tvecs_n); + for (std::size_t i = 0, n = tvecs_n.size(); i < n; i++) + { + std::vector tvec; + for (std::size_t j = 0, m = tvecs_n[i].size(); j < m; j++) + { + tvec.push_back(tvecs_n[i][j].toExpr()); } - }else{ - Assert(false); + tvecs.push_back(tvec); } } @@ -2568,7 +2444,7 @@ void SmtEngine::push() finishInit(); d_state->doPendingPops(); Trace("smt") << "SMT push()" << endl; - processAssertionsInternal(); + d_smtSolver->processAssertions(*d_asserts); if(Dump.isOn("benchmark")) { Dump("benchmark") << PushCommand(); } @@ -2635,14 +2511,7 @@ void SmtEngine::resetAssertions() // push the state to maintain global context around everything d_state->setup(); - /* Create new PropEngine. - * First force destruction of referenced PropEngine to enforce that - * statistics are unregistered by the obsolete PropEngine object before - * registered again by the new PropEngine object */ - d_propEngine.reset(nullptr); - d_propEngine.reset(new PropEngine( - getTheoryEngine(), getContext(), getUserContext(), getResourceManager())); - d_theoryEngine->setPropEngine(getPropEngine()); + d_smtSolver->resetAssertions(); } void SmtEngine::interrupt() @@ -2651,8 +2520,7 @@ void SmtEngine::interrupt() { return; } - d_propEngine->interrupt(); - d_theoryEngine->interrupt(); + d_smtSolver->interrupt(); } void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) { @@ -2707,7 +2575,9 @@ void SmtEngine::setUserAttribute(const std::string& attr, { node_values.push_back( expr_values[i].getNode() ); } - d_theoryEngine->setUserAttribute(attr, expr.getNode(), node_values, str_value); + TheoryEngine* te = getTheoryEngine(); + Assert(te != nullptr); + te->setUserAttribute(attr, expr.getNode(), node_values, str_value); } void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 4df57accb..1c71e371e 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -103,6 +103,7 @@ class SmtNodeManagerListener; class OptionsManager; class Preprocessor; /** Subsolvers */ +class SmtSolver; class AbductionSolver; /** * Representation of a defined function. We keep these around in @@ -149,6 +150,7 @@ class CVC4_PUBLIC SmtEngine friend class ::CVC4::smt::SmtEngineState; friend class ::CVC4::smt::SmtScope; friend class ::CVC4::smt::ProcessAssertions; + friend class ::CVC4::smt::SmtSolver; friend ProofManager* ::CVC4::smt::currentProofManager(); friend class ::CVC4::LogicRequest; friend class ::CVC4::theory::TheoryModel; @@ -908,10 +910,10 @@ class CVC4_PUBLIC SmtEngine context::Context* getContext(); /** Get a pointer to the TheoryEngine owned by this SmtEngine. */ - TheoryEngine* getTheoryEngine() { return d_theoryEngine.get(); } + TheoryEngine* getTheoryEngine(); /** Get a pointer to the PropEngine owned by this SmtEngine. */ - prop::PropEngine* getPropEngine() { return d_propEngine.get(); } + prop::PropEngine* getPropEngine(); /** Get a pointer to the ProofManager owned by this SmtEngine. */ ProofManager* getProofManager() { return d_proofManager.get(); }; @@ -988,12 +990,6 @@ class CVC4_PUBLIC SmtEngine */ void shutdown(); - /** - * Full check of consistency in current context. Returns true iff - * consistent. - */ - Result check(); - /** * Quick check of consistency in current context: calls * processAssertionList() then look for inconsistency (based only on @@ -1049,14 +1045,6 @@ class CVC4_PUBLIC SmtEngine */ void setLogicInternal(); - /** - * Process the assertions that have been asserted. This moves the set of - * assertions that have been buffered into the smt::Assertions object, - * preprocesses them, pushes them into the SMT solver, and clears the - * buffer. - */ - void processAssertionsInternal(); - /** * Add to Model command. This is used for recording a command * that should be reported during a get-model call. @@ -1066,13 +1054,12 @@ class CVC4_PUBLIC SmtEngine bool userVisible = true, const char* dumpTag = "declarations"); - /* Check satisfiability (used to check satisfiability and entailment). */ - Result checkSatisfiability(const Node& assumption, - bool inUnsatCore, - bool isEntailmentCheck); - Result checkSatisfiability(const std::vector& assumptions, - bool inUnsatCore, - bool isEntailmentCheck); + /* + * Check satisfiability (used to check satisfiability and entailment). + */ + Result checkSatInternal(const std::vector& assumptions, + bool inUnsatCore, + bool isEntailmentCheck); /** * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is @@ -1125,10 +1112,8 @@ class CVC4_PUBLIC SmtEngine /** Node manager listener */ std::unique_ptr d_snmListener; - /** The theory engine */ - std::unique_ptr d_theoryEngine; - /** The propositional engine */ - std::unique_ptr d_propEngine; + /** The SMT solver */ + std::unique_ptr d_smtSolver; /** The proof manager */ std::unique_ptr d_proofManager; diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp new file mode 100644 index 000000000..e0837c7cf --- /dev/null +++ b/src/smt/smt_solver.cpp @@ -0,0 +1,257 @@ +/********************* */ +/*! \file smt_solver.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The solver for SMT queries in an SmtEngine. + **/ + +#include "smt/smt_solver.h" + +#include "proof/theory_proof.h" +#include "prop/prop_engine.h" +#include "smt/assertions.h" +#include "smt/preprocessor.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_state.h" +#include "theory/theory_engine.h" +#include "theory/theory_traits.h" + +namespace CVC4 { +namespace smt { + +SmtSolver::SmtSolver(SmtEngine& smt, + SmtEngineState& state, + ResourceManager* rm, + Preprocessor& pp, + SmtEngineStatistics& stats) + : d_smt(smt), + d_state(state), + d_rm(rm), + d_pp(pp), + d_stats(stats), + d_theoryEngine(nullptr), + d_propEngine(nullptr) +{ +} + +SmtSolver::~SmtSolver() {} + +void SmtSolver::finishInit(const LogicInfo& logicInfo) +{ + // We have mutual dependency here, so we add the prop engine to the theory + // engine later (it is non-essential there) + d_theoryEngine.reset(new TheoryEngine(d_smt.getContext(), + d_smt.getUserContext(), + d_rm, + d_pp.getTermFormulaRemover(), + logicInfo)); + + // Add the theories + for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; + ++id) + { + theory::TheoryConstructor::addTheory(d_theoryEngine.get(), id); + // register with proof engine if applicable +#ifdef CVC4_PROOF + ProofManager::currentPM()->getTheoryProofEngine()->registerTheory( + d_theoryEngine->theoryOf(id)); +#endif + } + + Trace("smt-debug") << "Making prop engine..." << std::endl; + /* force destruction of referenced PropEngine to enforce that statistics + * are unregistered by the obsolete PropEngine object before registered + * again by the new PropEngine object */ + d_propEngine.reset(nullptr); + d_propEngine.reset(new PropEngine( + d_theoryEngine.get(), d_smt.getContext(), d_smt.getUserContext(), d_rm)); + + Trace("smt-debug") << "Setting up theory engine..." << std::endl; + d_theoryEngine->setPropEngine(getPropEngine()); + Trace("smt-debug") << "Finishing init for theory engine..." << std::endl; + d_theoryEngine->finishInit(); +} + +void SmtSolver::resetAssertions() +{ + /* Create new PropEngine. + * First force destruction of referenced PropEngine to enforce that + * statistics are unregistered by the obsolete PropEngine object before + * registered again by the new PropEngine object */ + d_propEngine.reset(nullptr); + d_propEngine.reset(new PropEngine( + d_theoryEngine.get(), d_smt.getContext(), d_smt.getUserContext(), d_rm)); + d_theoryEngine->setPropEngine(getPropEngine()); + // Notice that we do not reset TheoryEngine, nor does it require calling + // finishInit again. In particular, TheoryEngine::finishInit does not + // depend on knowing the associated PropEngine. +} + +void SmtSolver::interrupt() +{ + if (d_propEngine != nullptr) + { + d_propEngine->interrupt(); + } + if (d_theoryEngine != nullptr) + { + d_theoryEngine->interrupt(); + } +} + +void SmtSolver::shutdown() +{ + if (d_propEngine != nullptr) + { + d_propEngine->shutdown(); + } + if (d_theoryEngine != nullptr) + { + d_theoryEngine->shutdown(); + } +} + +Result SmtSolver::checkSatisfiability(Assertions& as, + const std::vector& assumptions, + bool inUnsatCore, + bool isEntailmentCheck) +{ + // update the state to indicate we are about to run a check-sat + bool hasAssumptions = !assumptions.empty(); + d_state.notifyCheckSat(hasAssumptions); + + // then, initialize the assertions + as.initializeCheckSat(assumptions, inUnsatCore, isEntailmentCheck); + + // make the check + Assert(d_smt.isFullyInited()); + + Trace("smt") << "SmtSolver::check()" << endl; + + const std::string& filename = d_state.getFilename(); + if (d_rm->out()) + { + Result::UnknownExplanation why = + d_rm->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT; + return Result(Result::ENTAILMENT_UNKNOWN, why, filename); + } + d_rm->beginCall(); + + // Make sure the prop layer has all of the assertions + Trace("smt") << "SmtSolver::check(): processing assertions" << endl; + processAssertions(as); + Trace("smt") << "SmtSolver::check(): done processing assertions" << endl; + + TimerStat::CodeTimer solveTimer(d_stats.d_solveTime); + + Chat() << "solving..." << endl; + Trace("smt") << "SmtSolver::check(): running check" << endl; + Result result = d_propEngine->checkSat(); + + d_rm->endCall(); + Trace("limit") << "SmtSolver::check(): cumulative millis " + << d_rm->getTimeUsage() << ", resources " + << d_rm->getResourceUsage() << endl; + + if ((options::solveRealAsInt() || options::solveIntAsBV() > 0) + && result.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); + } + // flipped if we did a global negation + if (as.isGlobalNegated()) + { + Trace("smt") << "SmtSolver::process global negate " << result << std::endl; + if (result.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + result = Result(Result::SAT); + } + else if (result.asSatisfiabilityResult().isSat() == Result::SAT) + { + // Only can answer unsat if the theory is satisfaction complete. This + // includes linear arithmetic and bitvectors, which are the primary + // targets for the global negate option. Other logics are possible here + // but not considered. + LogicInfo logic = d_smt.getLogicInfo(); + if ((logic.isPure(theory::THEORY_ARITH) && logic.isLinear()) || + logic.isPure(theory::THEORY_BV)) + { + result = Result(Result::UNSAT); + } + else + { + result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); + } + } + Trace("smt") << "SmtSolver::global negate returned " << result << std::endl; + } + + // set the filename on the result + Result r = Result(result, filename); + + // notify our state of the check-sat result + d_state.notifyCheckSatResult(hasAssumptions, r); + + return r; +} + +void SmtSolver::processAssertions(Assertions& as) +{ + TimerStat::CodeTimer paTimer(d_stats.d_processAssertionsTime); + d_rm->spendResource(ResourceManager::Resource::PreprocessStep); + Assert(d_state.isFullyReady()); + + preprocessing::AssertionPipeline& ap = as.getAssertionPipeline(); + + if (ap.size() == 0) + { + // nothing to do + return; + } + + // process the assertions with the preprocessor + bool noConflict = d_pp.process(as); + + // notify theory engine new preprocessed assertions + d_theoryEngine->notifyPreprocessedAssertions(ap.ref()); + + // Push the formula to decision engine + if (noConflict) + { + Chat() << "pushing to decision engine..." << endl; + d_propEngine->addAssertionsToDecisionEngine(ap); + } + + // end: INVARIANT to maintain: no reordering of assertions or + // introducing new ones + + d_pp.postprocess(as); + + // Push the formula to SAT + { + Chat() << "converting to CNF..." << endl; + TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime); + for (const Node& assertion : ap.ref()) + { + Chat() << "+ " << assertion << std::endl; + d_propEngine->assertFormula(assertion); + } + } + + // clear the current assertions + as.clearCurrent(); +} + +TheoryEngine* SmtSolver::getTheoryEngine() { return d_theoryEngine.get(); } + +prop::PropEngine* SmtSolver::getPropEngine() { return d_propEngine.get(); } + +} // namespace smt +} // namespace CVC4 diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h new file mode 100644 index 000000000..8d0644800 --- /dev/null +++ b/src/smt/smt_solver.h @@ -0,0 +1,137 @@ +/********************* */ +/*! \file smt_solver.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The solver for SMT queries in an SmtEngine. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__SMT__SMT_SOLVER_H +#define CVC4__SMT__SMT_SOLVER_H + +#include + +#include "expr/node.h" +#include "theory/logic_info.h" +#include "util/result.h" + +namespace CVC4 { + +class SmtEngine; +class TheoryEngine; +class ResourceManager; + +namespace prop { +class PropEngine; +} + +namespace smt { + +class Assertions; +class SmtEngineState; +class Preprocessor; +class SmtEngineStatistics; + +/** + * A solver for SMT queries. + * + * This class manages the initialization of the theory engine and propositional + * engines and implements the method for checking satisfiability of the current + * set of assertions. + * + * Notice that this class is only conceptually responsible for running + * check-sat commands and an interface for sending formulas to the underlying + * classes. It does not implement any query techniques beyond getting the result + * (unsat/sat/unknown) of check-sat calls. More detailed information (e.g. + * models) can be queries using other classes that examine the state of the + * TheoryEngine directly, which can be accessed via getTheoryEngine. + */ +class SmtSolver +{ + public: + SmtSolver(SmtEngine& smt, + SmtEngineState& state, + ResourceManager* rm, + Preprocessor& pp, + SmtEngineStatistics& stats); + ~SmtSolver(); + /** + * Create theory engine, prop engine based on the logic info. + */ + void finishInit(const LogicInfo& logicInfo); + /** Reset all assertions, global declarations, etc. */ + void resetAssertions(); + /** + * Interrupt a running query. This can be called from another thread + * or from a signal handler. Throws a ModalException if the SmtSolver + * isn't currently in a query. + */ + void interrupt(); + /** + * This is called by the destructor of SmtEngine, just before destroying the + * PropEngine, TheoryEngine, and DecisionEngine (in that order). It + * is important because there are destruction ordering issues + * between PropEngine and Theory. + */ + void shutdown(); + /** + * Check satisfiability (used to check satisfiability and entailment) + * in SmtEngine. This is done via adding assumptions (when necessary) to + * assertions as, preprocessing and pushing assertions into the prop engine + * of this class, and checking for satisfiability via the prop engine. + * + * @param as The object managing the assertions in SmtEngine. This class + * maintains a current set of (unprocessed) assertions which are pushed + * into the internal members of this class (TheoryEngine and PropEngine) + * during this call. + * @param assumptions The assumptions for this check-sat call, which are + * temporary assertions. + * @param inUnsatCore Whether assumptions are in the unsat core. + * @param isEntailmentCheck Whether this is an entailment check (assumptions + * are negated in this case). + */ + Result checkSatisfiability(Assertions& as, + const std::vector& assumptions, + bool inUnsatCore, + bool isEntailmentCheck); + /** + * Process the assertions that have been asserted in as. This moves the set of + * assertions that have been buffered into as, preprocesses them, pushes them + * into the SMT solver, and clears the buffer. + */ + void processAssertions(Assertions& as); + //------------------------------------------ access methods + /** Get a pointer to the TheoryEngine owned by this solver. */ + TheoryEngine* getTheoryEngine(); + /** Get a pointer to the PropEngine owned by this solver. */ + prop::PropEngine* getPropEngine(); + //------------------------------------------ end access methods + private: + /** Reference to the parent SMT engine */ + SmtEngine& d_smt; + /** Reference to the state of the SmtEngine */ + SmtEngineState& d_state; + /** Pointer to a resource manager (owned by SmtEngine) */ + ResourceManager* d_rm; + /** Reference to the preprocessor of SmtEngine */ + Preprocessor& d_pp; + /** Reference to the statistics of SmtEngine */ + SmtEngineStatistics& d_stats; + /** The theory engine */ + std::unique_ptr d_theoryEngine; + /** The propositional engine */ + std::unique_ptr d_propEngine; +}; + +} // namespace smt +} // namespace CVC4 + +#endif /* CVC4__SMT__SMT_SOLVER_H */ diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index dd0be5550..03b1922bd 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -114,10 +114,10 @@ public: // the following call, which constructs its underlying theory engine. d_smt->finishInit(); - d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH]->setOutputChannel( + d_smt->getTheoryEngine()->d_theoryTable[THEORY_ARITH]->setOutputChannel( d_outputChannel); d_arith = static_cast( - d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH]); + d_smt->getTheoryEngine()->d_theoryTable[THEORY_ARITH]); preregistered = new std::set(); diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index ff1ce31b6..582a031c9 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -78,7 +78,7 @@ public: d_smt->finishInit(); EagerBitblaster* bb = new EagerBitblaster( dynamic_cast( - d_smt->d_theoryEngine->d_theoryTable[THEORY_BV]), + d_smt->getTheoryEngine()->d_theoryTable[THEORY_BV]), d_smt->getContext()); Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(16)); Node y = d_nm->mkVar("y", d_nm->mkBitVectorType(16)); diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index 5da5a7c62..9693000a3 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -182,10 +182,10 @@ class TheoryBlack : public CxxTest::TestSuite { // the following call, which constructs its underlying theory engine. d_smt->finishInit(); // guard against duplicate statistics assertion errors - delete d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN]; - delete d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN]; - d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN] = NULL; - d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN] = NULL; + delete d_smt->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN]; + delete d_smt->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN]; + d_smt->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN] = NULL; + d_smt->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN] = NULL; d_dummy = new DummyTheory(d_ctxt, d_uctxt,