diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-05-04 15:36:41 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-04 15:36:41 -0300 |
commit | 5018442120cb22e6f1923a97df7cd98c2d2b5a4a (patch) | |
tree | 4b2c5331b7fe482c047665e069bffe0392b3989e /src/prop | |
parent | 4f265b2c81c4cb858942f6e1e51ce8abdd01345b (diff) |
Do not use proof CNF stream with assumptions-based cores (#6488)
Previously using proof CNF stream together with assumptions-based unsat cores added unnecessary performance overhead.
Co-authored-by: Mathias Preiner mathias.preiner@gmail.com
Diffstat (limited to 'src/prop')
-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()); |