From afc01bf9df9a36b6c8f83ff9706cfa349da8d24a Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 18 May 2020 16:56:25 -0500 Subject: Connect explained conflicts --- src/theory/theory_engine.cpp | 22 +++++++++++++++++++--- src/theory/theory_engine_proof_generator.cpp | 2 ++ src/theory/trust_node.cpp | 2 +- 3 files changed, 22 insertions(+), 4 deletions(-) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 982931d4a..3b6ffd6de 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1937,15 +1937,31 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp)); // Process the explanation - TrustNode tnc = getExplanation(vec, proofRecipe); + TrustNode tncExp = getExplanation(vec, proofRecipe); PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe)); + Node fullConflict = tncExp.getNode(); - // FIXME: have ~( F ) and E => F, prove ~( E ) if (d_lazyProof != nullptr) { + if (fullConflict!=conflict) + { + // store the explicit step + processTrustNode(tncExp, THEORY_BUILTIN); + } + Node fullConflictNeg = fullConflict.notNode(); + // ------------------------- explained ---------- from theory + // fullConflict => conflict ~conflict + // ----------------------------------------------- MACRO_SR_PRED_TRANSFORM + // ~fullConflict + std::vector children; + children.push_back(tncExp.getProven()); + children.push_back(conflict.notNode()); + std::vector args; + args.push_back(fullConflictNeg); + args.push_back(mkMethodId(MethodId::SB_PREDICATE)); + d_lazyProof->addStep(fullConflictNeg, PfRule::MACRO_SR_PRED_TRANSFORM, children, args); } - Node fullConflict = tnc.getNode(); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; Assert(properConflict(fullConflict)); lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST); diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp index 144fe0cc2..c11378e04 100644 --- a/src/theory/theory_engine_proof_generator.cpp +++ b/src/theory/theory_engine_proof_generator.cpp @@ -29,6 +29,7 @@ theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain( { theory::TrustNode trn = theory::TrustNode::mkTrustPropExp(lit, exp, this); Node p = trn.getProven(); + Assert(p.getKind() == IMPLIES && p.getNumChildren() == 2); // should not already be proven NodeLazyCDProofMap::iterator it = d_proofs.find(p); if (it != d_proofs.end()) @@ -45,6 +46,7 @@ theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain( std::shared_ptr TheoryEngineProofGenerator::getProofFor(Node f) { + // should only ask this generator for proofs of implications Assert(f.getKind() == IMPLIES && f.getNumChildren() == 2); NodeLazyCDProofMap::iterator it = d_proofs.find(f); if (it == d_proofs.end()) diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp index 8cb2a1f95..ff3e89154 100644 --- a/src/theory/trust_node.cpp +++ b/src/theory/trust_node.cpp @@ -83,7 +83,7 @@ ProofGenerator* TrustNode::getGenerator() const { return d_gen; } bool TrustNode::isNull() const { return d_proven.isNull(); } -Node TrustNode::getConflictProven(Node conf) { return conf.negate(); } +Node TrustNode::getConflictProven(Node conf) { return conf.notNode(); } Node TrustNode::getLemmaProven(Node lem) { return lem; } -- cgit v1.2.3