1 files changed, 371 insertions, 2 deletions

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 0dd573dc6..34f3a92ec 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -29,6 +29,7 @@
 #include "proof/proof_output_channel.h"
 #include "proof/proof_utils.h"
 #include "proof/sat_proof.h"
+#include "proof/simplify_boolean_node.h"
 #include "proof/uf_proof.h"
 #include "prop/sat_solver_types.h"
 #include "smt/smt_engine.h"
@@ -38,13 +39,11 @@
 #include "theory/bv/theory_bv.h"
 #include "theory/output_channel.h"
 #include "theory/term_registration_visitor.h"
-#include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/valuation.h"
 #include "util/hash.h"
 #include "util/proof.h"
 
-
 namespace CVC4 {
 
 unsigned CVC4::ProofLetCount::counter = 0;
@@ -1099,6 +1098,7 @@ void BooleanProof::registerTerm(Expr term) {
   }
 }
 
+theory::TheoryId BooleanProof::getTheoryId() { return theory::THEORY_BOOL; }
 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);
@@ -1264,4 +1264,373 @@ void TheoryProof::printRewriteProof(std::ostream& os, const Node &n1, const Node
   os << "))";
 }
 
+inline bool TheoryProof::match(TNode n1, TNode n2)
+{
+  theory::TheoryId theoryId = this->getTheoryId();
+  ProofManager* pm = ProofManager::currentPM();
+  bool ufProof = (theoryId == theory::THEORY_UF);
+  Debug(ufProof ? "pf::uf" : "mgd") << "match " << n1 << " " << n2 << std::endl;
+  if (pm->hasOp(n1))
+  {
+    n1 = pm->lookupOp(n1);
+  }
+  if (pm->hasOp(n2))
+  {
+    n2 = pm->lookupOp(n2);
+  }
+  Debug(ufProof ? "pf::uf" : "mgd") << "+ match " << n1 << " " << n2
+                                    << std::endl;
+  if (!ufProof)
+  {
+    Debug("pf::array") << "+ match: step 1" << std::endl;
+  }
+  if (n1 == n2)
+  {
+    return true;
+  }
+
+  if (n1.getType().isFunction() && n2.hasOperator())
+  {
+    if (pm->hasOp(n2.getOperator()))
+    {
+      return n1 == pm->lookupOp(n2.getOperator());
+    }
+    else
+    {
+      return n1 == n2.getOperator();
+    }
+  }
+
+  if (n2.getType().isFunction() && n1.hasOperator())
+  {
+    if (pm->hasOp(n1.getOperator()))
+    {
+      return n2 == pm->lookupOp(n1.getOperator());
+    }
+    else
+    {
+      return n2 == n1.getOperator();
+    }
+  }
+
+  if (n1.hasOperator() && n2.hasOperator()
+      && n1.getOperator() != n2.getOperator())
+  {
+    if (ufProof
+        || !((n1.getKind() == kind::SELECT
+              && n2.getKind() == kind::PARTIAL_SELECT_0)
+             || (n1.getKind() == kind::SELECT
+                 && n2.getKind() == kind::PARTIAL_SELECT_1)
+             || (n1.getKind() == kind::PARTIAL_SELECT_1
+                 && n2.getKind() == kind::SELECT)
+             || (n1.getKind() == kind::PARTIAL_SELECT_1
+                 && n2.getKind() == kind::PARTIAL_SELECT_0)
+             || (n1.getKind() == kind::PARTIAL_SELECT_0
+                 && n2.getKind() == kind::SELECT)
+             || (n1.getKind() == kind::PARTIAL_SELECT_0
+                 && n2.getKind() == kind::PARTIAL_SELECT_1)))
+    {
+      return false;
+    }
+  }
+
+  for (size_t i = 0; i < n1.getNumChildren() && i < n2.getNumChildren(); ++i)
+  {
+    if (n1[i] != n2[i])
+    {
+      return false;
+    }
+  }
+
+  return true;
+}
+
+int TheoryProof::assertAndPrint(
+    const theory::eq::EqProof& pf,
+    const ProofLetMap& map,
+    std::shared_ptr<theory::eq::EqProof> subTrans,
+    theory::eq::EqProof::PrettyPrinter* pPrettyPrinter)
+{
+  theory::TheoryId theoryId = getTheoryId();
+  int neg = -1;
+  Assert(theoryId == theory::THEORY_UF || theoryId == theory::THEORY_ARRAYS);
+  bool ufProof = (theoryId == theory::THEORY_UF);
+  std::string theoryName = theory::getStatsPrefix(theoryId);
+  pf.debug_print(("pf::" + theoryName).c_str(), 0, pPrettyPrinter);
+  Debug("pf::" + theoryName) << std::endl;
+
+  Assert(pf.d_id == theory::eq::MERGED_THROUGH_TRANS);
+  Assert(!pf.d_node.isNull());
+  Assert(pf.d_children.size() >= 2);
+
+  subTrans->d_id = theory::eq::MERGED_THROUGH_TRANS;
+  subTrans->d_node = pf.d_node;
+
+  size_t i = 0;
+  while (i < pf.d_children.size())
+  {
+    // special treatment for uf and not for array
+    if (ufProof
+        || 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);
+      (neg) = i;
+      ++i;
+    }
+
+    // Handle congruence closures over equalities.
+    else if (pf.d_children[i]->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE
+             && pf.d_children[i]->d_node.isNull())
+    {
+      Debug("pf::" + theoryName) << "Handling congruence over equalities"
+                                 << std::endl;
+
+      // Gather the sequence of consecutive congruence closures.
+      std::vector<std::shared_ptr<const theory::eq::EqProof>>
+          congruenceClosures;
+      unsigned count;
+      Debug("pf::" + theoryName) << "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();
+           ++count)
+      {
+        Debug("pf::" + theoryName) << "Found a congruence: " << std::endl;
+        pf.d_children[i + count]->debug_print(
+            ("pf::" + theoryName).c_str(), 0, pPrettyPrinter);
+        congruenceClosures.push_back(pf.d_children[i + count]);
+      }
+
+      Debug("pf::" + theoryName)
+          << "Total number of congruences found: " << congruenceClosures.size()
+          << std::endl;
+
+      // Determine if the "target" of the congruence sequence appears right
+      // before or right after the sequence.
+      bool targetAppearsBefore = true;
+      bool targetAppearsAfter = true;
+
+      if ((i == 0) || (i == 1 && neg == 0))
+      {
+        Debug("pf::" + theoryName) << "Target does not appear before"
+                                   << std::endl;
+        targetAppearsBefore = false;
+      }
+
+      if ((i + count >= pf.d_children.size())
+          || (!pf.d_children[i + count]->d_node.isNull()
+              && pf.d_children[i + count]->d_node.getKind() == kind::NOT))
+      {
+        Debug("pf::" + theoryName) << "Target does not appear after"
+                                   << std::endl;
+        targetAppearsAfter = false;
+      }
+
+      // Flow changes between uf and array
+      if (ufProof)
+      {
+        // 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;
+        }
+      }
+      else
+      {  // not a uf proof
+        // Assert that we have precisely one target clause.
+        Assert(targetAppearsBefore != targetAppearsAfter);
+      }
+
+      // Begin breaking up the congruences and ordering the equalities
+      // correctly.
+      std::vector<std::shared_ptr<theory::eq::EqProof>> orderedEqualities;
+
+      // Insert target clause first.
+      if (targetAppearsBefore)
+      {
+        orderedEqualities.push_back(pf.d_children[i - 1]);
+        // The target has already been added to subTrans; remove it.
+        subTrans->d_children.pop_back();
+      }
+      else
+      {
+        orderedEqualities.push_back(pf.d_children[i + count]);
+      }
+
+      // Start with the congruence closure closest to the target clause, and
+      // work our way back/forward.
+      if (targetAppearsBefore)
+      {
+        for (unsigned j = 0; j < count; ++j)
+        {
+          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]);
+        }
+      }
+      else
+      {
+        for (unsigned j = 0; j < count; ++j)
+        {
+          if (pf.d_children[i + count - 1 - j]->d_children[0]->d_id
+              != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+            orderedEqualities.insert(
+                orderedEqualities.begin(),
+                pf.d_children[i + count - 1 - j]->d_children[0]);
+          if (pf.d_children[i + count - 1 - j]->d_children[1]->d_id
+              != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+            orderedEqualities.insert(
+                orderedEqualities.end(),
+                pf.d_children[i + count - 1 - j]->d_children[1]);
+        }
+      }
+
+      // Copy the result into the main transitivity proof.
+      subTrans->d_children.insert(subTrans->d_children.end(),
+                                  orderedEqualities.begin(),
+                                  orderedEqualities.end());
+
+      // Increase i to skip over the children that have been processed.
+      i += count;
+      if (targetAppearsAfter)
+      {
+        ++i;
+      }
+    }
+
+    // Else, just copy the child proof as is
+    else
+    {
+      subTrans->d_children.push_back(pf.d_children[i]);
+      ++i;
+    }
+  }
+
+  bool disequalityFound = (neg >= 0);
+  if (!disequalityFound)
+  {
+    Debug("pf::" + theoryName)
+        << "A disequality was NOT found. UNSAT due to merged constants"
+        << std::endl;
+    Debug("pf::" + theoryName) << "Proof for: " << pf.d_node << std::endl;
+    Assert(pf.d_node.getKind() == kind::EQUAL);
+    Assert(pf.d_node.getNumChildren() == 2);
+    Assert(pf.d_node[0].isConst() && pf.d_node[1].isConst());
+  }
+  return neg;
+}
+
+std::pair<Node, Node> TheoryProof::identicalEqualitiesPrinterHelper(
+    bool evenLengthSequence,
+    bool sequenceOver,
+    const theory::eq::EqProof& pf,
+    const ProofLetMap& map,
+    const std::string subproofStr,
+    std::stringstream* outStream,
+    Node n,
+    Node nodeAfterEqualitySequence)
+{
+  theory::TheoryId theoryId = getTheoryId();
+  Assert(theoryId == theory::THEORY_UF || theoryId == theory::THEORY_ARRAYS);
+  bool ufProof = (theoryId == theory::THEORY_UF);
+  std::string theoryName = theory::getStatsPrefix(theoryId);
+  if (evenLengthSequence)
+  {
+    // If the length is even, we need to apply transitivity for the "correct"
+    // hand of the equality.
+
+    Debug("pf::" + theoryName) << "Equality sequence of even length"
+                               << std::endl;
+    Debug("pf::" + theoryName) << "n1 is: " << n << std::endl;
+    Debug("pf::" + theoryName) << "pf-d_node is: " << pf.d_node << std::endl;
+    Debug("pf::" + theoryName) << "Next node is: " << nodeAfterEqualitySequence
+                               << std::endl;
+
+    (*outStream) << "(trans _ _ _ _ ";
+
+    // If the sequence is at the very end of the transitivity proof, use
+    // pf.d_node to guide us.
+    if (!sequenceOver)
+    {
+      if (match(n[0], pf.d_node[0]))
+      {
+        n = n[0].eqNode(n[0]);
+        (*outStream) << subproofStr << " (symm _ _ _ " << subproofStr << ")";
+      }
+      else if (match(n[1], pf.d_node[1]))
+      {
+        n = n[1].eqNode(n[1]);
+        (*outStream) << " (symm _ _ _ " << subproofStr << ")" << subproofStr;
+      }
+      else
+      {
+        Debug("pf::" + theoryName) << "Error: identical equalities over, but "
+                                      "hands don't match what we're proving."
+                                   << std::endl;
+        Assert(false);
+      }
+    }
+    else
+    {
+      // We have a "next node". Use it to guide us.
+      if (!ufProof && nodeAfterEqualitySequence.getKind() == kind::NOT)
+      {
+        nodeAfterEqualitySequence = nodeAfterEqualitySequence[0];
+      }
+
+      Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL);
+
+      if ((n[0] == nodeAfterEqualitySequence[0])
+          || (n[0] == nodeAfterEqualitySequence[1]))
+      {
+        // Eliminate n[1]
+        (*outStream) << subproofStr << " (symm _ _ _ " << subproofStr << ")";
+        n = n[0].eqNode(n[0]);
+      }
+      else if ((n[1] == nodeAfterEqualitySequence[0])
+               || (n[1] == nodeAfterEqualitySequence[1]))
+      {
+        // Eliminate n[0]
+        (*outStream) << " (symm _ _ _ " << subproofStr << ")" << subproofStr;
+        n = n[1].eqNode(n[1]);
+      }
+      else
+      {
+        Debug("pf::" + theoryName) << "Error: even length sequence, but I "
+                                      "don't know which hand to keep!"
+                                   << std::endl;
+        Assert(false);
+      }
+    }
+
+    (*outStream) << ")";
+  }
+  else
+  {
+    Debug("pf::" + theoryName) << "Equality sequence length is odd!"
+                               << std::endl;
+    (*outStream).str(subproofStr);
+  }
+
+  Debug("pf::" + theoryName) << "Have proven: " << n << std::endl;
+  return std::make_pair<Node&, Node&>(n, nodeAfterEqualitySequence);
+}
+
 } /* namespace CVC4 */