diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-02-03 12:11:26 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-03 09:11:26 -0600 |
commit | a6c122da21b3d5b9c37d9ec670dec766eaff7001 (patch) | |
tree | b5586c3fcc7dd18a6304464cb5a5611bb2709a1c /src/smt/proof_post_processor.cpp | |
parent | d97cee1a7c1a688d1ad9c748247bd9da1d86973f (diff) |
[proof-new] Fix MACRO_RESOLUTION expansion for singleton clause corner case (#5850)
Evaluating the proof infrastructure in SMT-LIB has uncovered a rare case (i.e., not previously in our regressions!!) in which the resulting clause from crowding literal elimination is a singleton. This commit makes the expansion code robust to that and adds an example of a problematic benchmark as a regression.
Also improves a bit tracing and some comments.
Diffstat (limited to 'src/smt/proof_post_processor.cpp')
-rw-r--r-- | src/smt/proof_post_processor.cpp | 38 |
1 files changed, 28 insertions, 10 deletions
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 4b1a05e0f..ab8dd8f92 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -137,6 +137,7 @@ Node ProofPostprocessCallback::eliminateCrowdingLits( const std::vector<Node>& args, CDProof* cdp) { + Trace("smt-proof-pp-debug2") << push; NodeManager* nm = NodeManager::currentNM(); Node trueNode = nm->mkConst(true); // get crowding lits and the position of the last clause that includes @@ -164,10 +165,10 @@ Node ProofPostprocessCallback::eliminateCrowdingLits( size_t j; for (j = children.size() - 1; j > 0; --j) { - // notice that only non-unit clauses may be introducing the crowding - // literal, so we only care about non-unit OR nodes. We check then - // against the kind and whether the whole OR node occurs as a pivot of - // the respective resolution + // notice that only non-singleton clauses may be introducing the + // crowding literal, so we only care about non-singleton OR nodes. We + // check then against the kind and whether the whole OR node occurs as a + // pivot of the respective resolution if (children[j - 1].getKind() != kind::OR) { continue; @@ -376,6 +377,7 @@ Node ProofPostprocessCallback::eliminateCrowdingLits( Trace("smt-proof-pp-debug2") << "nextGuardedElimPos: " << nextGuardedElimPos << "\n"; } while (true); + Trace("smt-proof-pp-debug2") << pop; return lastClause; } @@ -659,10 +661,10 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, chainConclusion.end()}; std::set<Node> chainConclusionLitsSet{chainConclusion.begin(), chainConclusion.end()}; - // is args[0] a unit clause? If it's not an OR node, then yes. Otherwise, - // it's only a unit if it occurs in chainConclusionLitsSet + // is args[0] a singleton clause? If it's not an OR node, then yes. + // Otherwise, it's only a singleton if it occurs in chainConclusionLitsSet std::vector<Node> conclusionLits; - // whether conclusion is unit + // whether conclusion is singleton if (chainConclusionLitsSet.count(args[0])) { conclusionLits.push_back(args[0]); @@ -684,16 +686,32 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, chainConclusionLits, conclusionLits, children, args, cdp); // update vector of lits. Note that the set is no longer used, so we don't // need to update it + // + // We need again to check whether chainConclusion is a singleton + // clause. As above, it's a singleton if it's in the original + // chainConclusionLitsSet. chainConclusionLits.clear(); - chainConclusionLits.insert(chainConclusionLits.end(), - chainConclusion.begin(), - chainConclusion.end()); + if (chainConclusionLitsSet.count(chainConclusion)) + { + chainConclusionLits.push_back(chainConclusion); + } + else + { + Assert(chainConclusion.getKind() == kind::OR); + chainConclusionLits.insert(chainConclusionLits.end(), + chainConclusion.begin(), + chainConclusion.end()); + } } else { cdp->addStep( chainConclusion, PfRule::CHAIN_RESOLUTION, children, chainResArgs); } + Trace("smt-proof-pp-debug") + << "Conclusion after chain_res/elimCrowd: " << chainConclusion << "\n"; + Trace("smt-proof-pp-debug") + << "Conclusion lits: " << chainConclusionLits << "\n"; // Placeholder for running conclusion Node n = chainConclusion; // factoring |