Merged bit-vector and uf proof branch.

1 files changed, 336 insertions, 210 deletions

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 88d380c4f..0ae020090 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -15,13 +15,20 @@
  ** \todo document this file
  **/
 
-#include "proof/proof_manager.h"
-
-#include "base/cvc4_assert.h"
 #include "context/context.h"
+
+#include "proof/proof_manager.h"
 #include "proof/cnf_proof.h"
-#include "proof/sat_proof.h"
 #include "proof/theory_proof.h"
+#include "proof/bitvector_proof.h"
+#include "proof/proof_utils.h"
+#include "proof/sat_proof_implementation.h"
+#include "options/bv_options.h"
+
+#include "util/proof.h"
+#include "util/hash.h"
+
+#include "base/cvc4_assert.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "smt_util/node_visitor.h"
@@ -31,8 +38,7 @@
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/valuation.h"
-#include "util/hash.h"
-#include "util/proof.h"
+
 
 namespace CVC4 {
 
@@ -46,17 +52,13 @@ ProofManager::ProofManager(ProofFormat format):
   d_satProof(NULL),
   d_cnfProof(NULL),
   d_theoryProof(NULL),
-  d_inputClauses(),
-  d_theoryLemmas(),
-  d_theoryPropagations(),
   d_inputFormulas(),
   d_inputCoreFormulas(),
   d_outputCoreFormulas(),
   d_nextId(0),
   d_fullProof(NULL),
   d_format(format),
-  d_deps(),
-  d_assertion_counter(1)
+  d_deps()
 {
 }
 
@@ -65,21 +67,6 @@ ProofManager::~ProofManager() {
   delete d_cnfProof;
   delete d_theoryProof;
   delete d_fullProof;
-
-  for(IdToClause::iterator it = d_inputClauses.begin();
-      it != d_inputClauses.end();
-      ++it) {
-    delete it->second;
-  }
-
-  for(OrderedIdToClause::iterator it = d_theoryLemmas.begin();
-      it != d_theoryLemmas.end();
-      ++it) {
-    delete it->second;
-  }
-
-  // FIXME: memory leak because there are deleted theory lemmas that
-  // were not used in the SatProof
 }
 
 ProofManager* ProofManager::currentPM() {
@@ -93,13 +80,13 @@ Proof* ProofManager::getProof(SmtEngine* smt) {
   Assert (currentPM()->d_format == LFSC);
 
   currentPM()->d_fullProof = new LFSCProof(smt,
-                                           (LFSCSatProof*)getSatProof(),
+                                           (LFSCCoreSatProof*)getSatProof(),
                                            (LFSCCnfProof*)getCnfProof(),
-                                           (LFSCTheoryProof*)getTheoryProof());
+                                           (LFSCTheoryProofEngine*)getTheoryProofEngine());
   return currentPM()->d_fullProof;
 }
 
-SatProof* ProofManager::getSatProof() {
+CoreSatProof* ProofManager::getSatProof() {
   Assert (currentPM()->d_satProof);
   return currentPM()->d_satProof;
 }
@@ -109,48 +96,135 @@ CnfProof* ProofManager::getCnfProof() {
   return currentPM()->d_cnfProof;
 }
 
-TheoryProof* ProofManager::getTheoryProof() {
-  //Assert (currentPM()->d_theoryProof);
+TheoryProofEngine* ProofManager::getTheoryProofEngine() {
+  Assert (options::proof());
+  Assert (currentPM()->d_theoryProof != NULL);
   return currentPM()->d_theoryProof;
 }
 
+UFProof* ProofManager::getUfProof() {
+  Assert (options::proof());
+  TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_UF);
+  return (UFProof*)pf;
+}
+BitVectorProof* ProofManager::getBitVectorProof() {
+  Assert (options::proof());
+  TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_BV);
+  return (BitVectorProof*)pf;
+}
+
+ArrayProof* ProofManager::getArrayProof() {
+  Assert (options::proof());
+  TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARRAY);
+  return (ArrayProof*)pf;
+}
+
 void ProofManager::initSatProof(Minisat::Solver* solver) {
   Assert (currentPM()->d_satProof == NULL);
   Assert(currentPM()->d_format == LFSC);
-  currentPM()->d_satProof = new LFSCSatProof(solver);
+  currentPM()->d_satProof = new LFSCCoreSatProof(solver, "");
 }
 
