From 42eed1a8f72d4a5b9ac384100b42f7b0c8b46729 Mon Sep 17 00:00:00 2001
From: Guy <katz911@gmail.com>
Date: Thu, 30 Jun 2016 12:38:56 -0700
Subject: [PATCH] Support for the letification of chained AND and OR operations
 in LFSC proofs

---
 src/proof/proof_manager.cpp | 23 ++++++++++++++++++-----
 src/proof/theory_proof.cpp  | 28 ++++++++++++++++++++++++++++
 2 files changed, 46 insertions(+), 5 deletions(-)

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index d61261b38..d155630e5 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -689,10 +689,24 @@ void bind(Expr term, ProofLetMap& map, Bindings& letOrder) {
   for (unsigned i = 0; i < term.getNumChildren(); ++i)
     bind(term[i], map, letOrder);
 
-  unsigned newId = ProofLetCount::newId();
-  ProofLetCount letCount(newId);
-  map[term] = letCount;
-  letOrder.push_back(LetOrderElement(term, newId));
+  // Special case: chain operators. If we have and(a,b,c), it will be prineted as and(a,and(b,c)).
+  // The subterm and(b,c) may repeat elsewhere, so we need to bind it, too.
+  Kind k = term.getKind();
+  if (((k == kind::OR) || (k == kind::AND)) && term.getNumChildren() > 2) {
+    Node currentExpression = term[term.getNumChildren() - 1];
+    for (int i = term.getNumChildren() - 2; i >= 0; --i) {
+      NodeBuilder<> builder(k);
+      builder << term[i];
+      builder << currentExpression.toExpr();
+      currentExpression = builder;
+      bind(currentExpression.toExpr(), map, letOrder);
+    }
+  } else {
+    unsigned newId = ProofLetCount::newId();
+    ProofLetCount letCount(newId);
+    map[term] = letCount;
+    letOrder.push_back(LetOrderElement(term, newId));
+  }
 }
 
 void ProofManager::printGlobalLetMap(std::set<Node>& atoms,
@@ -708,7 +722,6 @@ void ProofManager::printGlobalLetMap(std::set<Node>& atoms,
   // TODO: give each theory a chance to add atoms. For now, just query BV directly...
   const std::set<Node>* additionalAtoms = ProofManager::getBitVectorProof()->getAtomsInBitblastingProof();
   for (atom = additionalAtoms->begin(); atom != additionalAtoms->end(); ++atom) {
-    Debug("gk::temp") << "Binding additional atom: " << *atom << std::endl;
     bind(atom->toExpr(), letMap, letOrder);
   }
 
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 634b2b738..eff0a8247 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -19,6 +19,7 @@
 #include "base/cvc4_assert.h"
 #include "context/context.h"
 #include "options/bv_options.h"
+#include "options/proof_options.h"
 #include "proof/arith_proof.h"
 #include "proof/array_proof.h"
 #include "proof/bitvector_proof.h"
@@ -801,6 +802,7 @@ void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const Pr
   if (it != map.end()) {
     unsigned id = it->second.id;
     unsigned count = it->second.count;
+
     if (count > LET_COUNT) {
       os << "let" << id;
       return;
@@ -1044,6 +1046,32 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLe
   switch(k) {
   case kind::OR:
   case kind::AND:
+    if (options::lfscLetification() && term.getNumChildren() > 2) {
+      // If letification is on, the entire term is probably a let expression.
+      // However, we need to transform it from (and a b c) into (and a (and b c)) form first.
+      Node currentExpression = term[term.getNumChildren() - 1];
+      for (int i = term.getNumChildren() - 2; i >= 0; --i) {
+        NodeBuilder<> builder(k);
+        builder << term[i];
+        builder << currentExpression.toExpr();
+        currentExpression = builder;
+      }
+
+      // The let map should already have the current expression.
+      ProofLetMap::const_iterator it = map.find(term);
+      if (it != map.end()) {
+        unsigned id = it->second.id;
+        unsigned count = it->second.count;
+
+        if (count > LET_COUNT) {
+          os << "let" << id;
+          break;
+        }
+      }
+    }
+
+    // If letification is off or there were 2 children, same treatment as the other cases.
+    // (No break is intentional).
   case kind::XOR:
   case kind::IFF:
   case kind::IMPLIES:
-- 
2.30.2