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.

diff --git a/src/options/proof_options b/src/options/proof_options
index 8a496bda6d9a2aa77a50ccd8943d4b01af404c77..322ef5a9ca7be3f920873ed444ee6bd9122d78d5 100644 (file)
--- 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 e987f1c6fba2577b6963ecfde3ad55ff326d2100..1c9bb0ff0558d2fdbad67b20b055da6cb6543f7b 100644 (file)
--- 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 cb5a2bdd17405c61ca98565c65804a66f5d9f67c..fa7224d72c74667282a3a1f8e1115436989a7cc6 100644 (file)
--- 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 d29fc86154551bb5165f6857262f04db303e8c93..1912dbadaa4391c501e69f2041c1825d86c6b33d 100644 (file)
--- 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 b76b90e8401eb91b73cd557a71b869be5351cdfb..d7b7f9c3e8a4ca1306803e42cbafdddf30c207ac 100644 (file)
--- 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());