diff options
| -rw-r--r-- | src/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/decision/decision_engine.cpp | 94 | ||||
| -rw-r--r-- | src/decision/decision_engine.h | 136 | ||||
| -rw-r--r-- | src/decision/decision_engine_old.cpp | 96 | ||||
| -rw-r--r-- | src/decision/decision_engine_old.h | 150 | ||||
| -rw-r--r-- | src/decision/decision_strategy.h | 15 | ||||
| -rw-r--r-- | src/decision/justification_heuristic.cpp | 6 | ||||
| -rw-r--r-- | src/decision/justification_heuristic.h | 2 | ||||
| -rw-r--r-- | src/prop/prop_engine.cpp | 10 |
9 files changed, 337 insertions, 174 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index af206c14d..901897e83 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -24,6 +24,8 @@ libcvc5_add_sources( decision/decision_attributes.h decision/decision_engine.cpp decision/decision_engine.h + decision/decision_engine_old.cpp + decision/decision_engine_old.h decision/decision_strategy.h decision/justification_heuristic.cpp decision/justification_heuristic.h diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index d55d2077f..4116ba90d 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -14,92 +14,80 @@ */ #include "decision/decision_engine.h" -#include "decision/decision_attributes.h" -#include "decision/justification_heuristic.h" -#include "expr/node.h" +#include "decision/decision_engine_old.h" #include "options/decision_options.h" -#include "options/smt_options.h" +#include "prop/sat_solver.h" #include "util/resource_manager.h" -using namespace std; - namespace cvc5 { namespace decision { -DecisionEngine::DecisionEngine(context::Context* sc, - context::UserContext* uc, +DecisionEngine::DecisionEngine(context::Context* c, + context::UserContext* u, + prop::SkolemDefManager* skdm, ResourceManager* rm) - : d_cnfStream(nullptr), - d_satSolver(nullptr), - d_satContext(sc), - d_userContext(uc), - d_result(sc, SAT_VALUE_UNKNOWN), - d_engineState(0), + : d_decEngineOld(new DecisionEngineOld(c, u)), d_resourceManager(rm), - d_enabledITEStrategy(nullptr) + d_useOld(true) { - Trace("decision") << "Creating decision engine" << std::endl; } -void DecisionEngine::init() +void DecisionEngine::finishInit(prop::CDCLTSatSolverInterface* ss, + prop::CnfStream* cs) { - Assert(d_engineState == 0); - d_engineState = 1; - - Trace("decision-init") << "DecisionEngine::init()" << std::endl; - Trace("decision-init") << " * options->decisionMode: " - << options::decisionMode() << std:: endl; - Trace("decision-init") << " * options->decisionStopOnly: " - << options::decisionStopOnly() << std::endl; - - if (options::decisionMode() == options::DecisionMode::JUSTIFICATION) + if (d_useOld) { - d_enabledITEStrategy.reset(new decision::JustificationHeuristic( - this, d_userContext, d_satContext)); + d_decEngineOld->setSatSolver(ss); + d_decEngineOld->setCnfStream(cs); + return; } } -void DecisionEngine::shutdown() -{ - Trace("decision") << "Shutting down decision engine" << std::endl; - - Assert(d_engineState == 1); - d_engineState = 2; - d_enabledITEStrategy.reset(nullptr); -} +void DecisionEngine::presolve() {} -SatLiteral DecisionEngine::getNext(bool& stopSearch) +prop::SatLiteral DecisionEngine::getNext(bool& stopSearch) { d_resourceManager->spendResource(Resource::DecisionStep); - Assert(d_cnfStream != nullptr) - << "Forgot to set cnfStream for decision engine?"; - Assert(d_satSolver != nullptr) - << "Forgot to set satSolver for decision engine?"; + if (d_useOld) + { + return d_decEngineOld->getNext(stopSearch); + } + return undefSatLiteral; +} - return d_enabledITEStrategy == nullptr - ? undefSatLiteral - : d_enabledITEStrategy->getNext(stopSearch); +bool DecisionEngine::isDone() +{ + if (d_useOld) + { + return d_decEngineOld->isDone(); + } + return false; } void DecisionEngine::addAssertion(TNode assertion) { - // new assertions, reset whatever result we knew - d_result = SAT_VALUE_UNKNOWN; - if (d_enabledITEStrategy != nullptr) + if (d_useOld) { - d_enabledITEStrategy->addAssertion(assertion); + d_decEngineOld->addAssertion(assertion); + return; } } void DecisionEngine::addSkolemDefinition(TNode lem, TNode skolem) { - // new assertions, reset whatever result we knew - d_result = SAT_VALUE_UNKNOWN; - if (d_enabledITEStrategy != nullptr) + if (d_useOld) { - d_enabledITEStrategy->addSkolemDefinition(lem, skolem); + d_decEngineOld->addSkolemDefinition(lem, skolem); } } +void DecisionEngine::notifyAsserted(TNode n) +{ + if (d_useOld) + { + return; + } } + +} // namespace decision } // namespace cvc5 diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index c10fe2bb9..de88d656e 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -18,110 +18,41 @@ #ifndef CVC5__DECISION__DECISION_ENGINE_H #define CVC5__DECISION__DECISION_ENGINE_H -#include "base/output.h" -#include "context/cdo.h" -#include "decision/decision_strategy.h" #include "expr/node.h" #include "prop/cnf_stream.h" #include "prop/sat_solver.h" #include "prop/sat_solver_types.h" -#include "util/result.h" - -using namespace cvc5::prop; -using namespace cvc5::decision; namespace cvc5 { -namespace decision { - -class DecisionEngine { - - // PropEngine* d_propEngine; - CnfStream* d_cnfStream; - CDCLTSatSolverInterface* d_satSolver; - - context::Context* d_satContext; - context::UserContext* d_userContext; - // Does decision engine know the answer? - context::CDO<SatValue> d_result; +namespace prop { +class SkolemDefManager; +} - // Disable creating decision engine without required parameters - DecisionEngine(); +class DecisionEngineOld; - // init/shutdown state - unsigned d_engineState; // 0=pre-init; 1=init,pre-shutdown; 2=shutdown - /** Pointer to resource manager for associated SmtEngine */ - ResourceManager* d_resourceManager; +namespace decision { +class DecisionEngine +{ public: - // Necessary functions - /** Constructor */ DecisionEngine(context::Context* sc, context::UserContext* uc, + prop::SkolemDefManager* skdm, ResourceManager* rm); - /** Destructor, currently does nothing */ - ~DecisionEngine() { - 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; - } - - /* Enables decision strategy based on options. */ - void init(); + /** Finish initialize */ + void finishInit(prop::CDCLTSatSolverInterface* ss, prop::CnfStream* cs); - /** - * This is called by SmtEngine, at shutdown time, just before - * destruction. It is important because there are destruction - * ordering issues between some parts of the system. - */ - void shutdown(); - - // Interface for External World to use our services + /** Presolve, called at the beginning of each check-sat call */ + void presolve(); /** Gets the next decision based on strategies that are enabled */ - SatLiteral getNext(bool& stopSearch); + prop::SatLiteral getNext(bool& stopSearch); /** Is the DecisionEngine in a state where it has solved everything? */ - bool isDone() { - Trace("decision") << "DecisionEngine::isDone() returning " - << (d_result != SAT_VALUE_UNKNOWN) - << (d_result != SAT_VALUE_UNKNOWN ? "true" : "false") - << std::endl; - return (d_result != SAT_VALUE_UNKNOWN); - } - - /** */ - Result getResult() { - switch(d_result.get()) { - case SAT_VALUE_TRUE: return Result(Result::SAT); - case SAT_VALUE_FALSE: return Result(Result::UNSAT); - case SAT_VALUE_UNKNOWN: return Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); - default: Assert(false) << "d_result is garbage"; - } - return Result(); - } - - /** */ - void setResult(SatValue val) { - d_result = val; - } - - // External World helping us help the Strategies + bool isDone(); /** * Notify this class that assertion is an (input) assertion, not corresponding @@ -129,38 +60,27 @@ class DecisionEngine { */ void addAssertion(TNode assertion); /** + * TODO: remove this interface * 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); - - // Interface for Strategies to use stuff stored in Decision Engine - // (which was possibly requested by them on initialization) - - // Interface for Strategies to get information about External World - - bool hasSatLiteral(TNode n) { - return d_cnfStream->hasLiteral(n); - } - SatLiteral getSatLiteral(TNode n) { - return d_cnfStream->getLiteral(n); - } - SatValue getSatValue(SatLiteral l) { - return d_satSolver->value(l); - } - SatValue getSatValue(TNode n) { - return getSatValue(getSatLiteral(n)); - } - Node getNode(SatLiteral l) { - return d_cnfStream->getNode(l); - } + /** + * Notify this class that the literal n has been asserted, possibly + * propagated by the SAT solver. + */ + void notifyAsserted(TNode n); private: - /** The ITE decision strategy we have allocated */ - std::unique_ptr<ITEDecisionStrategy> d_enabledITEStrategy; -};/* DecisionEngine class */ + /** The old implementation */ + std::unique_ptr<DecisionEngineOld> d_decEngineOld; + /** Pointer to resource manager for associated SmtEngine */ + ResourceManager* d_resourceManager; + /** using old implementation? */ + bool d_useOld; +}; -} +} // namespace decision } // namespace cvc5 #endif /* CVC5__DECISION__DECISION_ENGINE_H */ diff --git a/src/decision/decision_engine_old.cpp b/src/decision/decision_engine_old.cpp new file mode 100644 index 000000000..8ef7ad1f4 --- /dev/null +++ b/src/decision/decision_engine_old.cpp @@ -0,0 +1,96 @@ +/****************************************************************************** + * Top contributors (to current version): + * Kshitij Bansal, Aina Niemetz, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Old implementation of the decision engine + */ +#include "decision/decision_engine_old.h" + +#include "decision/decision_attributes.h" +#include "decision/justification_heuristic.h" +#include "expr/node.h" +#include "options/decision_options.h" +#include "options/smt_options.h" +#include "util/resource_manager.h" + +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), + d_result(sc, SAT_VALUE_UNKNOWN), + d_engineState(0), + d_enabledITEStrategy(nullptr) +{ + Trace("decision") << "Creating decision engine" << std::endl; + Assert(d_engineState == 0); + d_engineState = 1; + + 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; + + if (options::decisionMode() == options::DecisionMode::JUSTIFICATION) + { + d_enabledITEStrategy.reset(new decision::JustificationHeuristic( + this, d_userContext, d_satContext)); + } +} + +void DecisionEngineOld::shutdown() +{ + Trace("decision") << "Shutting down decision engine" << std::endl; + + Assert(d_engineState == 1); + d_engineState = 2; + d_enabledITEStrategy.reset(nullptr); +} + +SatLiteral DecisionEngineOld::getNext(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); +} + +void DecisionEngineOld::addAssertion(TNode assertion) +{ + // new assertions, reset whatever result we knew + d_result = SAT_VALUE_UNKNOWN; + if (d_enabledITEStrategy != nullptr) + { + d_enabledITEStrategy->addAssertion(assertion); + } +} + +void DecisionEngineOld::addSkolemDefinition(TNode lem, TNode skolem) +{ + // new assertions, reset whatever result we knew + d_result = SAT_VALUE_UNKNOWN; + if (d_enabledITEStrategy != nullptr) + { + d_enabledITEStrategy->addSkolemDefinition(lem, skolem); + } +} + +} // namespace cvc5 diff --git a/src/decision/decision_engine_old.h b/src/decision/decision_engine_old.h new file mode 100644 index 000000000..e9169d9b2 --- /dev/null +++ b/src/decision/decision_engine_old.h @@ -0,0 +1,150 @@ +/****************************************************************************** + * Top contributors (to current version): + * Kshitij Bansal, Andrew Reynolds, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Old implementation of the decision engine + */ + +#include "cvc5_private.h" + +#ifndef CVC4__DECISION__DECISION_ENGINE_OLD_H +#define CVC4__DECISION__DECISION_ENGINE_OLD_H + +#include "base/output.h" +#include "context/cdo.h" +#include "decision/decision_strategy.h" +#include "expr/node.h" +#include "prop/cnf_stream.h" +#include "prop/sat_solver.h" +#include "prop/sat_solver_types.h" +#include "util/result.h" + +using namespace cvc5::prop; +using namespace cvc5::decision; + +namespace cvc5 { + +class DecisionEngineOld +{ + public: + // Necessary functions + + /** Constructor */ + DecisionEngineOld(context::Context* sc, context::UserContext* uc); + + /** Destructor, currently does nothing */ + ~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 + * ordering issues between some parts of the system. + */ + void shutdown(); + + // Interface for External World to use our services + + /** Gets the next decision based on strategies that are enabled */ + SatLiteral getNext(bool& stopSearch); + + /** Is the DecisionEngineOld in a state where it has solved everything? */ + bool isDone() + { + Trace("decision") << "DecisionEngineOld::isDone() returning " + << (d_result != SAT_VALUE_UNKNOWN) + << (d_result != SAT_VALUE_UNKNOWN ? "true" : "false") + << std::endl; + return (d_result != SAT_VALUE_UNKNOWN); + } + + /** */ + Result getResult() + { + switch (d_result.get()) + { + case SAT_VALUE_TRUE: return Result(Result::SAT); + case SAT_VALUE_FALSE: return Result(Result::UNSAT); + case SAT_VALUE_UNKNOWN: + return Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); + default: Assert(false) << "d_result is garbage"; + } + return Result(); + } + + /** */ + void setResult(SatValue val) { d_result = val; } + + // External World helping us help the Strategies + + /** + * Notify this class that assertion is an (input) assertion, not corresponding + * to a skolem definition. + */ + void addAssertion(TNode assertion); + /** + * 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); + + // Interface for Strategies to use stuff stored in Decision Engine + // (which was possibly requested by them on initialization) + + // Interface for Strategies to get information about External World + + bool hasSatLiteral(TNode n) { return d_cnfStream->hasLiteral(n); } + SatLiteral getSatLiteral(TNode n) { return d_cnfStream->getLiteral(n); } + SatValue getSatValue(SatLiteral l) { return d_satSolver->value(l); } + SatValue getSatValue(TNode n) { return getSatValue(getSatLiteral(n)); } + Node getNode(SatLiteral l) { return d_cnfStream->getNode(l); } + + private: + // 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<SatValue> d_result; + + // init/shutdown state + unsigned d_engineState; // 0=pre-init; 1=init,pre-shutdown; 2=shutdown + /** The ITE decision strategy we have allocated */ + std::unique_ptr<ITEDecisionStrategy> d_enabledITEStrategy; + +}; /* DecisionEngineOld class */ + +} // namespace cvc5 + +#endif /* CVC4__DECISION__DECISION_ENGINE_H */ diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h index 0376b00cc..87c463c29 100644 --- a/src/decision/decision_strategy.h +++ b/src/decision/decision_strategy.h @@ -26,6 +26,8 @@ namespace cvc5 { +class DecisionEngineOld; + namespace context { class Context; } // namespace context @@ -36,10 +38,12 @@ class DecisionEngine; class DecisionStrategy { protected: - DecisionEngine* d_decisionEngine; + DecisionEngineOld* d_decisionEngine; + public: - DecisionStrategy(DecisionEngine* de, context::Context *c) : - d_decisionEngine(de) { + DecisionStrategy(DecisionEngineOld* de, context::Context* c) + : d_decisionEngine(de) + { } virtual ~DecisionStrategy() { } @@ -49,8 +53,9 @@ public: class ITEDecisionStrategy : public DecisionStrategy { public: - ITEDecisionStrategy(DecisionEngine* de, context::Context *c) : - DecisionStrategy(de, c) { + ITEDecisionStrategy(DecisionEngineOld* de, context::Context* c) + : DecisionStrategy(de, c) + { } /** * Add that assertion is an (input) assertion, not corresponding to a diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index ecc0ae68c..dcf8975bb 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -20,7 +20,7 @@ #include "justification_heuristic.h" #include "decision/decision_attributes.h" -#include "decision/decision_engine.h" +#include "decision/decision_engine_old.h" #include "expr/kind.h" #include "expr/node_manager.h" #include "options/decision_options.h" @@ -29,10 +29,12 @@ #include "theory/rewriter.h" #include "util/random.h" +using namespace cvc5::prop; + namespace cvc5 { namespace decision { -JustificationHeuristic::JustificationHeuristic(DecisionEngine* de, +JustificationHeuristic::JustificationHeuristic(DecisionEngineOld* de, context::UserContext* uc, context::Context* c) : ITEDecisionStrategy(de, c), diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 45f297bb9..870d0674c 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -117,7 +117,7 @@ class JustificationHeuristic : public ITEDecisionStrategy { }; public: - JustificationHeuristic(DecisionEngine* de, + JustificationHeuristic(DecisionEngineOld* de, context::UserContext* uc, context::Context* c); diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index dfd4c4528..70401c56d 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -22,6 +22,7 @@ #include "base/check.h" #include "base/output.h" #include "decision/decision_engine.h" +#include "decision/decision_engine_old.h" #include "options/base_options.h" #include "options/decision_options.h" #include "options/main_options.h" @@ -88,8 +89,8 @@ PropEngine::PropEngine(TheoryEngine* te, context::UserContext* userContext = d_env.getUserContext(); ResourceManager* rm = d_env.getResourceManager(); - d_decisionEngine.reset(new DecisionEngine(satContext, userContext, rm)); - d_decisionEngine->init(); // enable appropriate strategies + d_decisionEngine.reset( + new decision::DecisionEngine(satContext, userContext, d_skdm.get(), rm)); d_satSolver = SatSolverFactory::createCDCLTMinisat(smtStatisticsRegistry()); @@ -120,8 +121,7 @@ PropEngine::PropEngine(TheoryEngine* te, ? pnm : nullptr); - d_decisionEngine->setSatSolver(d_satSolver); - d_decisionEngine->setCnfStream(d_cnfStream); + d_decisionEngine->finishInit(d_satSolver, d_cnfStream); if (pnm && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS) { d_pfCnfStream.reset(new ProofCnfStream( @@ -157,7 +157,6 @@ void PropEngine::finishInit() PropEngine::~PropEngine() { Debug("prop") << "Destructing the PropEngine" << std::endl; - d_decisionEngine->shutdown(); d_decisionEngine.reset(nullptr); delete d_cnfStream; delete d_satSolver; @@ -370,6 +369,7 @@ Result PropEngine::checkSat() { d_inCheckSat = true; // TODO This currently ignores conflicts (a dangerous practice). + d_decisionEngine->presolve(); d_theoryEngine->presolve(); if(options::preprocessOnly()) { |