A few proof bugs fixed

diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index 484bc70c80407c30c5720ad658af77529b25ae7b..18e01728b4cc0dee126084fdf746b985abc5b20f 100644 (file)
--- 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 d12b561a64d30e92961bfb652fd6b9476189cd50..f0f333598d0045e116f088921244526aa04a7f88 100644 (file)
--- 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());

diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp
index 6dfd141572a7d624eb2de8ef82c33668abdb720c..8dd7fe782ef7166e4fbddaea6229b56b938a79de 100644 (file)
--- a/src/theory/arrays/array_proof_reconstruction.cpp
+++ b/src/theory/arrays/array_proof_reconstruction.cpp
@@ -60,7 +60,7 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a,
     // or ((a[i]:=t)[k] == a[k]) because (i != k).
 
     if (proof) {
-      if (a.getNumChildren() == 2) {
+      if (a.getKind() == kind::SELECT) {
         // This is the case of ((a[i]:=t)[k] == a[k]) because (i != k).
 
         // The edge is ((a[i]:=t)[k], a[k]), or (a[k], (a[i]:=t)[k]). This flag should be
@@ -156,7 +156,7 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a,
 
         proof->d_children.push_back(childProof);
       } else {
-        // This is the case of  (i == k) because ((a[i]:=t)[k] != a[k]),
+        // This is the case of (i == k) because ((a[i]:=t)[k] != a[k]),
 
         Node indexOne = a;
         Node indexTwo = b;

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 25b12f75f048d31f1ea66c7a8d174d56a0da6a6f..09d348584ca3476665c855311ff7976953b0b251 100644 (file)
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -393,7 +393,7 @@ const EqualityNode& EqualityEngine::getEqualityNode(EqualityNodeId nodeId) const
 
 void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, unsigned pid) {
 
-  Debug("equality") << d_name << "::eq::addEqualityInternal(" << t1 << "," << t2 << "), pid = " << pid << std::endl;
+  Debug("equality") << d_name << "::eq::addEqualityInternal(" << t1 << "," << t2 << "), reason = " << reason << ", pid = " << pid << std::endl;
 
   if (d_done) {
     return;
@@ -1204,7 +1204,6 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               Debug("equality") << d_name << "::eq::getExplanation(): adding: "
                                 << reason << std::endl;
               Debug("equality") << d_name << "::eq::getExplanation(): reason type = " << reasonType << std::endl;
-
               Node a = d_nodes[currentNode];
               Node b = d_nodes[d_equalityEdges[currentEdge].getNodeId()];