Remove input assertionsremove_in_assertions

4 files changed, 32 insertions, 45 deletions

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 5ce615366..879635d7b 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -60,7 +60,6 @@ ProofManager::ProofManager(ProofFormat format):
   d_satProof(NULL),
   d_cnfProof(NULL),
   d_theoryProof(NULL),
-  d_inputFormulas(),
   d_inputCoreFormulas(),
   d_outputCoreFormulas(),
   d_nextId(0),
@@ -223,7 +222,7 @@ std::string ProofManager::getAssertionName(Node node,
   return append(prefix+".A", node.getId());
 }
 std::string ProofManager::getInputFormulaName(const Expr& expr) {
-  return currentPM()->d_inputFormulaToName[expr];
+  return currentPM()->d_inputCoreFormulaToName[expr];
 }
 
 std::string ProofManager::getAtomName(TNode atom,
@@ -452,18 +451,13 @@ Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) {
   return builder;
 }
 
-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) {
   Debug("cores") << "assert: " << formula << std::endl;
   d_deps[Node::fromExpr(formula)]; // empty vector of deps
   d_inputCoreFormulas.insert(formula);
+  std::ostringstream name;
+  name << "A" << d_inputCoreFormulaToName.size();
+  d_inputCoreFormulaToName[formula] = name.str();
 }
 
 void ProofManager::addDependence(TNode n, TNode dep) {
@@ -707,7 +701,8 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& 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())) {
+      if (!ProofManager::currentPM()->have_input_core_assertion(
+              (*it).toExpr())) {
         os << "(th_let_pf _ (trust_f (iff ";
 
         Expr inputAssertion;
@@ -730,7 +725,8 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions,
           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());
+            inputAssertion =
+                *(ProofManager::currentPM()->begin_input_core_assertions());
           } else {
             if (inputAssertions.size() != 1) {
               Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Attention: more than one original assertion was found. Picking just one." << std::endl;
@@ -739,13 +735,6 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions,
           }
         }
 
-        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
@@ -796,8 +785,10 @@ void LFSCProof::checkUnrewrittenAssertion(const NodeSet& rewrites) {
   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()));
+    if (ProofManager::currentPM()->have_input_core_assertion(
+            (*rewrite).toExpr())) {
+      Assert(ProofManager::currentPM()->have_input_core_assertion(
+          (*rewrite).toExpr()));
       Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: this assertion was NOT rewritten!" << std::endl
                       << "\tAdding filter: "
                       << ProofManager::getPreprocessedAssertionName(*rewrite, "")
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index fa7224d72..13edab601 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -144,8 +144,7 @@ class ProofManager {
   TheoryProofEngine* d_theoryProof;
 
   // information that will need to be shared across proofs
-  ExprSet    d_inputFormulas;
-  std::map<Expr, std::string> d_inputFormulaToName;
+  std::map<Expr, std::string> d_inputCoreFormulaToName;
   ExprSet    d_inputCoreFormulas;
   ExprSet    d_outputCoreFormulas;
 
@@ -197,13 +196,14 @@ public:
   typedef ExprSet::const_iterator assertions_iterator;
 
   // iterate over the assertions (these are arbitrary boolean formulas)
-  assertions_iterator begin_assertions() const {
-    return d_inputFormulas.begin();
+  assertions_iterator begin_input_core_assertions() const {
+    return d_inputCoreFormulas.begin();
   }
-  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();
+  assertions_iterator end_input_core_assertions() const {
+    return d_inputCoreFormulas.end();
+  }
+  bool have_input_core_assertion(const Expr& assertion) const {
+    return d_inputCoreFormulas.find(assertion) != d_inputCoreFormulas.end();
   }
 
 //---from Morgan---
@@ -234,9 +234,6 @@ public:
   // for SMT variable names that have spaces and other things
   static std::string sanitize(TNode var);
 
-  /** Add proof assertion - unlike addCoreAssertion this is post definition expansion **/
-  void addAssertion(Expr formula);
-
   /** Public unsat core methods **/
   void addCoreAssertion(Expr formula);
 
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 1912dbada..2d89bfe24 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -308,8 +308,10 @@ void LFSCTheoryProofEngine::treatBoolsAsFormulas(bool value) {
 }
 
 void LFSCTheoryProofEngine::registerTermsFromAssertions() {
-  ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions();
-  ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions();
+  ProofManager::assertions_iterator it =
+      ProofManager::currentPM()->begin_input_core_assertions();
+  ProofManager::assertions_iterator end =
+      ProofManager::currentPM()->end_input_core_assertions();
 
   for(; it != end; ++it) {
     registerTerm(*it);
@@ -321,14 +323,17 @@ void LFSCTheoryProofEngine::registerTermsFromAssertions() {
 void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& paren) {
   Debug("pf::tp") << "LFSCTheoryProofEngine::printAssertions called" << std::endl << std::endl;
 
-  ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions();
-  ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions();
+  ProofManager::assertions_iterator it =
+      ProofManager::currentPM()->begin_input_core_assertions();
+  ProofManager::assertions_iterator end =
+      ProofManager::currentPM()->end_input_core_assertions();
 
   for (; it != end; ++it) {
     Debug("pf::tp") << "printAssertions: assertion is: " << *it << std::endl;
     os << "(% " << ProofManager::currentPM()->getInputFormulaName(*it) << " (th_holds ";
 
-    // Assertions appear before the global let map, so we use a dummpMap to avoid letification here.
+    // Assertions appear before the global let map, so we use a dummyMap to
+    // avoid letification here.
     ProofLetMap dummyMap;
     printBoundTerm(*it, os, dummyMap);
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a79416b76..a0066f9ff 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3835,6 +3835,8 @@ void SmtEnginePrivate::processAssertions() {
 
   // Add dummy assertion in last position - to be used as a
   // placeholder for any new assertions to get added
+  PROOF(ProofManager::currentPM()->addCoreAssertion(
+      NodeManager::currentNM()->mkConst<bool>(true).toExpr()));
   d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(true));
   // any assertions added beyond realAssertionsEnd must NOT affect the
   // equisatisfiability
@@ -3856,14 +3858,6 @@ void SmtEnginePrivate::processAssertions() {
   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-definition-expansion" << endl;
   dumpAssertions("post-definition-expansion", d_assertions);
 
-  // save the assertions now
-  THEORY_PROOF
-    (
-     for (unsigned i = 0; i < d_assertions.size(); ++i) {
-       ProofManager::currentPM()->addAssertion(d_assertions[i].toExpr());
-     }
-     );
-
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
   if( options::ceGuidedInst() ){