Connect explained conflicts

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<Node> children;
+      children.push_back(tncExp.getProven());
+      children.push_back(conflict.notNode());
+      std::vector<Node> 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<ProofNode> 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; }