-void ProofManager::initCnfProof(prop::CnfStream* cnfStream) {
-  Assert (currentPM()->d_cnfProof == NULL);
-  Assert (currentPM()->d_format == LFSC);
-  currentPM()->d_cnfProof = new LFSCCnfProof(cnfStream);
+void ProofManager::initCnfProof(prop::CnfStream* cnfStream,
+                                context::Context* ctx) {
+  ProofManager* pm = currentPM();
+  Assert (pm->d_cnfProof == NULL);
+  Assert (pm->d_format == LFSC);
+  CnfProof* cnf = new LFSCCnfProof(cnfStream, ctx, "");
+  pm->d_cnfProof = cnf;
+  Assert(pm-> d_satProof != NULL);
+  pm->d_satProof->setCnfProof(cnf);
+
+  // true and false have to be setup in a special way
+  Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
+  Node false_node = NodeManager::currentNM()->mkConst<bool>(false).notNode();
+
+  pm->d_cnfProof->pushCurrentAssertion(true_node);
+  pm->d_cnfProof->pushCurrentDefinition(true_node);
+  pm->d_cnfProof->registerConvertedClause(pm->d_satProof->getTrueUnit());
+  pm->d_cnfProof->popCurrentAssertion();
+  pm->d_cnfProof->popCurrentDefinition();
+
+  pm->d_cnfProof->pushCurrentAssertion(false_node);
+  pm->d_cnfProof->pushCurrentDefinition(false_node);
+  pm->d_cnfProof->registerConvertedClause(pm->d_satProof->getFalseUnit());
+  pm->d_cnfProof->popCurrentAssertion();
+  pm->d_cnfProof->popCurrentDefinition();
+
 }
 
-void ProofManager::initTheoryProof() {
+void ProofManager::initTheoryProofEngine(SmtGlobals* globals) {
   Assert (currentPM()->d_theoryProof == NULL);
   Assert (currentPM()->d_format == LFSC);
-  currentPM()->d_theoryProof = new LFSCTheoryProof();
+  currentPM()->d_theoryProof = new LFSCTheoryProofEngine(globals);
+}
+
+std::string ProofManager::getInputClauseName(ClauseId id,
+                                             const std::string& prefix) {
+  return append(prefix+".pb", id);
+}
+std::string ProofManager::getLemmaClauseName(ClauseId id,
+                                             const std::string& prefix) {
+  return append(prefix+".lemc", id);
 }
+  std::string ProofManager::getLemmaName(ClauseId id,
+           const std::string& prefix) {
+  return append(prefix+"lem", id);
+}
+
+std::string ProofManager::getLearntClauseName(ClauseId id,
+                                              const std::string& prefix) {
+  return append(prefix+".cl", id);
+}
+std::string ProofManager::getVarName(prop::SatVariable var,
+                                     const std::string& prefix) {
+  return append(prefix+".v", var);
+}
+std::string ProofManager::getAtomName(prop::SatVariable var,
+                                      const std::string& prefix) {
+  return append(prefix+".a", var);
+}
+std::string ProofManager::getLitName(prop::SatLiteral lit,
+                                     const std::string& prefix) {
+  return append(prefix+".l", lit.toInt());
+}
+
 
-std::string ProofManager::getInputClauseName(ClauseId id) { return append("pb", id); }
-std::string ProofManager::getLemmaName(ClauseId id) { return append("lem", id); }
-std::string ProofManager::getLemmaClauseName(ClauseId id) { return append("lemc", id); }
-std::string ProofManager::getLearntClauseName(ClauseId id) { return append("cl", id); }
-std::string ProofManager::getVarName(prop::SatVariable var) { return append("var", var); }
-std::string ProofManager::getAtomName(prop::SatVariable var) { return append("atom", var); }
-std::string ProofManager::getLitName(prop::SatLiteral lit) { return append("lit", lit.toInt()); }
+std::string ProofManager::getPreprocessedAssertionName(Node node,
+                                                       const std::string& prefix) {
+  node = node.getKind() == kind::BITVECTOR_EAGER_ATOM ? node[0] : node;
+  return append(prefix+".PA", node.getId());
+}
+std::string ProofManager::getAssertionName(Node node,
+                                           const std::string& prefix) {
+  return append(prefix+".A", node.getId());
+}
 
-std::string ProofManager::getAtomName(TNode atom) {
+std::string ProofManager::getAtomName(TNode atom,
+                                      const std::string& prefix) {
   prop::SatLiteral lit = currentPM()->d_cnfProof->getLiteral(atom);
   Assert(!lit.isNegated());
-  return getAtomName(lit.getSatVariable());
+  return getAtomName(lit.getSatVariable(), prefix);
 }
-std::string ProofManager::getLitName(TNode lit) {
-  return getLitName(currentPM()->d_cnfProof->getLiteral(lit));
+std::string ProofManager::getLitName(TNode lit,
+                                     const std::string& prefix) {
+  return getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix);
+}
+
+std::string ProofManager::sanitize(TNode var) {
+  Assert (var.isVar());
+  std::string name = var.toString();
+  std::replace(name.begin(), name.end(), ' ', '_');
+  return name;
 }
 
+
 void ProofManager::traceDeps(TNode n) {
   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))) {
+    return;
+  }
   if(d_inputCoreFormulas.find(n.toExpr()) != d_inputCoreFormulas.end()) {
     // originating formula was in core set
     Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl;
@@ -171,45 +245,38 @@ void ProofManager::traceDeps(TNode n) {
   }
 }
 
-void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind) {
-  /*for (unsigned i = 0; i < clause->size(); ++i) {
-    prop::SatLiteral lit = clause->operator[](i);
-    d_propVars.insert(lit.getSatVariable());
-  }*/
-  if (kind == INPUT) {
-    Debug("cores") << "; Add to inputClauses " << id << std::endl;
-    d_inputClauses.insert(std::make_pair(id, clause));
-    Assert(d_satProof->d_inputClauses.find(id) != d_satProof->d_inputClauses.end());
-    Debug("cores") << "; core id is " << d_satProof->d_inputClauses[id] << std::endl;
-    if(d_satProof->d_inputClauses[id] == uint64_t(-1)) {
-      Debug("cores") << "; + constant unit (true or false)" << std::endl;
-    } else if(options::unsatCores()) {
-      Expr e = d_cnfProof->getAssertion(d_satProof->d_inputClauses[id] & 0xffffffff);
-      Debug("cores") << "; core input assertion from CnfStream is " << e << std::endl;
-      Debug("cores") << "; with proof rule " << ((d_satProof->d_inputClauses[id] & 0xffffffff00000000llu) >> 32) << std::endl;
-      // Invalid proof rules are currently used for parts of CVC4 that don't
-      // support proofs (these are e.g. unproven theory lemmas) or don't need
-      // proofs (e.g. split lemmas).  We can ignore these safely when
-      // constructing unsat cores.
-      if(((d_satProof->d_inputClauses[id] & 0xffffffff00000000llu) >> 32) != RULE_INVALID) {
-        // trace dependences back to actual assertions
-        traceDeps(Node::fromExpr(e));
-      }
+void ProofManager::traceUnsatCore() {
+  Assert (options::unsatCores());
+  d_satProof->constructProof();
+  IdToSatClause used_lemmas;
+  IdToSatClause used_inputs;
+  d_satProof->collectClausesUsed(used_inputs,
+                                 used_lemmas);
+  IdToSatClause::const_iterator it = used_inputs.begin();
+  for(; it != used_inputs.end(); ++it) {
+    Node node = d_cnfProof->getAssertionForClause(it->first);
+    ProofRule rule = d_cnfProof->getProofRule(node);
+
+    Debug("cores") << "core input assertion " << node << std::endl;
+    Debug("cores") << "with proof rule " << rule << std::endl;
+    if (rule == RULE_TSEITIN ||
+        rule == RULE_GIVEN) {
+      // trace dependences back to actual assertions
+      // (this adds them to the unsat core)
+      traceDeps(node);
     }
-  } else {
-    Assert(kind == THEORY_LEMMA);
-    d_theoryLemmas.insert(std::make_pair(id, clause));
   }
 }
 
-void ProofManager::addAssertion(Expr formula, bool inUnsatCore) {
-  Debug("cores") << "assert: " << formula << std::endl;
+void ProofManager::addAssertion(Expr formula) {
+  Debug("proof:pm") << "assert: " << formula << std::endl;
   d_inputFormulas.insert(formula);
+}
+
+void ProofManager::addCoreAssertion(Expr formula) {
+  Debug("cores") << "assert: " << formula << std::endl;
   d_deps[Node::fromExpr(formula)]; // empty vector of deps
-  if(inUnsatCore || options::dumpUnsatCores() || options::checkUnsatCores()) {
-    Debug("cores") << "adding to input core forms: " << formula << std::endl;
-    d_inputCoreFormulas.insert(formula);
-  }
+  d_inputCoreFormulas.insert(formula);
 }
 
 void ProofManager::addDependence(TNode n, TNode dep) {
@@ -232,151 +299,210 @@ void ProofManager::setLogic(const LogicInfo& logic) {
   d_logic = logic;
 }
 
-void ProofManager::printProof(std::ostream& os, TNode n) {
-  // no proofs here yet
-}
 
-void ProofManager::setCnfDep( Expr child, Expr parent ) {
-  Debug("cores") << "CNF dep : " << child << " : " << parent << std::endl;
-  d_cnf_dep[child] = parent;
-}
 
-Expr ProofManager::getFormulaForClauseId( ClauseId id ) {
-  std::map< ClauseId, Expr >::const_iterator it = d_clause_id_to_assertion.find( id );
-  if( it!=d_clause_id_to_assertion.end() ){
-    return it->second;
-  }else{
-    Node ret;
-    return ret.toExpr();
-  }
-}
+LFSCProof::LFSCProof(SmtEngine* smtEngine,
+                     LFSCCoreSatProof* sat,
+                     LFSCCnfProof* cnf,
+                     LFSCTheoryProofEngine* theory)
+  : d_satProof(sat)
+  , d_cnfProof(cnf)
+  , d_theoryProof(theory)
+  , d_smtEngine(smtEngine)
+{}
 
-ProofRule ProofManager::getProofRuleForClauseId( ClauseId id ) {
-  std::map< ClauseId, ProofRule >::const_iterator it = d_clause_id_to_rule.find( id );
-  if( it!=d_clause_id_to_rule.end() ){
-    return it->second;
-  }else{
-    return RULE_INVALID;
-  }
-}
+void LFSCProof::toStream(std::ostream& out) {
+  d_satProof->constructProof();
 
-void ProofManager::setAssertion( Expr e ) {
-  d_assertion_to_id[e] = d_assertion_counter;
-  d_assertion_counter++;
-}
-
-// if this function returns true, writes to out a proof of e based on input assertions
-bool ProofManager::isInputAssertion( Expr e, std::ostream& out ) {
-  std::map< Expr, unsigned >::iterator itp = d_assertion_to_id.find( e );
-  if( itp==d_assertion_to_id.end() ){
-    //check if deduced by CNF
-    std::map< Expr, Expr >::iterator itd = d_cnf_dep.find( e );
-    if( itd!=d_cnf_dep.end() ){
-      Expr parent = itd->second;
-      //check if parent is an input assertion
-      std::stringstream out_parent;
-      if( isInputAssertion( parent, out_parent ) ){
-        if( parent.getKind()==kind::AND || ( parent.getKind()==kind::NOT && ( parent[0].getKind()==kind::IMPLIES || parent[0].getKind()==kind::OR ) ) ){
-          Expr parent_base = parent.getKind()==kind::NOT ? parent[0] : parent;
-          Expr e_base = e.getKind()==kind::NOT ? e[0] : e;
-          bool e_pol = e.getKind()!=kind::NOT;
-          for( unsigned i=0; i<parent_base.getNumChildren(); i++ ){
-            Expr child_base = parent_base[i].getKind()==kind::NOT ? parent_base[i][0] : parent_base[i];
-            bool child_pol = parent_base[i].getKind()!=kind::NOT;
-            if( parent_base.getKind()==kind::IMPLIES && i==0 ){
-              child_pol = !child_pol;
-            }
-            if( e_base==child_base && (e_pol==child_pol)==(parent_base.getKind()==kind::AND) ){
-              bool elimNn = ( ( parent_base.getKind()==kind::OR || ( parent_base.getKind()==kind::IMPLIES && i==1 ) ) && e_pol );
-              if( elimNn ){
-                out << "(not_not_elim _ ";
-              }
-              std::stringstream out_paren;
-              if( i+1<parent_base.getNumChildren() ){
-                out << "(and_elim_1 _ _ ";
-                if( parent_base.getKind()==kind::OR || parent_base.getKind()==kind::IMPLIES  ){
-                  out << "(not_" << ( parent_base.getKind()==kind::OR ? "or" : "impl" ) << "_elim _ _ ";
-                  out_paren << ")";
-                }
-                out_paren << ")";
-              }
-              for( unsigned j=0; j<i; j++ ){
-                out << "(and_elim_2 _ _ ";
-                if( parent_base.getKind()==kind::OR || parent_base.getKind()==kind::IMPLIES ){
-                  out << "(not_" << ( parent_base.getKind()==kind::OR ? "or" : "impl" ) << "_elim _ _ ";
-                  out_paren << ")";
-                }
-                out_paren << ")";
-              }
-              out << out_parent.str();
-              out << out_paren.str();
-              if( elimNn ){
-                out << ")";
-              }
-              return true;
-            }
-          }
-        }else{
-          Trace("cnf-pf-debug") << "; isInputAssertion : parent of " << e << " is not correct type (" << parent << ")" << std::endl;
-        }
-      }else{
-        Trace("cnf-pf-debug") << "; isInputAssertion : parent of " << e << " is not input" << std::endl;
-      }
-    }else{
-      Trace("cnf-pf-debug") << "; isInputAssertion : " << e << " has no parent" << std::endl;
-    }
-    return false;
-  }else{
-    out << "A" << itp->second;
-    return true;
+  // collecting leaf clauses in resolution proof
+  IdToSatClause used_lemmas;
+  IdToSatClause used_inputs;
+  d_satProof->collectClausesUsed(used_inputs,
+                                 used_lemmas);
+
+  // collecting assertions that lead to the clauses being asserted
+  NodeSet used_assertions;
+  d_cnfProof->collectAssertionsForClauses(used_inputs, used_assertions);
+
+  NodeSet atoms;
+  // collects the atoms in the clauses
+  d_cnfProof->collectAtomsForClauses(used_inputs, atoms);
+  d_cnfProof->collectAtomsForClauses(used_lemmas, atoms);
+
+  // collects the atoms in the assertions
+  for (NodeSet::const_iterator it = used_assertions.begin();
+       it != used_assertions.end(); ++it) {
+    utils::collectAtoms(*it, atoms);
   }
-}
 
-void ProofManager::setRegisteringFormula( Node n, ProofRule proof_id ) {
-  Trace("cnf-pf-debug") << "; set registering formula " << n << " proof rule = " << proof_id << std::endl;
-  d_registering_assertion = n;
-  d_registering_rule = proof_id;
-}
+  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;
+    }
 
-void ProofManager::setRegisteredClauseId( ClauseId id ) {
-  Trace("cnf-pf-debug") << "; set register clause id " << id << " " << d_registering_assertion << std::endl;
-  if( !d_registering_assertion.isNull() ){
-     d_clause_id_to_assertion[id] = d_registering_assertion.toExpr();
-     d_clause_id_to_rule[id] = d_registering_rule;
-     setRegisteringFormula( Node::null(), RULE_INVALID );
+    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;
+    }
   }
-}
 
-LFSCProof::LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory)
-  : d_satProof(sat)
-  , d_cnfProof(cnf)
-  , d_theoryProof(theory)
-  , d_smtEngine(smtEngine)
-{
-  d_satProof->constructProof();
-}
 
-void LFSCProof::toStream(std::ostream& out) {
+
   smt::SmtScope scope(d_smtEngine);
   std::ostringstream paren;
   out << "(check\n";
   out << " ;; Declarations\n";
-  if (d_theoryProof == NULL) {
-    d_theoryProof = new LFSCTheoryProof();
+
+  // declare the theory atoms
+  NodeSet::const_iterator it = atoms.begin();
+  NodeSet::const_iterator end = atoms.end();
+  for(; it != end; ++it) {
+    d_theoryProof->registerTerm((*it).toExpr());
   }
-  /*for(LFSCCnfProof::iterator i = d_cnfProof->begin_atom_mapping();
-      i != d_cnfProof->end_atom_mapping();
-      ++i) {
-    d_theoryProof->addDeclaration(*i);
-  }*/
+  // print out all the original assertions
   d_theoryProof->printAssertions(out, paren);
-  out << " ;; Proof of empty clause follows\n";
+
+
   out << "(: (holds cln)\n";
-  d_cnfProof->printClauses(out, paren);
-  d_satProof->printResolutions(out, paren);
-  paren <<")))\n;;";
-  out << paren.str();
-  out << "\n";
+
+  // print trust that input assertions are their preprocessed form
+  printPreprocessedAssertions(used_assertions, out, paren);
+
+  // print mapping between theory atoms and internal SAT variables
+  d_cnfProof->printAtomMapping(atoms, out, paren);
+
+  IdToSatClause::const_iterator cl_it = used_inputs.begin();
+  // print CNF conversion proof for each clause
+  for (; cl_it != used_inputs.end(); ++cl_it) {
+    d_cnfProof->printCnfProofForClause(cl_it->first, cl_it->second, out, paren);
+  }
+
+  // FIXME: for now assume all theory lemmas are in CNF form so
+  // distinguish between them and inputs
+  // print theory lemmas for resolution proof
+  d_theoryProof->printTheoryLemmas(used_lemmas, out, paren);
+
+
+  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) {
+    // print actual resolution proof
+    // d_satProof->printResolutions(out, paren);
+    ProofManager::getBitVectorProof()->getSatProof()->printResolutionEmptyClause(out, paren);
+    paren <<")))\n;;";
+    out << paren.str();
+    out << "\n";
+  } else {
+    // print actual resolution proof
+    d_satProof->printResolutions(out, paren);
+    d_satProof->printResolutionEmptyClause(out, paren);
+    paren <<")))\n;;";
+    out << paren.str();
+    out << "\n";
+  }
+}
+
+void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions,
+                                            std::ostream& os,
+                                            std::ostream& paren) {
+  os << " ;; Preprocessing \n";
+  NodeSet::const_iterator it = assertions.begin();
+  NodeSet::const_iterator end = assertions.end();
+
+  for (; it != end; ++it) {
+    os << "(th_let_pf _ ";
+
+    //TODO
+    os << "(trust_f ";
+    ProofManager::currentPM()->getTheoryProofEngine()->printLetTerm((*it).toExpr(), os);
+    os << ") ";
+
+    os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n";
+    paren << "))";
+
+  }
 }
 
+
+
+//---from Morgan---
+bool ProofManager::hasOp(TNode n) const {
+  return d_bops.find(n) != d_bops.end();
+}
+
+Node ProofManager::lookupOp(TNode n) const {
+  std::map<Node, Node>::const_iterator i = d_bops.find(n);
+  Assert(i != d_bops.end());
+  return (*i).second;
+}
+
+Node ProofManager::mkOp(TNode n) {
+  if(n.getKind() != kind::BUILTIN) {
+    return n;
+  }
+  Node& op = d_ops[n];
+  if(op.isNull()) {
+    Debug("mgd") << "making an op for " << n << "\n";
+    std::stringstream ss;
+    ss << n;
+    std::string s = ss.str();
+    Debug("mgd") << " : " << s << std::endl;
+    std::vector<TypeNode> v;
+    v.push_back(NodeManager::currentNM()->integerType());
+    if(n.getConst<Kind>() == kind::SELECT) {
+      v.push_back(NodeManager::currentNM()->integerType());
+      v.push_back(NodeManager::currentNM()->integerType());
+    } else if(n.getConst<Kind>() == kind::STORE) {
+      v.push_back(NodeManager::currentNM()->integerType());
+      v.push_back(NodeManager::currentNM()->integerType());
+      v.push_back(NodeManager::currentNM()->integerType());
+    }
+    TypeNode type = NodeManager::currentNM()->mkFunctionType(v);
+    op = NodeManager::currentNM()->mkSkolem(s, type, " ignore", NodeManager::SKOLEM_NO_NOTIFY);
+    d_bops[op] = n;
+  }
+  return op;
+}
+//---end from Morgan---
+
+std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k) {
+  switch(k) {
+  case RULE_GIVEN:
+    out << "RULE_GIVEN"; 
+    break;
+  case RULE_DERIVED:
+    out << "RULE_DERIVED"; 
+    break;
+  case RULE_RECONSTRUCT:
+    out << "RULE_RECONSTRUCT"; 
+    break;
+  case RULE_TRUST:
+    out << "RULE_TRUST"; 
+    break;
+  case RULE_INVALID:
+    out << "RULE_INVALID"; 
+    break;
+  case RULE_CONFLICT:
+    out << "RULE_CONFLICT"; 
+    break;
+  case RULE_TSEITIN:
+    out << "RULE_TSEITIN"; 
+    break;
+  case RULE_SPLIT:
+    out << "RULE_SPLIT"; 
+    break;
+  case RULE_ARRAYS_EXT:
+    out << "RULE_ARRAYS"; 
+    break;
+  case RULE_ARRAYS_ROW:
+    out << "RULE_ARRAYS"; 
+    break;
+  default:
+    out << "ProofRule Unknown! [" << unsigned(k) << "]";
+  }
+
+  return out;
+}
+
+
 } /* CVC4  namespace */