diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-07-09 11:10:00 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-09 11:10:00 -0700 |
| commit | 220dbf7bae9683aa6d14c012b066197af16347b0 (patch) | |
| tree | 28c02ecefb825ce89f3ffdc83828403ad54bf27b /src/decision/justification_strategy.cpp | |
| parent | b00335b00148fe9b5df701f0ce192ac3977e732f (diff) | |
| parent | e25d2ce5eff672bb5b58c245f0414a1ed9c51a6c (diff) | |
Merge branch 'master' into m1buildm1build
Diffstat (limited to 'src/decision/justification_strategy.cpp')
| -rw-r--r-- | src/decision/justification_strategy.cpp | 23 |
1 files changed, 11 insertions, 12 deletions
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 |