Revert "Merging proof branch"

This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.

1 files changed, 29 insertions, 62 deletions

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 5ce8b523f..a3689d746 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -200,6 +200,7 @@ std::string ProofManager::getLitName(prop::SatLiteral lit,
   return append(prefix+".l", lit.toInt());
 }
 
+
 std::string ProofManager::getPreprocessedAssertionName(Node node,
                                                        const std::string& prefix) {
   node = node.getKind() == kind::BITVECTOR_EAGER_ATOM ? node[0] : node;
@@ -216,15 +217,9 @@ std::string ProofManager::getAtomName(TNode atom,
   Assert(!lit.isNegated());
   return getAtomName(lit.getSatVariable(), prefix);
 }
-
 std::string ProofManager::getLitName(TNode lit,
                                      const std::string& prefix) {
-  std::string litName = getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix);
-  if (currentPM()->d_rewriteFilters.find(litName) != currentPM()->d_rewriteFilters.end()) {
-    return currentPM()->d_rewriteFilters[litName];
-  }
-
-  return litName;
+  return getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix);
 }
 
 std::string ProofManager::sanitize(TNode node) {
@@ -336,9 +331,6 @@ LFSCProof::LFSCProof(SmtEngine* smtEngine,
 {}
 
 void LFSCProof::toStream(std::ostream& out) {
-
-  Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER);
-
   d_satProof->constructProof();
 
   // collecting leaf clauses in resolution proof
@@ -392,37 +384,8 @@ void LFSCProof::toStream(std::ostream& out) {
   for (it3 = used_assertions.begin(); it3 != used_assertions.end(); ++it3)
     Debug("pf::pm") << "\t assertion = " << *it3 << std::endl;
 
-  std::set<Node> atoms;
-  NodePairSet rewrites;
+  NodeSet atoms;
   // collects the atoms in the clauses
-  d_cnfProof->collectAtomsAndRewritesForLemmas(used_lemmas, atoms, rewrites);
-
-  if (!rewrites.empty()) {
-    Debug("pf::pm") << std::endl << "Rewrites used in lemmas: " << std::endl;
-    NodePairSet::const_iterator rewriteIt;
-    for (rewriteIt = rewrites.begin(); rewriteIt != rewrites.end(); ++rewriteIt) {
-      Debug("pf::pm") << "\t" << rewriteIt->first << " --> " << rewriteIt->second << std::endl;
-    }
-    Debug("pf::pm") << std::endl << "Rewrite printing done" << std::endl;
-  } else {
-    Debug("pf::pm") << "No rewrites in lemmas found" << std::endl;
-  }
-
-  // The derived/unrewritten atoms may not have CNF literals required later on.
-  // If they don't, add them.
-  std::set<Node>::const_iterator it;
-  for (it = atoms.begin(); it != atoms.end(); ++it) {
-    Debug("pf::pm") << "Ensure literal for atom: " << *it << std::endl;
-    if (!d_cnfProof->hasLiteral(*it)) {
-      // For arithmetic: these literals are not normalized, causing an error in Arith.
-      if (theory::Theory::theoryOf(*it) == theory::THEORY_ARITH) {
-        d_cnfProof->ensureLiteral(*it, true); // This disables preregistration with the theory solver.
-      } else {
-        d_cnfProof->ensureLiteral(*it); // Normal method, with theory solver preregisteration.
-      }
-    }
-  }
-
   d_cnfProof->collectAtomsForClauses(used_inputs, atoms);
   d_cnfProof->collectAtomsForClauses(used_lemmas, atoms);
 
@@ -430,23 +393,38 @@ void LFSCProof::toStream(std::ostream& out) {
   for (NodeSet::const_iterator it = used_assertions.begin();
        it != used_assertions.end(); ++it) {
     utils::collectAtoms(*it, atoms);
-    // utils::collectAtoms(*it, newAtoms);
   }
 
-  std::set<Node>::iterator atomIt;
-  Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: "
-                  << std::endl << std::endl;
+  NodeSet::iterator atomIt;
+  Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: " << std::endl << std::endl;
   for (atomIt = atoms.begin(); atomIt != atoms.end(); ++atomIt) {
     Debug("pf::pm") << "\tAtom: " << *atomIt << std::endl;
+
+    if (Debug.isOn("proof:pm")) {
+      // std::cout << NodeManager::currentNM();
+      Debug("proof:pm") << "LFSCProof::Used assertions: "<< std::endl;
+      for(NodeSet::const_iterator it = used_assertions.begin(); it != used_assertions.end(); ++it) {
+        Debug("proof:pm") << "   " << *it << std::endl;
+      }
+
+      Debug("proof:pm") << "LFSCProof::Used atoms: "<< std::endl;
+      for(NodeSet::const_iterator it = atoms.begin(); it != atoms.end(); ++it) {
+        Debug("proof:pm") << "   " << *it << std::endl;
+      }
+    }
   }
+
   smt::SmtScope scope(d_smtEngine);
   std::ostringstream paren;
   out << "(check\n";
   out << " ;; Declarations\n";
 
   // declare the theory atoms
+  NodeSet::const_iterator it = atoms.begin();
+  NodeSet::const_iterator end = atoms.end();
+
   Debug("pf::pm") << "LFSCProof::toStream: registering terms:" << std::endl;
-  for(it = atoms.begin(); it != atoms.end(); ++it) {
+  for(; it != end; ++it) {
     Debug("pf::pm") << "\tTerm: " << (*it).toExpr() << std::endl;
     d_theoryProof->registerTerm((*it).toExpr());
   }
@@ -466,15 +444,9 @@ void LFSCProof::toStream(std::ostream& out) {
   out << "(: (holds cln)\n\n";
 
   // Have the theory proofs print deferred declarations, e.g. for skolem variables.
-  out << " ;; Printing deferred declarations \n\n";
+  out << " ;; Printing deferred declarations \n";
   d_theoryProof->printDeferredDeclarations(out, paren);
 
-  out << " ;; Printing aliasing declarations \n\n";
-  d_theoryProof->printAliasingDeclarations(out, paren);
-
-  out << " ;; Rewrites for Lemmas \n";
-  d_theoryProof->printLemmaRewrites(rewrites, out, paren);
-
   // print trust that input assertions are their preprocessed form
   printPreprocessedAssertions(used_assertions, out, paren);
 
@@ -492,6 +464,10 @@ void LFSCProof::toStream(std::ostream& out) {
 
   Debug("pf::pm") << std::endl << "Printing cnf proof for clauses DONE" << std::endl;
 
+  // FIXME: for now assume all theory lemmas are in CNF form so
+  // distinguish between them and inputs
+  // print theory lemmas for resolution proof
+
   Debug("pf::pm") << "Proof manager: printing theory lemmas" << std::endl;
   d_theoryProof->printTheoryLemmas(used_lemmas, out, paren);
   Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl;
@@ -520,8 +496,6 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions,
   NodeSet::const_iterator it = assertions.begin();
   NodeSet::const_iterator end = assertions.end();
 
-  Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions starting" << std::endl;
-
   for (; it != end; ++it) {
     os << "(th_let_pf _ ";
 
@@ -532,6 +506,7 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions,
 
     os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n";
     paren << "))";
+
   }
 
   os << "\n";
@@ -593,14 +568,6 @@ void ProofManager::markPrinted(const Type& type) {
   d_printedTypes.insert(type);
 }
 
-void ProofManager::addRewriteFilter(const std::string &original, const std::string &substitute) {
-  d_rewriteFilters[original] = substitute;
-}
-
-void ProofManager::clearRewriteFilters() {
-  d_rewriteFilters.clear();
-}
-
 std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k) {
   switch(k) {
   case RULE_GIVEN: