diff options
| -rw-r--r-- | src/prop/prop_engine.cpp | 26 | ||||
| -rw-r--r-- | src/prop/theory_proxy.cpp | 3 |
2 files changed, 19 insertions, 10 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 23377cb0c..5903c1606 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -111,11 +111,17 @@ PropEngine::PropEngine(TheoryEngine* te, // connect theory proxy d_theoryProxy->finishInit(d_cnfStream); // connect SAT solver - d_satSolver->initialize(d_context, d_theoryProxy, userContext, pnm); + d_satSolver->initialize( + d_context, + d_theoryProxy, + userContext, + options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS + ? pnm + : nullptr); d_decisionEngine->setSatSolver(d_satSolver); d_decisionEngine->setCnfStream(d_cnfStream); - if (pnm) + if (pnm && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS) { d_pfCnfStream.reset(new ProofCnfStream( userContext, @@ -261,21 +267,23 @@ void PropEngine::assertInternal( TNode node, bool negated, bool removable, bool input, ProofGenerator* pg) { // Assert as (possibly) removable - if (isProofEnabled()) + if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS) { - if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS - && input) + if (input) { Assert(!negated); - d_pfCnfStream->ensureLiteral(node); + d_cnfStream->ensureLiteral(node); d_assumptions.push_back(node); } else { - d_pfCnfStream->convertAndAssert(node, negated, removable, pg); + d_cnfStream->convertAndAssert(node, removable, negated, input); } - - // if input, register the assertion + } + else if (isProofEnabled()) + { + d_pfCnfStream->convertAndAssert(node, negated, removable, pg); + // if input, register the assertion in the proof manager if (input) { d_ppm->registerAssertion(node); diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 43f91f732..090b44b90 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -98,7 +98,8 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { theory::TrustNode tte = d_theoryEngine->getExplanation(lNode); Node theoryExplanation = tte.getNode(); - if (options::produceProofs()) + if (options::produceProofs() + && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS) { Assert(options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF || tte.getGenerator()); |