diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-04 19:25:25 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-04 19:25:25 -0500 |
| commit | 8a7c43f82b17a444c2f9518bc27f4ea8afe21201 (patch) | |
| tree | 12f66f7bde98f4855b06038d813b49829ea82509 /src/prop | |
| parent | 67c43a7294442a7c660a26faf230cd983b21117d (diff) | |
Move current decision engine to decision engine old (#6466)
The decision engine is the class that contains strategies for doing e.g. justification heuristic.
The current implementation is hardcoded for the old implementation of justification heuristic.
Since both implementations will be maintained in the short term, this splits the parts of DecisionEngine that are specific to the old implementation to a class DecisionEngineOld.
It refactors the interface of DecisionEngine in a way that is compatible with both implementations.
Diffstat (limited to 'src/prop')
| -rw-r--r-- | src/prop/prop_engine.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
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()) { |