From: Andrew Reynolds Date: Fri, 9 Jul 2021 16:50:51 +0000 (-0500) Subject: Implement stop-only for new justification heuristic (#6847) X-Git-Tag: cvc5-1.0.0~1512 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ff91290122d478dc637fb3e9ff4fe4c0ead5bd32;p=cvc5.git Implement stop-only for new justification heuristic (#6847) This also refactors decision engine so that we use inheritance instead of a dummy flag + members to determine which implementation to use. --- diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index d439f33a6..5b65951a6 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -22,86 +22,37 @@ namespace cvc5 { namespace decision { -DecisionEngine::DecisionEngine(context::Context* c, - context::UserContext* u, - prop::SkolemDefManager* skdm, - ResourceManager* rm) - : d_decEngineOld(new DecisionEngineOld(c, u)), - d_jstrat(new JustificationStrategy(c, u, skdm)), +DecisionEngine::DecisionEngine(context::Context* c, ResourceManager* rm) + : d_context(c), d_resourceManager(rm), - d_useOld(options::decisionMode() != options::DecisionMode::JUSTIFICATION) + d_cnfStream(nullptr), + d_satSolver(nullptr) { } -void DecisionEngine::finishInit(prop::CDCLTSatSolverInterface* ss, - prop::CnfStream* cs) +void DecisionEngine::finishInit(CDCLTSatSolverInterface* ss, CnfStream* cs) { - if (d_useOld) - { - d_decEngineOld->setSatSolver(ss); - d_decEngineOld->setCnfStream(cs); - return; - } - d_jstrat->finishInit(ss, cs); -} - -void DecisionEngine::presolve() -{ - if (!d_useOld) - { - d_jstrat->presolve(); - } + d_satSolver = ss; + d_cnfStream = cs; } prop::SatLiteral DecisionEngine::getNext(bool& stopSearch) { d_resourceManager->spendResource(Resource::DecisionStep); - if (d_useOld) - { - return d_decEngineOld->getNext(stopSearch); - } - return d_jstrat->getNext(stopSearch); -} - -bool DecisionEngine::isDone() -{ - if (d_useOld) - { - return d_decEngineOld->isDone(); - } - return d_jstrat->isDone(); + return getNextInternal(stopSearch); } -void DecisionEngine::addAssertion(TNode assertion) +DecisionEngineEmpty::DecisionEngineEmpty(context::Context* sc, + ResourceManager* rm) + : DecisionEngine(sc, rm) { - if (d_useOld) - { - d_decEngineOld->addAssertion(assertion); - return; - } - d_jstrat->addAssertion(assertion); } - -void DecisionEngine::addSkolemDefinition(TNode lem, TNode skolem) -{ - if (d_useOld) - { - d_decEngineOld->addSkolemDefinition(lem, skolem); - } - else - { - d_jstrat->addSkolemDefinition(lem, skolem); - } -} - -void DecisionEngine::notifyAsserted(TNode n) +bool DecisionEngineEmpty::isDone() { return false; } +void DecisionEngineEmpty::addAssertion(TNode assertion) {} +void DecisionEngineEmpty::addSkolemDefinition(TNode lem, TNode skolem) {} +prop::SatLiteral DecisionEngineEmpty::getNextInternal(bool& stopSearch) { - if (d_useOld) - { - return; - } - // old implementation does not use this - d_jstrat->notifyAsserted(n); + return undefSatLiteral; } } // namespace decision diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index e54e1fc3c..4cf057840 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -18,20 +18,12 @@ #ifndef CVC5__DECISION__DECISION_ENGINE_H #define CVC5__DECISION__DECISION_ENGINE_H -#include "decision/justification_strategy.h" #include "expr/node.h" #include "prop/cnf_stream.h" #include "prop/sat_solver.h" #include "prop/sat_solver_types.h" namespace cvc5 { - -namespace prop { -class SkolemDefManager; -} - -class DecisionEngineOld; - namespace decision { class DecisionEngine @@ -39,48 +31,68 @@ class DecisionEngine public: /** Constructor */ DecisionEngine(context::Context* sc, - context::UserContext* uc, - prop::SkolemDefManager* skdm, ResourceManager* rm); + virtual ~DecisionEngine() {} /** Finish initialize */ void finishInit(prop::CDCLTSatSolverInterface* ss, prop::CnfStream* cs); /** Presolve, called at the beginning of each check-sat call */ - void presolve(); + virtual void presolve() {} - /** Gets the next decision based on strategies that are enabled */ + /** + * Gets the next decision based on strategies that are enabled. This sets + * stopSearch to true if no further SAT variables need to be assigned in + * this SAT context. + */ prop::SatLiteral getNext(bool& stopSearch); /** Is the DecisionEngine in a state where it has solved everything? */ - bool isDone(); + virtual bool isDone() = 0; /** * Notify this class that assertion is an (input) assertion, not corresponding * to a skolem definition. */ - void addAssertion(TNode assertion); + virtual void addAssertion(TNode assertion) = 0; /** - * !!!! temporary until the old justification implementation is deleted. - * Notify this class that lem is the skolem definition for skolem, which is + * Notify this class that lem is the skolem definition for skolem, which is * a part of the current assertions. */ - void addSkolemDefinition(TNode lem, TNode skolem); + virtual void addSkolemDefinition(TNode lem, TNode skolem) = 0; /** * Notify this class that the literal n has been asserted, possibly * propagated by the SAT solver. */ - void notifyAsserted(TNode n); + virtual void notifyAsserted(TNode n) {} - private: - /** The old implementation */ - std::unique_ptr d_decEngineOld; - /** The new implementation */ - std::unique_ptr d_jstrat; + protected: + /** Get next internal, the engine-specific implementation of getNext */ + virtual prop::SatLiteral getNextInternal(bool& stopSearch) = 0; + /** Pointer to the SAT context */ + context::Context* d_context; /** Pointer to resource manager for associated SmtEngine */ ResourceManager* d_resourceManager; - /** using old implementation? */ - bool d_useOld; + /** Pointer to the CNF stream */ + prop::CnfStream* d_cnfStream; + /** Pointer to the SAT solver */ + prop::CDCLTSatSolverInterface* d_satSolver; +}; + +/** + * Instance of the above class which does nothing. This is used when + * the decision mode is set to internal. + */ +class DecisionEngineEmpty : public DecisionEngine +{ + public: + DecisionEngineEmpty(context::Context* sc, ResourceManager* rm); + bool isDone() override; + void addAssertion(TNode assertion) override; + void addSkolemDefinition(TNode lem, TNode skolem) override; + + protected: + prop::SatLiteral getNextInternal(bool& stopSearch) override; }; } // namespace decision diff --git a/src/decision/decision_engine_old.cpp b/src/decision/decision_engine_old.cpp index 8ef7ad1f4..6bfba35ee 100644 --- a/src/decision/decision_engine_old.cpp +++ b/src/decision/decision_engine_old.cpp @@ -26,14 +26,14 @@ using namespace std; namespace cvc5 { DecisionEngineOld::DecisionEngineOld(context::Context* sc, - context::UserContext* uc) - : d_cnfStream(nullptr), - d_satSolver(nullptr), - d_satContext(sc), - d_userContext(uc), + context::UserContext* uc, + ResourceManager* rm) + : DecisionEngine(sc, rm), d_result(sc, SAT_VALUE_UNKNOWN), d_engineState(0), - d_enabledITEStrategy(nullptr) + d_enabledITEStrategy(nullptr), + d_decisionStopOnly(options::decisionMode() + == options::DecisionMode::STOPONLY_OLD) { Trace("decision") << "Creating decision engine" << std::endl; Assert(d_engineState == 0); @@ -42,13 +42,13 @@ DecisionEngineOld::DecisionEngineOld(context::Context* sc, Trace("decision-init") << "DecisionEngineOld::init()" << std::endl; Trace("decision-init") << " * options->decisionMode: " << options::decisionMode() << std::endl; - Trace("decision-init") << " * options->decisionStopOnly: " - << options::decisionStopOnly() << std::endl; + Trace("decision-init") << " * decisionStopOnly: " << d_decisionStopOnly + << std::endl; if (options::decisionMode() == options::DecisionMode::JUSTIFICATION) { - d_enabledITEStrategy.reset(new decision::JustificationHeuristic( - this, d_userContext, d_satContext)); + d_enabledITEStrategy.reset( + new decision::JustificationHeuristic(this, uc, sc)); } } @@ -61,16 +61,18 @@ void DecisionEngineOld::shutdown() d_enabledITEStrategy.reset(nullptr); } -SatLiteral DecisionEngineOld::getNext(bool& stopSearch) +SatLiteral DecisionEngineOld::getNextInternal(bool& stopSearch) { Assert(d_cnfStream != nullptr) << "Forgot to set cnfStream for decision engine?"; Assert(d_satSolver != nullptr) << "Forgot to set satSolver for decision engine?"; - return d_enabledITEStrategy == nullptr - ? undefSatLiteral - : d_enabledITEStrategy->getNext(stopSearch); + SatLiteral ret = d_enabledITEStrategy == nullptr + ? undefSatLiteral + : d_enabledITEStrategy->getNext(stopSearch); + // if we are doing stop only, we don't return the literal + return d_decisionStopOnly ? undefSatLiteral : ret; } void DecisionEngineOld::addAssertion(TNode assertion) diff --git a/src/decision/decision_engine_old.h b/src/decision/decision_engine_old.h index 4e7bde4b5..3e9a563b7 100644 --- a/src/decision/decision_engine_old.h +++ b/src/decision/decision_engine_old.h @@ -20,6 +20,7 @@ #include "base/output.h" #include "context/cdo.h" +#include "decision/decision_engine.h" #include "decision/decision_strategy.h" #include "expr/node.h" #include "prop/cnf_stream.h" @@ -32,13 +33,15 @@ using namespace cvc5::decision; namespace cvc5 { -class DecisionEngineOld +class DecisionEngineOld : public decision::DecisionEngine { public: // Necessary functions /** Constructor */ - DecisionEngineOld(context::Context* sc, context::UserContext* uc); + DecisionEngineOld(context::Context* sc, + context::UserContext* uc, + ResourceManager* rm); /** Destructor, currently does nothing */ ~DecisionEngineOld() @@ -46,22 +49,6 @@ class DecisionEngineOld Trace("decision") << "Destroying decision engine" << std::endl; } - void setSatSolver(CDCLTSatSolverInterface* ss) - { - // setPropEngine should not be called more than once - Assert(d_satSolver == NULL); - Assert(ss != NULL); - d_satSolver = ss; - } - - void setCnfStream(CnfStream* cs) - { - // setPropEngine should not be called more than once - Assert(d_cnfStream == NULL); - Assert(cs != NULL); - d_cnfStream = cs; - } - /** * This is called by SmtEngine, at shutdown time, just before * destruction. It is important because there are destruction @@ -72,10 +59,10 @@ class DecisionEngineOld // Interface for External World to use our services /** Gets the next decision based on strategies that are enabled */ - SatLiteral getNext(bool& stopSearch); + SatLiteral getNextInternal(bool& stopSearch) override; /** Is the DecisionEngineOld in a state where it has solved everything? */ - bool isDone() + bool isDone() override { Trace("decision") << "DecisionEngineOld::isDone() returning " << (d_result != SAT_VALUE_UNKNOWN) @@ -107,12 +94,12 @@ class DecisionEngineOld * Notify this class that assertion is an (input) assertion, not corresponding * to a skolem definition. */ - void addAssertion(TNode assertion); + void addAssertion(TNode assertion) override; /** * Notify this class that lem is the skolem definition for skolem, which is * a part of the current assertions. */ - void addSkolemDefinition(TNode lem, TNode skolem); + void addSkolemDefinition(TNode lem, TNode skolem) override; // Interface for Strategies to use stuff stored in Decision Engine // (which was possibly requested by them on initialization) @@ -129,12 +116,6 @@ class DecisionEngineOld // Disable creating decision engine without required parameters DecisionEngineOld(); - CnfStream* d_cnfStream; - CDCLTSatSolverInterface* d_satSolver; - - context::Context* d_satContext; - context::UserContext* d_userContext; - // Does decision engine know the answer? context::CDO d_result; @@ -142,6 +123,8 @@ class DecisionEngineOld unsigned d_engineState; // 0=pre-init; 1=init,pre-shutdown; 2=shutdown /** The ITE decision strategy we have allocated */ std::unique_ptr d_enabledITEStrategy; + /** Whether we are using stop only */ + bool d_decisionStopOnly; }; /* DecisionEngineOld class */ diff --git a/src/decision/justification_strategy.cpp b/src/decision/justification_strategy.cpp index b73b24bd0..56d96b32f 100644 --- a/src/decision/justification_strategy.cpp +++ b/src/decision/justification_strategy.cpp @@ -25,10 +25,9 @@ namespace decision { JustificationStrategy::JustificationStrategy(context::Context* c, context::UserContext* u, - prop::SkolemDefManager* skdm) - : d_context(c), - d_cnfStream(nullptr), - d_satSolver(nullptr), + prop::SkolemDefManager* skdm, + ResourceManager* rm) + : DecisionEngine(c, rm), d_skdm(skdm), d_assertions( u, @@ -40,18 +39,13 @@ JustificationStrategy::JustificationStrategy(context::Context* c, d_lastDecisionLit(c), d_currStatusDec(false), d_useRlvOrder(options::jhRlvOrder()), + d_decisionStopOnly(options::decisionMode() + == options::DecisionMode::STOPONLY), d_jhSkMode(options::jhSkolemMode()), d_jhSkRlvMode(options::jhSkolemRlvMode()) { } -void JustificationStrategy::finishInit(CDCLTSatSolverInterface* ss, - CnfStream* cs) -{ - d_satSolver = ss; - d_cnfStream = cs; -} - void JustificationStrategy::presolve() { d_lastDecisionLit = Node::null(); @@ -64,7 +58,7 @@ void JustificationStrategy::presolve() d_stack.clear(); } -SatLiteral JustificationStrategy::getNext(bool& stopSearch) +SatLiteral JustificationStrategy::getNextInternal(bool& stopSearch) { // ensure we have an assertion if (!refreshCurrentAssertion()) @@ -186,6 +180,11 @@ SatLiteral JustificationStrategy::getNext(bool& stopSearch) d_lastDecisionLit = next.first; // record that we made a decision d_currStatusDec = true; + if (d_decisionStopOnly) + { + // only doing stop-only, return undefSatLiteral. + return undefSatLiteral; + } return lastChildVal == SAT_VALUE_FALSE ? ~nsl : nsl; } else diff --git a/src/decision/justification_strategy.h b/src/decision/justification_strategy.h index 667f53115..fc31805dd 100644 --- a/src/decision/justification_strategy.h +++ b/src/decision/justification_strategy.h @@ -21,6 +21,7 @@ #include "context/cdinsert_hashmap.h" #include "context/cdo.h" #include "decision/assertion_list.h" +#include "decision/decision_engine.h" #include "decision/justify_info.h" #include "decision/justify_stack.h" #include "decision/justify_stats.h" @@ -117,19 +118,17 @@ namespace decision { * definition, and Q alone would have sufficed to show the input formula * was satisfied. */ -class JustificationStrategy +class JustificationStrategy : public DecisionEngine { public: /** Constructor */ JustificationStrategy(context::Context* c, context::UserContext* u, - prop::SkolemDefManager* skdm); - - /** Finish initialize */ - void finishInit(prop::CDCLTSatSolverInterface* ss, prop::CnfStream* cs); + prop::SkolemDefManager* skdm, + ResourceManager* rm); /** Presolve, called at the beginning of each check-sat call */ - void presolve(); + void presolve() override; /** * Gets the next decision based on the current assertion to satisfy. This @@ -140,7 +139,7 @@ class JustificationStrategy * @param stopSearch Set to true if we can stop the search * @return The next SAT literal to decide on. */ - prop::SatLiteral getNext(bool& stopSearch); + prop::SatLiteral getNextInternal(bool& stopSearch) override; /** * Are we finished assigning values to literals? @@ -148,24 +147,24 @@ class JustificationStrategy * @return true if and only if all relevant input assertions are already * propositionally satisfied by the current assignment. */ - bool isDone(); + bool isDone() override; /** * Notify this class that assertion is an (input) assertion, not corresponding * to a skolem definition. */ - void addAssertion(TNode assertion); + void addAssertion(TNode assertion) override; /** * Notify this class that lem is the skolem definition for skolem, which is * a part of the current assertions. */ - void addSkolemDefinition(TNode lem, TNode skolem); + void addSkolemDefinition(TNode lem, TNode skolem) override; /** * Notify this class that literal n has been asserted. This is triggered when * n is sent to TheoryEngine. This activates skolem definitions for skolems * k that occur in n. */ - void notifyAsserted(TNode n); + void notifyAsserted(TNode n) override; private: /** @@ -225,12 +224,6 @@ class JustificationStrategy static bool isTheoryLiteral(TNode n); /** Is n a theory atom? */ static bool isTheoryAtom(TNode n); - /** Pointer to the SAT context */ - context::Context* d_context; - /** Pointer to the CNF stream */ - prop::CnfStream* d_cnfStream; - /** Pointer to the SAT solver */ - prop::CDCLTSatSolverInterface* d_satSolver; /** Pointer to the skolem definition manager */ prop::SkolemDefManager* d_skdm; /** The assertions, which are user-context dependent. */ @@ -252,6 +245,8 @@ class JustificationStrategy //------------------------------------ options /** using relevancy order */ bool d_useRlvOrder; + /** using stop only */ + bool d_decisionStopOnly; /** skolem mode */ options::JutificationSkolemMode d_jhSkMode; /** skolem relevancy mode */ diff --git a/src/options/README.md b/src/options/README.md index df5686abc..b0b026166 100644 --- a/src/options/README.md +++ b/src/options/README.md @@ -194,14 +194,14 @@ Full Example [[option.mode.JUSTIFICATION]] name = "justification" help = "An ATGP-inspired justification heuristic." - [[option.mode.RELEVANCY]] + [[option.mode.STOPONLY]] name = "justification-stoponly" help = "Use the justification heuristic only to stop early, not for decisions." This defines a new option that is accessible via `d_options.{module.id}.decisionMode` and stores an automatically generated mode `DecisionMode`, an enum class with the values `INTERNAL`, `JUSTIFICATION` and -`RELEVANCY`. From the outside, it can be set by `--decision=internal`, but also +`STOPONLY`. From the outside, it can be set by `--decision=internal`, but also with `--decision-mode=justification`, and similarly from an SMT-LIB input with `(set-option :decision internal)` and `(set-option :decision-mode justification)`. The command-line help for this option looks as follows: diff --git a/src/options/decision_options.toml b/src/options/decision_options.toml index 8cc2bf2fe..abb27ac9f 100644 --- a/src/options/decision_options.toml +++ b/src/options/decision_options.toml @@ -8,7 +8,6 @@ name = "Decision Heuristics" long = "decision=MODE" type = "DecisionMode" default = "INTERNAL" - predicates = ["setDecisionModeStopOnly"] help = "choose decision mode, see --decision=help" help_mode = "Decision modes." [[option.mode.INTERNAL]] @@ -17,17 +16,15 @@ name = "Decision Heuristics" [[option.mode.JUSTIFICATION]] name = "justification" help = "An ATGP-inspired justification heuristic." +[[option.mode.STOPONLY]] + name = "stoponly" + help = "Use the justification heuristic only to stop early, not for decisions." [[option.mode.JUSTIFICATION_OLD]] name = "justification-old" help = "Older implementation of an ATGP-inspired justification heuristic." -[[option.mode.RELEVANCY]] - name = "justification-stoponly" - help = "Use the justification heuristic only to stop early, not for decisions." - -[[option]] - name = "decisionStopOnly" - category = "undocumented" - type = "bool" +[[option.mode.STOPONLY_OLD]] + name = "stoponly-old" + help = "Use the old implementation of justification heuristic only to stop early, not for decisions." [[option]] name = "decisionThreshold" diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 6958dcb12..e423dc149 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -234,14 +234,6 @@ InstFormatMode OptionsHandler::stringToInstFormatMode(const std::string& option, } } -// decision/options_handlers.h -void OptionsHandler::setDecisionModeStopOnly(const std::string& option, - const std::string& flag, - DecisionMode m) -{ - d_options->decision.decisionStopOnly = (m == DecisionMode::RELEVANCY); -} - void OptionsHandler::setProduceAssertions(const std::string& option, const std::string& flag, bool value) diff --git a/src/options/options_handler.h b/src/options/options_handler.h index bf07729ae..eed361c0d 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -100,11 +100,6 @@ public: const std::string& flag, const std::string& optarg); - // decision/options_handlers.h - void setDecisionModeStopOnly(const std::string& option, - const std::string& flag, - DecisionMode m); - /** * Throws a ModalException if this option is being set after final * initialization. diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 62b2f655c..24b98577f 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -21,8 +21,8 @@ #include "base/check.h" #include "base/output.h" -#include "decision/decision_engine.h" #include "decision/decision_engine_old.h" +#include "decision/justification_strategy.h" #include "options/base_options.h" #include "options/decision_options.h" #include "options/main_options.h" @@ -88,8 +88,22 @@ PropEngine::PropEngine(TheoryEngine* te, context::UserContext* userContext = d_env.getUserContext(); ResourceManager* rm = d_env.getResourceManager(); - d_decisionEngine.reset( - new decision::DecisionEngine(satContext, userContext, d_skdm.get(), rm)); + options::DecisionMode dmode = options::decisionMode(); + if (dmode == options::DecisionMode::JUSTIFICATION + || dmode == options::DecisionMode::STOPONLY) + { + d_decisionEngine.reset(new decision::JustificationStrategy( + satContext, userContext, d_skdm.get(), rm)); + } + else if (dmode == options::DecisionMode::JUSTIFICATION_OLD + || dmode == options::DecisionMode::STOPONLY_OLD) + { + d_decisionEngine.reset(new DecisionEngineOld(satContext, userContext, rm)); + } + else + { + d_decisionEngine.reset(new decision::DecisionEngineEmpty(satContext, rm)); + } d_satSolver = SatSolverFactory::createCDCLTMinisat(smtStatisticsRegistry()); diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 845289841..47263af97 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -151,7 +151,7 @@ SatLiteral TheoryProxy::getNextDecisionEngineRequest(bool &stopSearch) { if(stopSearch) { Trace("decision") << " *** Decision Engine stopped search *** " << std::endl; } - return options::decisionStopOnly() ? undefSatLiteral : ret; + return ret; } bool TheoryProxy::theoryNeedCheck() const { diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 229fdeec5..f4d885f4b 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -946,9 +946,20 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) ? true : false); - Trace("smt") << "setting decision mode to " << decMode << std::endl; opts.decision.decisionMode = decMode; - opts.decision.decisionStopOnly = stoponly; + if (stoponly) + { + if (opts.decision.decisionMode == options::DecisionMode::JUSTIFICATION) + { + opts.decision.decisionMode = options::DecisionMode::STOPONLY; + } + else + { + Assert(opts.decision.decisionMode == options::DecisionMode::INTERNAL); + } + } + Trace("smt") << "setting decision mode to " << opts.decision.decisionMode + << std::endl; } if (options::incrementalSolving()) {