A few proof bugs fixed

2 files changed, 101 insertions, 23 deletions

diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index 484bc70c8..18e01728b 100644
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -637,6 +637,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       //       we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs
       //       b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof,
       //       and use it to determine which option we need.
+
       if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) {
         if (((n1[0] == n2[0]) && (n1[1] == n2[1])) || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) {
           // We are in a sequence of identical equalities
@@ -900,7 +901,6 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       // inner index != outer index
       // t3 is the outer index
 
-
       Assert(pf->d_children.size() == 1);
       std::stringstream ss;
       Node subproof = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map);
@@ -915,22 +915,76 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       tp->printTerm(t4.toExpr(), out, map);
       out << " ";
 
+
       Debug("pf::array") << "pf->d_children[0]->d_node is: " << pf->d_children[0]->d_node
                          << ". t3 is: " << t3 << std::endl
                          << "subproof is: " << subproof << std::endl;
 
       Debug("pf::array") << "Subproof is: " << ss.str() << std::endl;
 
-      if (subproof[0][1] == t3) {
-        Debug("pf::array") << "Dont need symmetry!" << std::endl;
-        out << ss.str();
+      // The subproof needs to show that t2 != t3. This can either be a direct disequality,
+      // or, if (wlog) t2 is constant, it can show that t3 is equal to another constant.
+      if (subproof.getKind() == kind::NOT) {
+        // The subproof is for t2 != t3 (or t3 != t2)
+        if (subproof[0][1] == t3) {
+          Debug("pf::array") << "Dont need symmetry!" << std::endl;
+          out << ss.str();
+        } else {
+          Debug("pf::array") << "Need symmetry!" << std::endl;
+          out << "(negsymm _ _ _ " << ss.str() << ")";
+        }
       } else {
-        Debug("pf::array") << "Need symmetry!" << std::endl;
-        out << "(negsymm _ _ _ " << ss.str() << ")";
+        // Either t2 or t3 is a constant.
+        Assert(subproof.getKind() == kind::EQUAL);
+        Assert(subproof[0].isConst() || subproof[1].isConst());
+        Assert(t2.isConst() || t3.isConst());
+        Assert(!(t2.isConst() && t3.isConst()));
+
+        bool t2IsConst = t2.isConst();
+        if (subproof[0].isConst()) {
+          if (t2IsConst) {
+            // (t3 == subproof[1]) == subproof[0] != t2
+            // goal is t2 != t3
+            // subproof already shows constant = t3
+            Assert(t3 == subproof[1]);
+            out << "(negtrans _ _ _ _ ";
+            tp->printConstantDisequalityProof(out, t2.toExpr(), subproof[0].toExpr());
+            out << " ";
+            out << ss.str();
+            out << ")";
+          } else {
+            Assert(t2 == subproof[1]);
+            out << "(negsymm _ _ _ ";
+            out << "(negtrans _ _ _ _ ";
+            tp->printConstantDisequalityProof(out, t3.toExpr(), subproof[0].toExpr());
+            out << " ";
+            out << ss.str();
+            out << "))";
+          }
+        } else {
+          if (t2IsConst) {
+            // (t3 == subproof[0]) == subproof[1] != t2
+            // goal is t2 != t3
+            // subproof already shows constant = t3
+            Assert(t3 == subproof[0]);
+            out << "(negtrans _ _ _ _ ";
+            tp->printConstantDisequalityProof(out, t2.toExpr(), subproof[1].toExpr());
+            out << " ";
+            out << "(symm _ _ _ " << ss.str() << ")";
+            out << ")";
+          } else {
+            Assert(t2 == subproof[0]);
+            out << "(negsymm _ _ _ ";
+            out << "(negtrans _ _ _ _ ";
+            tp->printConstantDisequalityProof(out, t3.toExpr(), subproof[1].toExpr());
+            out << " ";
+            out << "(symm _ _ _ " << ss.str() << ")";
+            out << "))";
+          }
+        }
       }
 
       out << ")";
-
       return ret;
     } else {
       Debug("pf::array") << "In the case of NEGATIVE ROW" << std::endl;
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index d12b561a6..f0f333598 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -135,17 +135,17 @@ void TheoryProofEngine::printConstantDisequalityProof(std::ostream& os, Expr c1,
 }
 
 void TheoryProofEngine::registerTerm(Expr term) {
-  Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering term: " << term << std::endl;
+  Debug("pf::tp::register") << "TheoryProofEngine::registerTerm: registering term: " << term << std::endl;
 
   if (d_registrationCache.count(term)) {
     return;
   }
 
-  Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering NEW term: " << term << std::endl;
+  Debug("pf::tp::register") << "TheoryProofEngine::registerTerm: registering NEW term: " << term << std::endl;
 
   theory::TheoryId theory_id = theory::Theory::theoryOf(term);
 
-  Debug("pf::tp") << "Term's theory( " << term << " ) = " << theory_id << std::endl;
+  Debug("pf::tp::register") << "Term's theory( " << term << " ) = " << theory_id << std::endl;
 
   // don't need to register boolean terms
   if (theory_id == theory::THEORY_BUILTIN ||
@@ -165,7 +165,7 @@ void TheoryProofEngine::registerTerm(Expr term) {
   // A special case: the array theory needs to know of every skolem, even if
   // it belongs to another theory (e.g., a BV skolem)
   if (ProofManager::getSkolemizationManager()->isSkolem(term) && theory_id != theory::THEORY_ARRAY) {
-    Debug("pf::tp") << "TheoryProofEngine::registerTerm: Special case: registering a non-array skolem: " << term << std::endl;
+    Debug("pf::tp::register") << "TheoryProofEngine::registerTerm: registering a non-array skolem: " << term << std::endl;
     getTheoryProof(theory::THEORY_ARRAY)->registerTerm(term);
   }
 
@@ -632,15 +632,27 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
         clause_expr[k] = missingAssertion->toExpr();
 
         std::ostringstream rewritten;
-        rewritten << "(or_elim_1 _ _ ";
-        rewritten << "(not_not_intro _ ";
-        rewritten << pm->getLitName(explanation);
-        rewritten << ") (iff_elim_1 _ _ ";
-        rewritten << d_assertionToRewrite[missingAssertion->negate()];
-        rewritten << "))";
+
+        if (missingAssertion->getKind() == kind::NOT && (*missingAssertion)[0].toExpr() == utils::mkFalse()) {
+          rewritten << "(or_elim_2 _ _ ";
+          rewritten << "(not_not_intro _ ";
+          rewritten << pm->getLitName(explanation);
+          rewritten << ") (iff_elim_2 _ _ ";
+          rewritten << d_assertionToRewrite[missingAssertion->negate()];
+          rewritten << "))";
+        }
+        else {
+          rewritten << "(or_elim_1 _ _ ";
+          rewritten << "(not_not_intro _ ";
+          rewritten << pm->getLitName(explanation);
+          rewritten << ") (iff_elim_1 _ _ ";
+          rewritten << d_assertionToRewrite[missingAssertion->negate()];
+          rewritten << "))";
+        }
 
         Debug("pf::tp") << "Setting a rewrite filter for this proof: " << std::endl
                         << pm->getLitName(*missingAssertion) << " --> " << rewritten.str()
+                        << ", explanation = " << explanation
                         << std::endl << std::endl;
 
         pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str());
@@ -742,15 +754,27 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
           currentClauseExpr[k] = missingAssertion->toExpr();
 
           std::ostringstream rewritten;
-          rewritten << "(or_elim_1 _ _ ";
-          rewritten << "(not_not_intro _ ";
-          rewritten << pm->getLitName(explanation);
-          rewritten << ") (iff_elim_1 _ _ ";
-          rewritten << d_assertionToRewrite[missingAssertion->negate()];
-          rewritten << "))";
+
+          if (missingAssertion->getKind() == kind::NOT && (*missingAssertion)[0].toExpr() == utils::mkFalse()) {
+            rewritten << "(or_elim_2 _ _ ";
+            rewritten << "(not_not_intro _ ";
+            rewritten << pm->getLitName(explanation);
+            rewritten << ") (iff_elim_2 _ _ ";
+            rewritten << d_assertionToRewrite[missingAssertion->negate()];
+            rewritten << "))";
+          }
+          else {
+            rewritten << "(or_elim_1 _ _ ";
+            rewritten << "(not_not_intro _ ";
+            rewritten << pm->getLitName(explanation);
+            rewritten << ") (iff_elim_1 _ _ ";
+            rewritten << d_assertionToRewrite[missingAssertion->negate()];
+            rewritten << "))";
+          }
 
           Debug("pf::tp") << "Setting a rewrite filter for this proof: " << std::endl
                           << pm->getLitName(*missingAssertion) << " --> " << rewritten.str()
+                          << "explanation = " << explanation
                           << std::endl << std::endl;
 
           pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str());