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

9 files changed, 340 insertions, 40 deletions

diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index af158f37b..6d1bd567d 100644
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -15,9 +15,10 @@
 
 **/
 
-#include "proof/theory_proof.h"
-#include "proof/proof_manager.h"
 #include "proof/array_proof.h"
+#include "proof/proof_manager.h"
+#include "proof/simplify_boolean_node.h"
+#include "proof/theory_proof.h"
 #include "theory/arrays/theory_arrays.h"
 #include <stack>
 
@@ -147,6 +148,9 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
 
     size_t i = 0;
     while (i < pf->d_children.size()) {
+      if (pf->d_children[i]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE)
+        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);
@@ -318,6 +322,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     pf->debug_print("mgd", 0, &d_proofPrinter);
     std::stack<const theory::eq::EqProof*> stk;
     for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) {
+      Debug("mgd") << "Looking at pf2 with d_node: " << pf2->d_node << std::endl;
+
       Assert(!pf2->d_node.isNull());
       Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF ||
              pf2->d_node.getKind() == kind::BUILTIN ||
@@ -601,6 +607,9 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     Debug("mgd") << "\ndoing trans proof[[\n";
     pf->debug_print("mgd", 0, &d_proofPrinter);
     Debug("mgd") << "\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("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n";
     if(tb == 1) {
@@ -617,6 +626,13 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       std::stringstream ss1(ss.str()), ss2;
       ss.str("");
 
+      // In congruences, we can have something like a[x] - it's important to keep these,
+      // and not turn them into (a[x]=true), because that will mess up the congruence application
+      // later.
+
+      if (pf->d_children[i]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE)
+        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;
@@ -1166,6 +1182,13 @@ void ArrayProof::registerTerm(Expr term) {
     d_declarations.insert(term);
   }
 
+  if (term.getKind() == kind::SELECT && term.getType().isBoolean()) {
+    // 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
   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
     // could belong to other theories
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index ddd2029fb..d8eefdcf0 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -243,6 +243,10 @@ std::string ProofManager::getLitName(TNode lit,
   return litName;
 }
 
+bool ProofManager::hasLitName(TNode lit) {
+  return currentPM()->d_cnfProof->hasLiteral(lit);
+}
+
 std::string ProofManager::sanitize(TNode node) {
   Assert (node.isVar() || node.isConst());
 
@@ -875,6 +879,11 @@ void ProofManager::addRewriteFilter(const std::string &original, const std::stri
   d_rewriteFilters[original] = substitute;
 }
 
+bool ProofManager::haveRewriteFilter(TNode lit) {
+  std::string litName = getLitName(currentPM()->d_cnfProof->getLiteral(lit));
+  return d_rewriteFilters.find(litName) != d_rewriteFilters.end();
+}
+
 void ProofManager::clearRewriteFilters() {
   d_rewriteFilters.clear();
 }
@@ -1002,4 +1011,8 @@ void ProofManager::printGlobalLetMap(std::set<Node>& atoms,
   out << std::endl << std::endl;
 }
 
+void ProofManager::ensureLiteral(Node node) {
+  d_cnfProof->ensureLiteral(node);
+}
+
 } /* CVC4  namespace */
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index fa7224d72..19215589f 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -206,6 +206,8 @@ public:
     return d_inputFormulas.find(assertion) != d_inputFormulas.end();
   }
 
+  void ensureLiteral(Node node);
+
 //---from Morgan---
   Node mkOp(TNode n);
   Node lookupOp(TNode n) const;
@@ -230,6 +232,7 @@ public:
   static std::string getAtomName(TNode atom, const std::string& prefix = "");
   static std::string getLitName(prop::SatLiteral lit, const std::string& prefix = "");
   static std::string getLitName(TNode lit, const std::string& prefix = "");
+  static bool hasLitName(TNode lit);
 
   // for SMT variable names that have spaces and other things
   static std::string sanitize(TNode var);
@@ -265,6 +268,7 @@ public:
 
   void addRewriteFilter(const std::string &original, const std::string &substitute);
   void clearRewriteFilters();
+  bool haveRewriteFilter(TNode lit);
 
   void addAssertionFilter(const Node& node, const std::string& rewritten);
 
diff --git a/src/proof/simplify_boolean_node.cpp b/src/proof/simplify_boolean_node.cpp
new file mode 100644
index 000000000..34c3f526d
--- /dev/null
+++ b/src/proof/simplify_boolean_node.cpp
@@ -0,0 +1,183 @@
+/*********************                                                        */
+/*! \file simplify_boolean_node.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   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
+ **
+ ** \brief Simplifying a boolean node, needed for constructing LFSC proofs.
+ **
+ **/
+
+#include "cvc4_private.h"
+
+#include "proof_manager.h"
+
+namespace CVC4 {
+
+inline static Node eqNode(TNode n1, TNode n2) {
+  return NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2);
+}
+
+Node simplifyBooleanNode(const Node &n) {
+  if (n.isNull())
+    return n;
+
+  // Only simplify boolean nodes
+  if (!n.getType().isBoolean())
+    return n;
+
+  // Sometimes we get sent intermediate nodes that we shouldn't simplify.
+  // If a node doesn't have a literal, it's clearly intermediate - ignore.
+  if (!ProofManager::hasLitName(n))
+    return n;
+
+  // If we already simplified the node, ignore.
+  if (ProofManager::currentPM()->haveRewriteFilter(n.negate()))
+    return n;
+
+
+  std::string litName = ProofManager::getLitName(n.negate());
+  Node falseNode = NodeManager::currentNM()->mkConst(false);
+  Node trueNode = NodeManager::currentNM()->mkConst(true);
+  Node simplified = n;
+
+  // (not (= false b)), (not (= true b)))
+  if ((n.getKind() == kind::NOT) && (n[0].getKind() == kind::EQUAL) &&
+      (n[0][0].getKind() == kind::BOOLEAN_TERM_VARIABLE || n[0][1].getKind() == kind::BOOLEAN_TERM_VARIABLE)) {
+    Node lhs = n[0][0];
+    Node rhs = n[0][1];
+
+    if (lhs == falseNode) {
+      Assert(rhs != falseNode);
+      Assert(rhs.getKind() == kind::BOOLEAN_TERM_VARIABLE);
+      // (not (= false b)) --> true = b
+
+      simplified = eqNode(trueNode, rhs);
+
+      std::string simplifiedLitName = ProofManager::getLitName(simplified.negate());
+      std::stringstream newLitName;
+      newLitName << "(pred_not_iff_f _ " << litName << ")";
+      ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str());
+
+    } else if (rhs == falseNode) {
+      Assert(lhs != falseNode);
+      Assert(lhs.getKind() == kind::BOOLEAN_TERM_VARIABLE);
+      // (not (= b false)) --> b = true
+
+      simplified = eqNode(lhs, trueNode);
+      std::string simplifiedLitName = ProofManager::getLitName(simplified.negate());
+      std::stringstream newLitName;
+      newLitName << "(pred_not_iff_f_2 _ " << litName << ")";
+      ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str());
+
+    } else if (lhs == trueNode) {
+      Assert(rhs != trueNode);
+      Assert(rhs.getKind() == kind::BOOLEAN_TERM_VARIABLE);
+      // (not (= true b)) --> b = false
+
+      simplified = eqNode(falseNode, rhs);
+      std::string simplifiedLitName = ProofManager::getLitName(simplified.negate());
+      std::stringstream newLitName;
+      newLitName << "(pred_not_iff_t _ " << litName << ")";
+      ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str());
+
+    } else if (rhs == trueNode) {
+      Assert(lhs != trueNode);
+      Assert(lhs.getKind() == kind::BOOLEAN_TERM_VARIABLE);
+      // (not (= b true)) --> b = false
+
+      simplified = eqNode(lhs, falseNode);
+      std::string simplifiedLitName = ProofManager::getLitName(simplified.negate());
+      std::stringstream newLitName;
+      newLitName << "(pred_not_iff_t_2 _ " << litName << ")";
+      ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str());
+    }
+
+  } else if ((n.getKind() == kind::EQUAL) &&
+             (n[0].getKind() == kind::BOOLEAN_TERM_VARIABLE || n[1].getKind() == kind::BOOLEAN_TERM_VARIABLE)) {
+    Node lhs = n[0];
+    Node rhs = n[1];
+
+    if (lhs == falseNode) {
+      Assert(rhs != falseNode);
+      Assert(rhs.getKind() == kind::BOOLEAN_TERM_VARIABLE);
+      // (= false b)
+
+      std::stringstream newLitName;
+      newLitName << "(pred_iff_f _ " << litName << ")";
+      ProofManager::currentPM()->addRewriteFilter(litName, newLitName.str());
+
+    } else if (rhs == falseNode) {
+      Assert(lhs != falseNode);
+      Assert(lhs.getKind() == kind::BOOLEAN_TERM_VARIABLE);
+      // (= b false))
+
+      std::stringstream newLitName;
+      newLitName << "(pred_iff_f_2 _ " << litName << ")";
+      ProofManager::currentPM()->addRewriteFilter(litName, newLitName.str());
+
+    } else if (lhs == trueNode) {
+      Assert(rhs != trueNode);
+      Assert(rhs.getKind() == kind::BOOLEAN_TERM_VARIABLE);
+      // (= true b)
+
+      std::stringstream newLitName;
+      newLitName << "(pred_iff_t _ " << litName << ")";
+      ProofManager::currentPM()->addRewriteFilter(litName, newLitName.str());
+
+    } else if (rhs == trueNode) {
+      Assert(lhs != trueNode);
+      Assert(lhs.getKind() == kind::BOOLEAN_TERM_VARIABLE);
+      // (= b true)
+
+
+      std::stringstream newLitName;
+      newLitName << "(pred_iff_t_2 _ " << litName << ")";
+      ProofManager::currentPM()->addRewriteFilter(litName, newLitName.str());
+    }
+
+  } else if ((n.getKind() == kind::NOT) && (n[0].getKind() == kind::BOOLEAN_TERM_VARIABLE)) {
+    // (not b) --> b = false
+    simplified = eqNode(n[0], falseNode);
+    std::string simplifiedLitName = ProofManager::getLitName(simplified.negate());
+    std::stringstream newLitName;
+    newLitName << "(pred_eq_f _ " << litName << ")";
+    ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str());
+
+  } else if (n.getKind() == kind::BOOLEAN_TERM_VARIABLE) {
+    // (b) --> b = true
+    simplified = eqNode(n, trueNode);
+    std::string simplifiedLitName = ProofManager::getLitName(simplified.negate());
+    std::stringstream newLitName;
+    newLitName << "(pred_eq_t _ " << litName << ")";
+    ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str());
+
+  } else if ((n.getKind() == kind::NOT) && (n[0].getKind() == kind::SELECT)) {
+    // not(a[x]) --> a[x] = false
+    simplified = eqNode(n[0], falseNode);
+    std::string simplifiedLitName = ProofManager::getLitName(simplified.negate());
+    std::stringstream newLitName;
+    newLitName << "(pred_eq_f _ " << litName << ")";
+    ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str());
+
+  } else if (n.getKind() == kind::SELECT) {
+    // a[x] --> a[x] = true
+    simplified = eqNode(n, trueNode);
+    std::string simplifiedLitName = ProofManager::getLitName(simplified.negate());
+    std::stringstream newLitName;
+    newLitName << "(pred_eq_t _ " << litName << ")";
+    ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str());
+  }
+
+  if (simplified != n)
+    Debug("pf::simplify") << "simplifyBooleanNode: " << n << " --> " << simplified << std::endl;
+
+  return simplified;
+}
+
+}/* CVC4 namespace */
diff --git a/src/proof/simplify_boolean_node.h b/src/proof/simplify_boolean_node.h
new file mode 100644
index 000000000..dcf7e93db
--- /dev/null
+++ b/src/proof/simplify_boolean_node.h
@@ -0,0 +1,27 @@
+/*********************                                                        */
+/*! \file simplify_boolean_node.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   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
+ **
+ ** \brief Simplifying a boolean node, needed for constructing LFSC proofs.
+ **
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__SIMPLIFY_BOOLEAN_NODE_H
+#define __CVC4__SIMPLIFY_BOOLEAN_NODE_H
+
+namespace CVC4 {
+
+Node simplifyBooleanNode(const Node &n);
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SIMPLIFY_BOOLEAN_NODE_H */
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index e245117fd..c684aa6bc 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -1092,6 +1092,20 @@ void BooleanProof::registerTerm(Expr term) {
   }
 }
 
+void LFSCBooleanProof::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 << "(negsymm _ _ _ t_t_neq_f)";
+}
+
 void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
   Assert (term.getType().isBoolean());
   if (term.isVariable()) {
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index bbdb7d6d7..b9fb33406 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -332,6 +332,7 @@ public:
   virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
 
   bool printsAsBool(const Node &n);
+  void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
 };
 
 } /* CVC4 namespace */
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 */
diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h
index 221a50f43..c4bd28dc5 100644
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -73,6 +73,8 @@ public:
   virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
 
   bool printsAsBool(const Node &n);
+
+  void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
 };