diff options
Diffstat (limited to 'src/decision/justification_strategy.cpp')
| -rw-r--r-- | src/decision/justification_strategy.cpp | 21 |
1 files changed, 10 insertions, 11 deletions
diff --git a/src/decision/justification_strategy.cpp b/src/decision/justification_strategy.cpp index 56d96b32f..d9e6b43e9 100644 --- a/src/decision/justification_strategy.cpp +++ b/src/decision/justification_strategy.cpp @@ -23,20 +23,19 @@ using namespace cvc5::prop; namespace cvc5 { namespace decision { -JustificationStrategy::JustificationStrategy(context::Context* c, - context::UserContext* u, - prop::SkolemDefManager* skdm, - ResourceManager* rm) - : DecisionEngine(c, rm), +JustificationStrategy::JustificationStrategy(Env& env, + prop::SkolemDefManager* skdm) + : DecisionEngine(env), d_skdm(skdm), d_assertions( - u, - c, + userContext(), + context(), options::jhRlvOrder()), // assertions are user-context dependent - d_skolemAssertions(c, c), // skolem assertions are SAT-context dependent - d_justified(c), - d_stack(c), - d_lastDecisionLit(c), + d_skolemAssertions( + context(), context()), // skolem assertions are SAT-context dependent + d_justified(context()), + d_stack(context()), + d_lastDecisionLit(context()), d_currStatusDec(false), d_useRlvOrder(options::jhRlvOrder()), d_decisionStopOnly(options::decisionMode() |