1 files changed, 123 insertions, 12 deletions

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index e987f1c6f..1c9bb0ff0 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -211,6 +211,10 @@ std::string ProofManager::getLitName(prop::SatLiteral lit,
 
 std::string ProofManager::getPreprocessedAssertionName(Node node,
                                                        const std::string& prefix) {
+  if (currentPM()->d_assertionFilters.find(node) != currentPM()->d_assertionFilters.end()) {
+    return currentPM()->d_assertionFilters[node];
+  }
+
   node = node.getKind() == kind::BITVECTOR_EAGER_ATOM ? node[0] : node;
   return append(prefix+".PA", node.getId());
 }
@@ -218,6 +222,9 @@ std::string ProofManager::getAssertionName(Node node,
                                            const std::string& prefix) {
   return append(prefix+".A", node.getId());
 }
+std::string ProofManager::getInputFormulaName(const Expr& expr) {
+  return currentPM()->d_inputFormulaToName[expr];
+}
 
 std::string ProofManager::getAtomName(TNode atom,
                                       const std::string& prefix) {
@@ -252,7 +259,7 @@ std::string ProofManager::sanitize(TNode node) {
   return name;
 }
 
-void ProofManager::traceDeps(TNode n) {
+void ProofManager::traceDeps(TNode n, ExprSet* coreAssertions) {
   Debug("cores") << "trace deps " << n << std::endl;
   if ((n.isConst() && n == NodeManager::currentNM()->mkConst<bool>(true)) ||
       (n.getKind() == kind::NOT && n[0] == NodeManager::currentNM()->mkConst<bool>(false))) {
@@ -261,7 +268,7 @@ void ProofManager::traceDeps(TNode n) {
   if(d_inputCoreFormulas.find(n.toExpr()) != d_inputCoreFormulas.end()) {
     // originating formula was in core set
     Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl;
-    d_outputCoreFormulas.insert(n.toExpr());
+    coreAssertions->insert(n.toExpr());
   } else {
     Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl;
     if(d_deps.find(n) == d_deps.end()) {
@@ -272,7 +279,7 @@ void ProofManager::traceDeps(TNode n) {
     for(std::vector<Node>::const_iterator i = deps.begin(); i != deps.end(); ++i) {
       Debug("cores") << " + tracing deps: " << n << " -deps-on- " << *i << std::endl;
       if( !(*i).isNull() ){
-        traceDeps(*i);
+        traceDeps(*i, coreAssertions);
       }
     }
   }
@@ -296,7 +303,7 @@ void ProofManager::traceUnsatCore() {
         rule == RULE_GIVEN) {
       // trace dependences back to actual assertions
       // (this adds them to the unsat core)
-      traceDeps(node);
+      traceDeps(node, &d_outputCoreFormulas);
     }
   }
 }
@@ -444,6 +451,9 @@ Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) {
 void ProofManager::addAssertion(Expr formula) {
   Debug("proof:pm") << "assert: " << formula << std::endl;
   d_inputFormulas.insert(formula);
+  std::ostringstream name;
+  name << "A" << d_inputFormulaToName.size();
+  d_inputFormulaToName[formula] = name.str();
 }
 
 void ProofManager::addCoreAssertion(Expr formula) {
@@ -468,6 +478,10 @@ void ProofManager::addUnsatCore(Expr formula) {
   d_outputCoreFormulas.insert(formula);
 }
 
+void ProofManager::addAssertionFilter(const Node& node, const std::string& rewritten) {
+  d_assertionFilters[node] = rewritten;
+}
+
 void ProofManager::setLogic(const LogicInfo& logic) {
   d_logic = logic;
 }
@@ -682,21 +696,118 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions,
 
   Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions starting" << std::endl;
 
-  for (; it != end; ++it) {
-    os << "(th_let_pf _ ";
+  if (options::fewerPreprocessingHoles()) {
+    // Check for assertions that did not get rewritten, and update the printing filter.
+    checkUnrewrittenAssertion(assertions);
+
+    // For the remaining assertions, bind them to input assertions.
+    for (; it != end; ++it) {
+      // Rewrite preprocessing step if it cannot be eliminated
+      if (!ProofManager::currentPM()->have_input_assertion((*it).toExpr())) {
+        os << "(th_let_pf _ (trust_f (iff ";
+
+        Expr inputAssertion;
+
+        if (((*it).isConst() && *it == NodeManager::currentNM()->mkConst<bool>(true)) ||
+            ((*it).getKind() == kind::NOT && (*it)[0] == NodeManager::currentNM()->mkConst<bool>(false))) {
+          inputAssertion = NodeManager::currentNM()->mkConst<bool>(true).toExpr();
+        } else {
+          // Figure out which input assertion led to this assertion
+          ExprSet inputAssertions;
+          ProofManager::currentPM()->traceDeps(*it, &inputAssertions);
+
+          Debug("pf::pm") << "Original assertions for " << *it << " are: " << std::endl;
+
+          ProofManager::assertions_iterator assertionIt;
+          for (assertionIt = inputAssertions.begin(); assertionIt != inputAssertions.end(); ++assertionIt) {
+            Debug("pf::pm") << "\t" << *assertionIt << std::endl;
+          }
+
+          if (inputAssertions.size() == 0) {
+            Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Count NOT find the assertion that caused this PA. Picking an arbitrary one..." << std::endl;
+            // For now just use the first assertion...
+            inputAssertion = *(ProofManager::currentPM()->begin_assertions());
+          } else {
+            if (inputAssertions.size() != 1) {
+              Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Attention: more than one original assertion was found. Picking just one." << std::endl;
+            }
+            inputAssertion = *inputAssertions.begin();
+          }
+        }
+
+        if (!ProofManager::currentPM()->have_input_assertion(inputAssertion)) {
+          // The thing returned by traceDeps does not appear in the input assertions...
+          Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Count NOT find the assertion that caused this PA. Picking an arbitrary one..." << std::endl;
+          // For now just use the first assertion...
+          inputAssertion = *(ProofManager::currentPM()->begin_assertions());
+        }
+
+        Debug("pf::pm") << "Original assertion for " << *it
+                        << " is: "
+                        << inputAssertion
+                        << ", AKA "
+                        << ProofManager::currentPM()->getInputFormulaName(inputAssertion)
+                        << std::endl;
+
+        ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm(inputAssertion, os, globalLetMap);
+        os << " ";
+        ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap);
+
+        os << "))";
+        os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n";
+        paren << "))";
 
-    //TODO
-    os << "(trust_f ";
-    ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap);
-    os << ") ";
+        std::ostringstream rewritten;
 
-    os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n";
-    paren << "))";
+        rewritten << "(or_elim_1 _ _ ";
+        rewritten << "(not_not_intro _ ";
+        rewritten << ProofManager::currentPM()->getInputFormulaName(inputAssertion);
+        rewritten << ") (iff_elim_1 _ _ ";
+        rewritten << ProofManager::getPreprocessedAssertionName(*it, "");
+        rewritten << "))";
+
+        ProofManager::currentPM()->addAssertionFilter(*it, rewritten.str());
+      }
+    }
+  } else {
+    for (; it != end; ++it) {
+      os << "(th_let_pf _ ";
+
+      //TODO
+      os << "(trust_f ";
+      ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap);
+      os << ") ";
+
+      os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n";
+      paren << "))";
+    }
   }
 
   os << "\n";
 }
 
+void LFSCProof::checkUnrewrittenAssertion(const NodeSet& rewrites) {
+  Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion starting" << std::endl;
+
+  NodeSet::const_iterator rewrite;
+  for (rewrite = rewrites.begin(); rewrite != rewrites.end(); ++rewrite) {
+    Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: handling " << *rewrite << std::endl;
+    if (ProofManager::currentPM()->have_input_assertion((*rewrite).toExpr())) {
+      Assert(ProofManager::currentPM()->have_input_assertion((*rewrite).toExpr()));
+      Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: this assertion was NOT rewritten!" << std::endl
+                      << "\tAdding filter: "
+                      << ProofManager::getPreprocessedAssertionName(*rewrite, "")
+                      << " --> "
+                      << ProofManager::currentPM()->getInputFormulaName((*rewrite).toExpr())
+                      << std::endl;
+      ProofManager::currentPM()->addAssertionFilter(*rewrite,
+        ProofManager::currentPM()->getInputFormulaName((*rewrite).toExpr()));
+    } else {
+      Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: this assertion WAS rewritten! " << *rewrite << std::endl;
+    }
+  }
+}
+
 //---from Morgan---
 
 bool ProofManager::hasOp(TNode n) const {