Add support for fewer preprocessing holes

This commit adds support for the --fewer-preprocessing-holes flag. This
flag changes the preprocessing part in proofs in two ways: it (1)
removes assertions that are just restating inputs and uses the inputs
directly instead and it (2) changes the form of the preprocessed
assertions to contain the input that they originate from.

The code in this commit is mostly taken from the proofs branch in Guy's
fork.

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 {