From: Haniel Barbosa Date: Wed, 14 Jul 2021 23:02:30 +0000 (-0300) Subject: [proof] Fix open proof issues in SAT proof (#6887) X-Git-Tag: cvc5-1.0.0~1486 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e3cd14dcc00eddef1238dce4e9c90be18858bb73;p=cvc5.git [proof] Fix open proof issues in SAT proof (#6887) Commit d1eee40cc (PR #6346), in a foolish attempt to prevent speculated issues, introduced an overwriting policy to addition of resolution chains during SAT solving at the SAT proof manager. First, this is nonsensical because the lazy proof chain is context-dependent and at the same level other ways of proving that clause are simply redundant and therefore should be ignored. Second, and catastrophically, this policy, for reasons beyond me, can lead to open SAT proofs when the same clause is rederived at the same level. So this commit simply reverts the change and adds an optimization that when the clause would be rederived at the same level we do nothing and leave the method. --- 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& 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 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))))))