Propagate the usage of proof let maps into constant disequality proofs

4 files changed, 17 insertions, 23 deletions

diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index 63758e573..ccc072eca 100644
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -305,7 +305,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       out << " ";
       ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out,
                                                                           n1[0].toExpr(),
-                                                                          n1[1].toExpr());
+                                                                          n1[1].toExpr(),
+                                                                          map);
     }
 
     out << "))" << std::endl;
@@ -585,7 +586,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
 
     ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out,
                                                                         n[0].toExpr(),
-                                                                        n[1].toExpr());
+                                                                        n[1].toExpr(),
+                                                                        map);
     return pf->d_node;
   }
 
@@ -948,7 +950,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
             // subproof already shows constant = t3
             Assert(t3 == subproof[1]);
             out << "(negtrans _ _ _ _ ";
-            tp->printConstantDisequalityProof(out, t2.toExpr(), subproof[0].toExpr());
+            tp->printConstantDisequalityProof(out, t2.toExpr(), subproof[0].toExpr(), map);
             out << " ";
             out << ss.str();
             out << ")";
@@ -956,7 +958,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
             Assert(t2 == subproof[1]);
             out << "(negsymm _ _ _ ";
             out << "(negtrans _ _ _ _ ";
-            tp->printConstantDisequalityProof(out, t3.toExpr(), subproof[0].toExpr());
+            tp->printConstantDisequalityProof(out, t3.toExpr(), subproof[0].toExpr(), map);
             out << " ";
             out << ss.str();
             out << "))";
@@ -968,7 +970,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
             // subproof already shows constant = t3
             Assert(t3 == subproof[0]);
             out << "(negtrans _ _ _ _ ";
-            tp->printConstantDisequalityProof(out, t2.toExpr(), subproof[1].toExpr());
+            tp->printConstantDisequalityProof(out, t2.toExpr(), subproof[1].toExpr(), map);
             out << " ";
             out << "(symm _ _ _ " << ss.str() << ")";
             out << ")";
@@ -976,7 +978,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
             Assert(t2 == subproof[0]);
             out << "(negsymm _ _ _ ";
             out << "(negtrans _ _ _ _ ";
-            tp->printConstantDisequalityProof(out, t3.toExpr(), subproof[1].toExpr());
+            tp->printConstantDisequalityProof(out, t3.toExpr(), subproof[1].toExpr(), map);
             out << " ";
             out << "(symm _ _ _ " << ss.str() << ")";
             out << "))";
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 8c74d0c2c..9753844a1 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -126,12 +126,12 @@ void TheoryProofEngine::markTermForFutureRegistration(Expr term, theory::TheoryI
   d_exprToTheoryIds[term].insert(id);
 }
 
-void TheoryProofEngine::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) {
+void TheoryProofEngine::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) {
   Assert(c1.isConst());
   Assert(c2.isConst());
 
   Assert(theory::Theory::theoryOf(c1) == theory::Theory::theoryOf(c2));
-  getTheoryProof(theory::Theory::theoryOf(c1))->printConstantDisequalityProof(os, c1, c2);
+  getTheoryProof(theory::Theory::theoryOf(c1))->printConstantDisequalityProof(os, c1, c2, globalLetMap);
 }
 
 void TheoryProofEngine::registerTerm(Expr term) {
@@ -992,13 +992,6 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
     Assert(!oc.d_lemma.isNull());
     Trace("pf::tp") << "; ++ but got lemma: " << oc.d_lemma << std::endl;
 
-    // Original, as in Liana's branch
-    // Trace("pf::tp") << "; asserting " << oc.d_lemma[1].negate() << std::endl;
-    // th->assertFact(oc.d_lemma[1].negate(), false);
-    // th->check(theory::Theory::EFFORT_FULL);
-
-    // Altered version, to handle OR lemmas
-
     if (oc.d_lemma.getKind() == kind::OR) {
       Debug("pf::tp") << "OR lemma. Negating each child separately" << std::endl;
       for (unsigned i = 0; i < oc.d_lemma.getNumChildren(); ++i) {
@@ -1087,7 +1080,7 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLe
       }
 
       // The let map should already have the current expression.
-      ProofLetMap::const_iterator it = map.find(currentExpression.toExpr());
+      ProofLetMap::const_iterator it = map.find(term);
       if (it != map.end()) {
         unsigned id = it->second.id;
         unsigned count = it->second.count;
@@ -1178,15 +1171,14 @@ void LFSCBooleanProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
   Unreachable("No boolean lemmas yet!");
 }
 
-void TheoryProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) {
+void TheoryProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) {
   // By default, we just print a trust statement. Specific theories can implement
   // better proofs.
-  ProofLetMap emptyMap;
 
   os << "(trust_f (not (= _ ";
-  d_proofEngine->printBoundTerm(c1, os, emptyMap);
+  d_proofEngine->printBoundTerm(c1, os, globalLetMap);
   os << " ";
-  d_proofEngine->printBoundTerm(c2, os, emptyMap);
+  d_proofEngine->printBoundTerm(c2, os, globalLetMap);
   os << ")))";
 }
 
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 968d46e68..c622fabee 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -149,7 +149,7 @@ public:
 
   void markTermForFutureRegistration(Expr term, theory::TheoryId id);
 
-  void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2);
+  void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
 
   virtual void treatBoolsAsFormulas(bool value) {};
 
@@ -286,7 +286,7 @@ public:
    *
    * @param term
    */
-  virtual void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2);
+  virtual void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
   /**
    * Print a proof for the equivalence of n1 and n2.
    *
diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index e122a46bc..17faf0f7d 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -264,7 +264,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
 
       out << ss.str();
       out << " ";
-      ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, n1[0].toExpr(), n1[1].toExpr());
+      ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, n1[0].toExpr(), n1[1].toExpr(), map);
       out << "))" << std::endl;
     }