better support for proof production when encountering bool terms: handle the new proof constructs generated by the equality engine.

proof production for bool-array.smt2 passes

1 files changed, 71 insertions, 38 deletions

diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index c38fa1403..cea873b6d 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -1,22 +1,23 @@
 /*********************                                                        */
 /*! \file uf_proof.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Liana Hadarean, Guy Katz
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** [[ Add lengthier description here ]]
-
- ** \todo document this file
+** \verbatim
+** Top contributors (to current version):
+**   Liana Hadarean, Guy Katz
+** This file is part of the CVC4 project.
+** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+** in the top-level source directory) and their institutional affiliations.
+** All rights reserved.  See the file COPYING in the top-level source
+** directory for licensing information.\endverbatim
+**
+** [[ Add lengthier description here ]]
+
+** \todo document this file
 
 **/
 
-#include "proof/theory_proof.h"
 #include "proof/proof_manager.h"
+#include "proof/simplify_boolean_node.h"
+#include "proof/theory_proof.h"
 #include "proof/uf_proof.h"
 #include "theory/uf/theory_uf.h"
 #include <stack>
@@ -110,10 +111,14 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
     subTrans.d_node = pf->d_node;
 
     size_t i = 0;
+
     while (i < pf->d_children.size()) {
+      pf->d_children[i]->d_node = simplifyBooleanNode(pf->d_children[i]->d_node);
+
       // Look for the negative clause, with which we will form a contradiction.
       if(!pf->d_children[i]->d_node.isNull() && pf->d_children[i]->d_node.getKind() == kind::NOT) {
         Assert(neg < 0);
+        Node node = pf->d_children[i]->d_node[0];
         neg = i;
         ++i;
       }
@@ -128,8 +133,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
         Debug("pf::uf") << "Collecting congruence sequence" << std::endl;
         for (count = 0;
              i + count < pf->d_children.size() &&
-             pf->d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE &&
-             pf->d_children[i + count]->d_node.isNull();
+               pf->d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE &&
+               pf->d_children[i + count]->d_node.isNull();
              ++count) {
           Debug("pf::uf") << "Found a congruence: " << std::endl;
           pf->d_children[i+count]->debug_print("pf::uf");
@@ -154,13 +159,16 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
           targetAppearsAfter = false;
         }
 
-        // Assert that we have precisely one target clause.
-        Assert(targetAppearsBefore != targetAppearsAfter);
+        // Assert that we have precisely at least one possible clause.
+        Assert(targetAppearsBefore || targetAppearsAfter);
+
+        // If both are valid, assume the one after the sequence is correct
+        if (targetAppearsAfter && targetAppearsBefore)
+          targetAppearsBefore = false;
 
         // Begin breaking up the congruences and ordering the equalities correctly.
         std::vector<theory::eq::EqProof *> orderedEqualities;
 
-
         // Insert target clause first.
         if (targetAppearsBefore) {
           orderedEqualities.push_back(pf->d_children[i - 1]);
@@ -176,7 +184,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
             if (pf->d_children[i + j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
               orderedEqualities.insert(orderedEqualities.begin(), pf->d_children[i + j]->d_children[0]);
             if (pf->d_children[i + j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-            orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + j]->d_children[1]);
+              orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + j]->d_children[1]);
           }
         } else {
           for (unsigned j = 0; j < count; ++j) {
@@ -231,6 +239,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
     if (disequalityFound) {
       Node n2 = pf->d_children[neg]->d_node;
       Assert(n2.getKind() == kind::NOT);
+
       Debug("pf::uf") << "n2 is " << n2[0] << std::endl;
 
       if (n2[0].getNumChildren() > 0) { Debug("pf::uf") << "\nn2[0]: " << n2[0][0] << std::endl; }
@@ -248,6 +257,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
           out << ss.str();
         }
         out << "(pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl;
+      } else if (n2[0].getKind() == kind::BOOLEAN_TERM_VARIABLE) {
+        out << ss.str() << " " << ProofManager::getLitName(n2[0]) << "))";
       } else {
         Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1]));
         if(n1[1] == n2[0][0]) {
@@ -308,8 +319,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
       Debug("pf::uf") << "SIDE IS 1\n";
       //}
       if(!match(pf2->d_node, n1[1])) {
-      Debug("pf::uf") << "IN BAD CASE, our first subproof is\n";
-      pf2->d_children[0]->debug_print("pf::uf");
+        Debug("pf::uf") << "IN BAD CASE, our first subproof is\n";
+        pf2->d_children[0]->debug_print("pf::uf");
       }
       Assert(match(pf2->d_node, n1[1]));
       side = 1;
@@ -352,7 +363,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
     out << ")";
     while(!stk.empty()) {
       if(tb == 1) {
-      Debug("pf::uf") << "\nMORE TO DO\n";
+        Debug("pf::uf") << "\nMORE TO DO\n";
       }
       pf2 = stk.top();
       stk.pop();
@@ -410,7 +421,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
     }
     Node n = (side == 0 ? eqNode(n1, n2) : eqNode(n2, n1));
     if(tb == 1) {
-    Debug("pf::uf") << "\ncong proved: " << n << "\n";
+      Debug("pf::uf") << "\ncong proved: " << n << "\n";
     }
     return n;
   }
@@ -436,6 +447,9 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
     Debug("pf::uf") << "\ndoing trans proof[[\n";
     pf->debug_print("pf::uf");
     Debug("pf::uf") << "\n";
