diff options
| -rw-r--r-- | src/prop/sat_proof_manager.cpp | 17 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/regress/regress0/proofs/open-pf-datatypes.smt2 | 11 | ||||
| -rw-r--r-- | test/regress/regress0/proofs/open-pf-rederivation.smt2 | 6 |
4 files changed, 30 insertions, 6 deletions
diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index 0f8ad8e69..ad23bedc9 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -162,6 +162,16 @@ void SatProofManager::endResChain(Node conclusion, const std::set<SatLiteral>& conclusionLits) { Trace("sat-proof") << ", " << conclusion << "\n"; + if (d_resChains.hasGenerator(conclusion)) + { + Trace("sat-proof") + << "SatProofManager::endResChain: skip repeated proof of " << conclusion + << "\n"; + // clearing + d_resLinks.clear(); + d_redundantLits.clear(); + return; + } // first process redundant literals std::set<SatLiteral> visited; unsigned pos = d_resLinks.size(); @@ -240,11 +250,6 @@ void SatProofManager::endResChain(Node conclusion, return; } } - if (Trace.isOn("sat-proof") && d_resChains.hasGenerator(conclusion)) - { - Trace("sat-proof") << "SatProofManager::endResChain: replacing proof of " - << conclusion << "\n"; - } // since the conclusion can be both reordered and without duplicates and the // SAT solver does not record this information, we use a MACRO_RESOLUTION // step, which bypasses these. Note that we could generate a chain resolution @@ -252,7 +257,7 @@ void SatProofManager::endResChain(Node conclusion, // post-processing. ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args); // note that we must tell the proof generator to overwrite if repeated - d_resChainPg.addStep(conclusion, ps, CDPOverwrite::ALWAYS); + d_resChainPg.addStep(conclusion, ps); // the premises of this resolution may not have been justified yet, so we do // not pass assumptions to check closedness d_resChains.addLazyStep(conclusion, &d_resChainPg); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 205729553..db6a7ae48 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -829,7 +829,9 @@ set(regress_0_tests regress0/printer/tuples_and_records.cvc regress0/proofs/cyclic-ucp.smt2 regress0/proofs/issue277-circuit-propagator.smt2 + regress0/proofs/open-pf-datatypes.smt2 regress0/proofs/open-pf-if-unordered-iff.smt2 + regress0/proofs/open-pf-rederivation.smt2 regress0/proofs/scope.smt2 regress0/proofs/trust-subs-eq-open.smt2 regress0/push-pop/boolean/fuzz_12.smt2 diff --git a/test/regress/regress0/proofs/open-pf-datatypes.smt2 b/test/regress/regress0/proofs/open-pf-datatypes.smt2 new file mode 100644 index 000000000..24d20bfd8 --- /dev/null +++ b/test/regress/regress0/proofs/open-pf-datatypes.smt2 @@ -0,0 +1,11 @@ +; EXPECT: unsat +(set-logic ALL) +(declare-datatypes ((C 0)) (((r) (b)))) +(declare-datatypes ((P 0)) (((a (f C) (s C))))) +(declare-fun p () P) +(declare-fun p2 () P) +(declare-fun p3 () P) +(declare-fun p4 () P) +(declare-fun p5 () P) +(assert (distinct p p2 p3 p4 p5)) +(check-sat) diff --git a/test/regress/regress0/proofs/open-pf-rederivation.smt2 b/test/regress/regress0/proofs/open-pf-rederivation.smt2 new file mode 100644 index 000000000..7095ec942 --- /dev/null +++ b/test/regress/regress0/proofs/open-pf-rederivation.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --bv-solver=simple +; EXPECT: unsat +(set-logic ALL) +(declare-const __ (_ BitVec 7)) +(assert (bvule ((_ zero_extend 31) ((_ zero_extend 16) ((_ zero_extend 8) __))) ((_ zero_extend 30) ((_ zero_extend 1) ((_ zero_extend 16) ((_ zero_extend 8) __)))))) +(check-sat-assuming ((not (bvule (bvsub ((_ zero_extend 32) ((_ zero_extend 1) ((_ zero_extend 16) ((_ zero_extend 8) __)))) (_ bv1 64)) (bvsub ((_ zero_extend 1) ((_ zero_extend 1) ((_ zero_extend 31) ((_ zero_extend 16) ((_ zero_extend 8) __))))) (_ bv1 64)))))) |