From: Andrew Reynolds Date: Wed, 20 Apr 2022 22:59:35 +0000 (-0500) Subject: Add utilities in preparation for deep restarts (#8642) X-Git-Tag: cvc5-1.0.1~236 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fec80c0648b9f81b2d24dec2b1a250636bfcb4f7;p=cvc5.git Add utilities in preparation for deep restarts (#8642) --- diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index eebd54492..fdbcf9667 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -711,5 +711,10 @@ std::vector PropEngine::getLearnedZeroLevelLiterals( return d_theoryProxy->getLearnedZeroLevelLiterals(ltype); } +std::vector PropEngine::getLearnedZeroLevelLiteralsForRestart() const +{ + return d_theoryProxy->getLearnedZeroLevelLiteralsForRestart(); +} + } // namespace prop } // namespace cvc5::internal diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index be4306934..5afb38716 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -25,6 +25,7 @@ #include "expr/node.h" #include "proof/proof.h" #include "proof/trust_node.h" +#include "prop/learned_db.h" #include "prop/skolem_def_manager.h" #include "smt/env_obj.h" #include "theory/output_channel.h" @@ -313,6 +314,9 @@ class PropEngine : protected EnvObj std::vector getLearnedZeroLevelLiterals( modes::LearnedLitType ltype) const; + /** Get the zero-level assertions that should be used on deep restart */ + std::vector getLearnedZeroLevelLiteralsForRestart() const; + private: /** Dump out the satisfying assignment (after SAT result) */ void printSatisfyingAssignment(); diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index abd37695c..d6c6f6a56 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -50,7 +50,8 @@ TheoryProxy::TheoryProxy(Env& env, d_queue(context()), d_tpp(env, *theoryEngine), d_skdm(skdm), - d_zll(nullptr) + d_zll(nullptr), + d_stopSearch(false, userContext()) { bool trackZeroLevel = isOutputOn(OutputTag::LEARNED_LITS) || options().smt.produceLearnedLiterals; @@ -70,6 +71,7 @@ void TheoryProxy::presolve() { d_decisionEngine->presolve(); d_theoryEngine->presolve(); + d_stopSearch = false; } void TheoryProxy::notifyTopLevelSubstitution(const Node& lhs, @@ -136,6 +138,10 @@ void TheoryProxy::theoryCheck(theory::Theory::Effort effort) { d_queue.pop(); if (d_zll != nullptr) { + if (d_stopSearch.get()) + { + break; + } int32_t alevel = d_propEngine->getDecisionLevel(assertion); d_zll->notifyAsserted(assertion, alevel); } @@ -155,7 +161,10 @@ void TheoryProxy::theoryCheck(theory::Theory::Effort effort) { d_decisionEngine->notifyActiveSkolemDefs(activeSkolemDefs); } } - d_theoryEngine->check(effort); + if (!d_stopSearch.get()) + { + d_theoryEngine->check(effort); + } } void TheoryProxy::theoryPropagate(std::vector& output) { @@ -235,6 +244,11 @@ SatLiteral TheoryProxy::getNextTheoryDecisionRequest() { SatLiteral TheoryProxy::getNextDecisionEngineRequest(bool &stopSearch) { Assert(d_decisionEngine != NULL); Assert(stopSearch != true); + if (d_stopSearch.get()) + { + stopSearch = true; + return undefSatLiteral; + } SatLiteral ret = d_decisionEngine->getNext(stopSearch); if(stopSearch) { Trace("decision") << " *** Decision Engine stopped search *** " << std::endl; @@ -243,12 +257,16 @@ SatLiteral TheoryProxy::getNextDecisionEngineRequest(bool &stopSearch) { } bool TheoryProxy::theoryNeedCheck() const { + if (d_stopSearch.get()) + { + return false; + } return d_theoryEngine->needCheck(); } bool TheoryProxy::isIncomplete() const { - return d_theoryEngine->isIncomplete(); + return d_stopSearch.get() || d_theoryEngine->isIncomplete(); } TNode TheoryProxy::getNode(SatLiteral lit) { @@ -268,7 +286,7 @@ void TheoryProxy::spendResource(Resource r) bool TheoryProxy::isDecisionRelevant(SatVariable var) { return true; } bool TheoryProxy::isDecisionEngineDone() { - return d_decisionEngine->isDone(); + return d_decisionEngine->isDone() || d_stopSearch.get(); } SatValue TheoryProxy::getDecisionPolarity(SatVariable var) { @@ -321,5 +339,14 @@ std::vector TheoryProxy::getLearnedZeroLevelLiterals( return {}; } +std::vector TheoryProxy::getLearnedZeroLevelLiteralsForRestart() const +{ + if (d_zll != nullptr) + { + return d_zll->getLearnedZeroLevelLiteralsForRestart(); + } + return {}; +} + } // namespace prop } // namespace cvc5::internal diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 8d0270fa4..a3b824799 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -179,6 +179,8 @@ class TheoryProxy : protected EnvObj, public Registrar /** Get the zero-level assertions */ std::vector getLearnedZeroLevelLiterals( modes::LearnedLitType ltype) const; + /** Get the zero-level assertions that should be used on deep restart */ + std::vector getLearnedZeroLevelLiteralsForRestart() const; private: /** The prop engine we are using. */ @@ -217,6 +219,8 @@ class TheoryProxy : protected EnvObj, public Registrar /** The zero level learner */ std::unique_ptr d_zll; + /** Whether we have been requested to stop the search */ + context::CDO d_stopSearch; }; /* class TheoryProxy */ } // namespace prop diff --git a/src/prop/zero_level_learner.cpp b/src/prop/zero_level_learner.cpp index a98136ca8..32eb90059 100644 --- a/src/prop/zero_level_learner.cpp +++ b/src/prop/zero_level_learner.cpp @@ -265,6 +265,30 @@ std::vector ZeroLevelLearner::getLearnedZeroLevelLiterals( return ret; } +std::vector ZeroLevelLearner::getLearnedZeroLevelLiteralsForRestart() + const +{ + std::vector ret; + for (modes::LearnedLitType ltype : d_learnedTypes) + { + std::vector rett = getLearnedZeroLevelLiterals(ltype); + ret.insert(ret.end(), rett.begin(), rett.end()); + } + return ret; +} + +bool ZeroLevelLearner::hasLearnedLiteralForRestart() const +{ + for (modes::LearnedLitType ltype : d_learnedTypes) + { + if (d_ldb.getNumLearnedLiterals(ltype) > 0) + { + return true; + } + } + return false; +} + bool ZeroLevelLearner::isLearnable(modes::LearnedLitType ltype) const { return d_learnedTypes.find(ltype) != d_learnedTypes.end(); diff --git a/src/prop/zero_level_learner.h b/src/prop/zero_level_learner.h index e61d41584..16b5e7e3c 100644 --- a/src/prop/zero_level_learner.h +++ b/src/prop/zero_level_learner.h @@ -64,6 +64,8 @@ class ZeroLevelLearner : protected EnvObj /** Get the zero-level assertions */ std::vector getLearnedZeroLevelLiterals( modes::LearnedLitType ltype) const; + /** Get the zero-level assertions that should be used on deep restart */ + std::vector getLearnedZeroLevelLiteralsForRestart() const; private: static void getAtoms(TNode a, @@ -77,6 +79,8 @@ class ZeroLevelLearner : protected EnvObj bool isLearnable(modes::LearnedLitType ltype) const; /** get solved */ bool getSolved(const Node& lit, Subs& subs); + /** has learned literal */ + bool hasLearnedLiteralForRestart() const; /** The theory engine we are using */ TheoryEngine* d_theoryEngine;