+
+    pf->d_children[0]->d_node = simplifyBooleanNode(pf->d_children[0]->d_node);
+
     Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map);
     Debug("pf::uf") << "\ndoing trans proof, got n1 " << n1 << "\n";
     if(tb == 1) {
@@ -452,6 +466,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
       std::stringstream ss1(ss.str()), ss2;
       ss.str("");
 
+      pf->d_children[i]->d_node = simplifyBooleanNode(pf->d_children[i]->d_node);
+
       // It is possible that we've already converted the i'th child to stream. If so,
       // use previously stored result. Otherwise, convert and store.
       Node n2;
@@ -524,7 +540,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
                   ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str();
                 } else {
                   Debug("pf::uf") << "Error: identical equalities over, but hands don't match what we're proving."
-                                     << std::endl;
+                                  << std::endl;
                   Assert(false);
                 }
               } else {
@@ -595,18 +611,18 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
         // Both elements of the transitivity rule are equalities/iffs
       {
         if(n1[0] == n2[0]) {
-            if(tb == 1) { Debug("pf::uf") << "case 1\n"; }
-            n1 = eqNode(n1[1], n2[1]);
-            ss << "(symm _ _ _ " << ss1.str() << ") " << ss2.str();
+          if(tb == 1) { Debug("pf::uf") << "case 1\n"; }
+          n1 = eqNode(n1[1], n2[1]);
+          ss << "(symm _ _ _ " << ss1.str() << ") " << ss2.str();
         } else if(n1[1] == n2[1]) {
           if(tb == 1) { Debug("pf::uf") << "case 2\n"; }
           n1 = eqNode(n1[0], n2[0]);
           ss << ss1.str() << " (symm _ _ _ " << ss2.str() << ")";
         } else if(n1[0] == n2[1]) {
-            if(tb == 1) { Debug("pf::uf") << "case 3\n"; }
-            n1 = eqNode(n2[0], n1[1]);
-            ss << ss2.str() << " " << ss1.str();
-            if(tb == 1) { Debug("pf::uf") << "++ proved " << n1 << "\n"; }
+          if(tb == 1) { Debug("pf::uf") << "case 3\n"; }
+          n1 = eqNode(n2[0], n1[1]);
+          ss << ss2.str() << " " << ss1.str();
+          if(tb == 1) { Debug("pf::uf") << "++ proved " << n1 << "\n"; }
         } else if(n1[1] == n2[0]) {
           if(tb == 1) { Debug("pf::uf") << "case 4\n"; }
           n1 = eqNode(n1[0], n2[1]);
@@ -646,9 +662,6 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
       } else {
         // Both n1 and n2 are predicates.
         // We want to prove b1 = b2, and we know that ((b1), (b2)) or ((not b1), (not b2))
-        Debug("gk::temp") << "Two-predicate case. pf->d_node = " << pf->d_node
-                          << ", n1 = " << n1 << ", n2 = " << n2 << std::endl;
-
         if (n1.getKind() == kind::NOT) {
           Assert(n2.getKind() == kind::NOT);
           Assert(pf->d_node[0] == n1[0] || pf->d_node[0] == n2[0]);
@@ -687,7 +700,6 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
 
       ss << ")";
     }
-
     out << ss.str();
     Debug("pf::uf") << "\n++ trans proof done, have proven " << n1 << std::endl;
     return n1;
@@ -724,6 +736,14 @@ void UFProof::registerTerm(Expr term) {
 
   if (term.isVariable()) {
     d_declarations.insert(term);
+
+
+    if (term.getKind() == kind::BOOLEAN_TERM_VARIABLE) {
+      // Ensure cnf literals
+      Node asNode(term);
+      ProofManager::currentPM()->ensureLiteral(eqNode(term, NodeManager::currentNM()->mkConst(true)));
+      ProofManager::currentPM()->ensureLiteral(eqNode(term, NodeManager::currentNM()->mkConst(false)));
+    }
   }
 
   // recursively declare all other terms
@@ -756,6 +776,7 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap&
   }
   os << func << " ";
   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
+
     bool convertToBool = (term[i].getType().isBoolean() && !d_proofEngine->printsAsBool(term[i]));
     if (convertToBool) os << "(f_to_b ";
     d_proofEngine->printBoundTerm(term[i], os, map);
@@ -839,13 +860,25 @@ void LFSCUFProof::printAliasingDeclarations(std::ostream& os, std::ostream& pare
   // Nothing to do here at this point.
 }
 
-bool LFSCUFProof::printsAsBool(const Node &n)
-{
-  Debug("gk::temp") << "\nUF printsAsBool: " << n << std::endl;
+bool LFSCUFProof::printsAsBool(const Node &n) {
   if (n.getKind() == kind::BOOLEAN_TERM_VARIABLE)
     return true;
 
   return false;
 }
 
+void LFSCUFProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) {
+  Node falseNode = NodeManager::currentNM()->mkConst(false);
+  Node trueNode = NodeManager::currentNM()->mkConst(true);
+
+  Assert(c1 == falseNode.toExpr() || c1 == trueNode.toExpr());
+  Assert(c2 == falseNode.toExpr() || c2 == trueNode.toExpr());
+  Assert(c1 != c2);
+
+  if (c1 == trueNode.toExpr())
+    os << "t_t_neq_f";
+  else
+    os << "(symm _ _ _ t_t_neq_f)";
+}
+
 } /* namespace CVC4 */