Merge pull request #90 from 4tXJ7f/fewer_preproc_holes

Add support for fewer preprocessing holes

5 files changed, 145 insertions, 20 deletions

diff --git a/src/options/proof_options b/src/options/proof_options
index 8a496bda6..322ef5a9c 100644
--- a/src/options/proof_options
+++ b/src/options/proof_options
@@ -11,4 +11,7 @@ option lfscLetification --lfsc-letification bool :default true
 option aggressiveCoreMin --aggressive-core-min bool :default false
  turns on aggressive unsat core minimization (experimental)
 
+option fewerPreprocessingHoles --fewer-preprocessing-holes bool :default false :read-write
+  try to eliminate preprocessing holes in proofs
+
 endmodule
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 {
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index cb5a2bdd1..fa7224d72 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -145,6 +145,7 @@ class ProofManager {
 
   // information that will need to be shared across proofs
   ExprSet    d_inputFormulas;
+  std::map<Expr, std::string> d_inputFormulaToName;
   ExprSet    d_inputCoreFormulas;
   ExprSet    d_outputCoreFormulas;
 
@@ -156,12 +157,11 @@ class ProofManager {
   ProofFormat d_format; // used for now only in debug builds
 
   NodeToNodes d_deps;
-  // trace dependences back to unsat core
-  void traceDeps(TNode n);
 
   std::set<Type> d_printedTypes;
 
   std::map<std::string, std::string> d_rewriteFilters;
+  std::map<Node, std::string> d_assertionFilters;
 
   std::vector<RewriteLogEntry> d_rewriteLog;
 
@@ -202,6 +202,9 @@ public:
   }
   assertions_iterator end_assertions() const { return d_inputFormulas.end(); }
   size_t num_assertions() const { return d_inputFormulas.size(); }
+  bool have_input_assertion(const Expr& assertion) {
+    return d_inputFormulas.find(assertion) != d_inputFormulas.end();
+  }
 
 //---from Morgan---
   Node mkOp(TNode n);
@@ -220,6 +223,7 @@ public:
   static std::string getLearntClauseName(ClauseId id, const std::string& prefix = "");
   static std::string getPreprocessedAssertionName(Node node, const std::string& prefix = "");
   static std::string getAssertionName(Node node, const std::string& prefix = "");
+  static std::string getInputFormulaName(const Expr& expr);
 
   static std::string getVarName(prop::SatVariable var, const std::string& prefix = "");
   static std::string getAtomName(prop::SatVariable var, const std::string& prefix = "");
@@ -239,6 +243,8 @@ public:
   void addDependence(TNode n, TNode dep);
   void addUnsatCore(Expr formula);
 
+  // trace dependences back to unsat core
+  void traceDeps(TNode n, ExprSet* coreAssertions);
   void traceUnsatCore();
   assertions_iterator begin_unsat_core() const { return d_outputCoreFormulas.begin(); }
   assertions_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); }
@@ -260,6 +266,8 @@ public:
   void addRewriteFilter(const std::string &original, const std::string &substitute);
   void clearRewriteFilters();
 
+  void addAssertionFilter(const Node& node, const std::string& rewritten);
+
   static void registerRewrite(unsigned ruleId, Node original, Node result);
   static void clearRewriteLog();
 
@@ -287,6 +295,9 @@ class LFSCProof : public Proof {
                                    std::ostream& os,
                                    std::ostream& paren,
                                    ProofLetMap& globalLetMap);
+
+  void checkUnrewrittenAssertion(const NodeSet& assertions);
+
 public:
   LFSCProof(SmtEngine* smtEngine,
             LFSCCoreSatProof* sat,
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index d29fc8615..1912dbada 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -321,15 +321,12 @@ void LFSCTheoryProofEngine::registerTermsFromAssertions() {
 void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& paren) {
   Debug("pf::tp") << "LFSCTheoryProofEngine::printAssertions called" << std::endl << std::endl;
 
-  unsigned counter = 0;
   ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions();
   ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions();
 
   for (; it != end; ++it) {
     Debug("pf::tp") << "printAssertions: assertion is: " << *it << std::endl;
-    std::ostringstream name;
-    name << "A" << counter++;
-    os << "(% " << name.str() << " (th_holds ";
+    os << "(% " << ProofManager::currentPM()->getInputFormulaName(*it) << " (th_holds ";
 
     // Assertions appear before the global let map, so we use a dummpMap to avoid letification here.
     ProofLetMap dummyMap;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b76b90e84..d7b7f9c3e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -57,6 +57,7 @@
 #include "options/open_ostream.h"
 #include "options/option_exception.h"
 #include "options/printer_options.h"
+#include "options/proof_options.h"
 #include "options/prop_options.h"
 #include "options/quantifiers_options.h"
 #include "options/set_language.h"
@@ -92,9 +93,9 @@
 #include "theory/quantifiers/fun_def_process.h"
 #include "theory/quantifiers/macros.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/sep/theory_sep.h"
 #include "theory/sort_inference.h"
 #include "theory/strings/theory_strings.h"
-#include "theory/sep/theory_sep.h"
 #include "theory/substitutions.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_model.h"
@@ -4283,8 +4284,10 @@ void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput)
   PROOF(
     if( inInput ){
       // n is an input assertion
-      if (inUnsatCore || options::dumpUnsatCores() || options::checkUnsatCores())
+      if (inUnsatCore || options::dumpUnsatCores() || options::checkUnsatCores() || options::fewerPreprocessingHoles()) {
+
         ProofManager::currentPM()->addCoreAssertion(n.toExpr());
+      }
     }else{
       // n is the result of an unknown preprocessing step, add it to dependency map to null
       ProofManager::currentPM()->addDependence(n, Node::null());