Merge from proof branch

1 files changed, 62 insertions, 29 deletions

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index a3689d746..5ce8b523f 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -200,7 +200,6 @@ 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;
@@ -217,9 +216,15 @@ std::string ProofManager::getAtomName(TNode atom,
   Assert(!lit.isNegated());
   return getAtomName(lit.getSatVariable(), prefix);
 }
+
 std::string ProofManager::getLitName(TNode lit,
                                      const std::string& prefix) {
-  return getLitName(currentPM()->d_cnfProof->getLiteral(lit), 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;
 }
 
 std::string ProofManager::sanitize(TNode node) {
@@ -331,6 +336,9 @@ 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
@@ -384,8 +392,37 @@ void LFSCProof::toStream(std::ostream& out) {
   for (it3 = used_assertions.begin(); it3 != used_assertions.end(); ++it3)
     Debug("pf::pm") << "\t assertion = " << *it3 << std::endl;
 
-  NodeSet atoms;
+  std::set<Node> atoms;
+  NodePairSet rewrites;
   // 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);
 
@@ -393,38 +430,23 @@ 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);
   }
 
-  NodeSet::iterator atomIt;
-  Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: " << std::endl << std::endl;
+  std::set<Node>::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 != end; ++it) {
+  for(it = atoms.begin(); it != atoms.end(); ++it) {
     Debug("pf::pm") << "\tTerm: " << (*it).toExpr() << std::endl;
     d_theoryProof->registerTerm((*it).toExpr());
   }
@@ -444,9 +466,15 @@ 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";
+  out << " ;; Printing deferred declarations \n\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);
 
@@ -464,10 +492,6 @@ 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;
@@ -496,6 +520,8 @@ 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 _ ";
 
@@ -506,7 +532,6 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions,
 
     os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n";
     paren << "))";
-
   }
 
   os << "\n";
@@ -568,6 +593,14 @@ 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: