Unsat core infrastruture and API (SMT-LIB compliance to come).

7 files changed, 300 insertions, 149 deletions

diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index 3dfb61428..22a40ff69 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -30,6 +30,8 @@ CnfProof::CnfProof(CnfStream* stream)
   : d_cnfStream(stream)
 {}
 
+CnfProof::~CnfProof() {
+}
 
 Expr CnfProof::getAtom(prop::SatVariable var) {
   prop::SatLiteral lit (var);
@@ -38,34 +40,33 @@ Expr CnfProof::getAtom(prop::SatVariable var) {
   return atom;
 }
 
-CnfProof::~CnfProof() {
-}
-
-LFSCCnfProof::iterator LFSCCnfProof::begin_atom_mapping() {
-  return iterator(*this, ProofManager::currentPM()->begin_vars());
+prop::SatLiteral CnfProof::getLiteral(TNode atom) {
+  return d_cnfStream->getLiteral(atom);
 }
 
-LFSCCnfProof::iterator LFSCCnfProof::end_atom_mapping() {
-  return iterator(*this, ProofManager::currentPM()->end_vars());
+Expr CnfProof::getAssertion(uint64_t id) {
+  return d_cnfStream->getAssertion(id).toExpr();
 }
 
-void LFSCCnfProof::printAtomMapping(std::ostream& os, std::ostream& paren) {
-  ProofManager::var_iterator it = ProofManager::currentPM()->begin_vars();
-  ProofManager::var_iterator end = ProofManager::currentPM()->end_vars();
-
-  for (;it != end;  ++it) {
-    os << "(decl_atom ";
-
-    if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) {
-      Expr atom = getAtom(*it);
-      LFSCTheoryProof::printTerm(atom, os);
-    } else {
-      // print fake atoms for all other logics
-      os << "true ";
+void LFSCCnfProof::printAtomMapping(const prop::SatClause* clause, std::ostream& os, std::ostream& paren) {
+  for (unsigned i = 0; i < clause->size(); ++i) {
+    prop::SatLiteral lit = clause->operator[](i);
+    if(d_atomsDeclared.find(lit.getSatVariable()) == d_atomsDeclared.end()) {
+      d_atomsDeclared.insert(lit.getSatVariable());
+      os << "(decl_atom ";
+      if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0 ||
+          ProofManager::currentPM()->getLogic().compare("QF_AX") == 0 ||
+          ProofManager::currentPM()->getLogic().compare("QF_SAT") == 0) {
+        Expr atom = getAtom(lit.getSatVariable());
+        LFSCTheoryProof::printTerm(atom, os);
+      } else {
+        // print fake atoms for all other logics (for now)
+        os << "true ";
+      }
+
+      os << " (\\ " << ProofManager::getVarName(lit.getSatVariable()) << " (\\ " << ProofManager::getAtomName(lit.getSatVariable()) << "\n";
+      paren << ")))";
     }
-
-    os << " (\\ " << ProofManager::getVarName(*it) << " (\\ " << ProofManager::getAtomName(*it) << "\n";
-    paren << ")))";
   }
 }
 
@@ -75,36 +76,93 @@ void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) {
 }
 
 void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) {
-  os << " ;; Input Clauses \n";
+  os << " ;; Clauses\n";
   ProofManager::clause_iterator it = ProofManager::currentPM()->begin_input_clauses();
   ProofManager::clause_iterator end = ProofManager::currentPM()->end_input_clauses();
 
   for (; it != end; ++it) {
     ClauseId id = it->first;
     const prop::SatClause* clause = it->second;
+    printAtomMapping(clause, os, paren);
     os << "(satlem _ _ ";
     std::ostringstream clause_paren;
     printClause(*clause, os, clause_paren);
-    os << " (clausify_false trust)" << clause_paren.str();
-    os << "( \\ " << ProofManager::getInputClauseName(id) << "\n";
+    os << "(clausify_false trust)" << clause_paren.str()
+       << " (\\ " << ProofManager::getInputClauseName(id) << "\n";
     paren << "))";
   }
 }
 
-
 void LFSCCnfProof::printTheoryLemmas(std::ostream& os, std::ostream& paren) {
-  os << " ;; Theory Lemmas \n";
-  ProofManager::clause_iterator it = ProofManager::currentPM()->begin_lemmas();
-  ProofManager::clause_iterator end = ProofManager::currentPM()->end_lemmas();
+  os << " ;; Theory Lemmas\n";
+  ProofManager::ordered_clause_iterator it = ProofManager::currentPM()->begin_lemmas();
+  ProofManager::ordered_clause_iterator end = ProofManager::currentPM()->end_lemmas();
+
+  for(size_t n = 0; it != end; ++it, ++n) {
+    if(n % 100 == 0) {
+      Chat() << "proving theory conflicts...(" << n << "/" << ProofManager::currentPM()->num_lemmas() << ")" << std::endl;
+    }
 
-  for (; it != end; ++it) {
     ClauseId id = it->first;
     const prop::SatClause* clause = it->second;
+    NodeBuilder<> c(kind::AND);
+    for(unsigned i = 0; i < clause->size(); ++i) {
+      prop::SatLiteral lit = (*clause)[i];
+      prop::SatVariable var = lit.getSatVariable();
+      if(lit.isNegated()) {
+        c << Node::fromExpr(getAtom(var));
+      } else {
+        c << Node::fromExpr(getAtom(var)).notNode();
+      }
+    }
+    Node cl = c;
+    if(ProofManager::getSatProof()->d_lemmaClauses.find(id) != ProofManager::getSatProof()->d_lemmaClauses.end()) {
+      uint64_t proof_id = ProofManager::getSatProof()->d_lemmaClauses[id];
+      TNode orig = d_cnfStream->getAssertion(proof_id & 0xffffffff);
+      if(((proof_id >> 32) & 0xffffffff) == RULE_ARRAYS_EXT) {
+        Debug("cores") << "; extensional lemma!" << std::endl;
+        Assert(cl.getKind() == kind::AND && cl.getNumChildren() == 2 && cl[0].getKind() == kind::EQUAL && cl[0][0].getKind() == kind::SELECT);
+        TNode myk = cl[0][0][1];
+        Debug("cores") << "; so my skolemized k is " << myk << std::endl;
+        os << "(ext _ _ " << orig[0][0] << " " << orig[0][1] << " (\\ " << myk << " (\\ " << ProofManager::getLemmaName(id) << "\n";
+        paren << ")))";
+      }
+    }
+    printAtomMapping(clause, os, paren);
     os << "(satlem _ _ ";
     std::ostringstream clause_paren;
     printClause(*clause, os, clause_paren);
-    os << " (clausify_false trust)" << clause_paren.str();
-    os << "( \\ " << ProofManager::getLemmaClauseName(id) <<"\n";
+
+    Debug("cores") << "\n;id is " << id << std::endl;
+    if(ProofManager::getSatProof()->d_lemmaClauses.find(id) != ProofManager::getSatProof()->d_lemmaClauses.end()) {
+      uint64_t proof_id = ProofManager::getSatProof()->d_lemmaClauses[id];
+      Debug("cores") << ";getting id " << int32_t(proof_id & 0xffffffff) << std::endl;
+      Assert(int32_t(proof_id & 0xffffffff) != -1);
+      TNode orig = d_cnfStream->getAssertion(proof_id & 0xffffffff);
+      Debug("cores") << "; ID is " << id << " and that's a lemma with " << ((proof_id >> 32) & 0xffffffff) << " / " << (proof_id & 0xffffffff) << std::endl;
+      Debug("cores") << "; that means the lemma was " << orig << std::endl;
+      if(((proof_id >> 32) & 0xffffffff) == RULE_ARRAYS_EXT) {
+        Debug("cores") << "; extensional" << std::endl;
+        os << "(clausify_false trust)\n";
+      } else if(proof_id == 0) {
+        // theory propagation caused conflict
+        //ProofManager::currentPM()->printProof(os, cl);
+        os << "(clausify_false trust)\n";
+      } else if(((proof_id >> 32) & 0xffffffff) == RULE_CONFLICT) {
+        os << "\n;; need to generate a (conflict) proof of " << cl << "\n";
+        //ProofManager::currentPM()->printProof(os, cl);
+        os << "(clausify_false trust)\n";
+      } else {
+        os << "\n;; need to generate a (lemma) proof of " << cl;
+        os << "\n;; DON'T KNOW HOW !!\n";
+        os << "(clausify_false trust)\n";
+      }
+    } else {
+      os << "\n;; need to generate a (conflict) proof of " << cl << "\n";
+      ProofManager::currentPM()->printProof(os, cl);
+    }
+    os << clause_paren.str()
+       << " (\\ " << ProofManager::getLemmaClauseName(id) << "\n";
     paren << "))";
   }
 }
@@ -114,10 +172,10 @@ void LFSCCnfProof::printClause(const prop::SatClause& clause, std::ostream& os,
     prop::SatLiteral lit = clause[i];
     prop::SatVariable var = lit.getSatVariable();
     if (lit.isNegated()) {
-      os << "(ast _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " ";
+      os << "(ast _ _ _ " << ProofManager::getAtomName(var) << " (\\ " << ProofManager::getLitName(lit) << " ";
       paren << "))";
     } else {
-      os << "(asf _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " ";
+      os << "(asf _ _ _ " << ProofManager::getAtomName(var) << " (\\ " << ProofManager::getLitName(lit) << " ";
       paren << "))";
     }
   }
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index b2c35c4f7..459815e60 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -30,62 +30,38 @@
 namespace CVC4 {
 namespace prop {
   class CnfStream;
-}
+}/* CVC4::prop namespace */
 
 class CnfProof;
 
-class AtomIterator {
-  CnfProof& d_cnf;
-  ProofManager::var_iterator d_it;
-
-public:
-  AtomIterator(CnfProof& cnf, const ProofManager::var_iterator& it)
-    : d_cnf(cnf), d_it(it)
-  {}
-  inline Expr operator*();
-  AtomIterator& operator++() { ++d_it; return *this; }
-  AtomIterator operator++(int) { AtomIterator x = *this; ++d_it; return x; }
-  bool operator==(const AtomIterator& it) const { return &d_cnf == &it.d_cnf && d_it == it.d_it; }
-  bool operator!=(const AtomIterator& it) const { return !(*this == it); }
-};/* class AtomIterator */
-
 class CnfProof {
 protected:
   CVC4::prop::CnfStream* d_cnfStream;
-  Expr getAtom(prop::SatVariable var);
-  friend class AtomIterator;
+  VarSet d_atomsDeclared;
 public:
   CnfProof(CVC4::prop::CnfStream* cnfStream);
 
-  typedef AtomIterator iterator;
-  virtual iterator begin_atom_mapping() = 0;
-  virtual iterator end_atom_mapping() = 0;
+  Expr getAtom(prop::SatVariable var);
+  Expr getAssertion(uint64_t id);
+  prop::SatLiteral getLiteral(TNode atom);
 
-  virtual void printAtomMapping(std::ostream& os, std::ostream& paren) = 0;
   virtual void printClauses(std::ostream& os, std::ostream& paren) = 0;
   virtual ~CnfProof();
-};
+};/* class CnfProof */
 
 class LFSCCnfProof : public CnfProof {
   void printInputClauses(std::ostream& os, std::ostream& paren);
   void printTheoryLemmas(std::ostream& os, std::ostream& paren);
   void printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren);
+  virtual void printAtomMapping(const prop::SatClause* clause, std::ostream& os, std::ostream& paren);
 
 public:
   LFSCCnfProof(CVC4::prop::CnfStream* cnfStream)
     : CnfProof(cnfStream)
   {}
 
-  virtual iterator begin_atom_mapping();
-  virtual iterator end_atom_mapping();
-
-  virtual void printAtomMapping(std::ostream& os, std::ostream& paren);
   virtual void printClauses(std::ostream& os, std::ostream& paren);
-};
-
-inline Expr AtomIterator::operator*() {
-  return d_cnf.getAtom(*d_it);
-}
+};/* class LFSCCnfProof */
 
 } /* CVC4 namespace */
 
diff --git a/src/proof/proof.h b/src/proof/proof.h
index 174913755..440279dbc 100644
--- a/src/proof/proof.h
+++ b/src/proof/proof.h
@@ -22,9 +22,9 @@
 #include "smt/options.h"
 
 #ifdef CVC4_PROOF
-#  define PROOF(x) if(options::proof()) { x; }
-#  define NULLPROOF(x) (options::proof()) ? x : NULL
-#  define PROOF_ON() options::proof()
+#  define PROOF(x) if(options::proof() || options::unsatCores()) { x; }
+#  define NULLPROOF(x) (options::proof() || options::unsatCores()) ? x : NULL
+#  define PROOF_ON() (options::proof() || options::unsatCores())
 #else /* CVC4_PROOF */
 #  define PROOF(x)
 #  define NULLPROOF(x) NULL
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 680e57d39..0cca16574 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -23,6 +23,15 @@
 #include "util/cvc4_assert.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "theory/output_channel.h"
+#include "theory/valuation.h"
+#include "util/node_visitor.h"
+#include "theory/term_registration_visitor.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/arrays/theory_arrays.h"
+#include "context/context.h"
+#include "util/hash.h"
 
 namespace CVC4 {
 
@@ -37,7 +46,8 @@ ProofManager::ProofManager(ProofFormat format):
   d_cnfProof(NULL),
   d_theoryProof(NULL),
   d_fullProof(NULL),
-  d_format(format)
+  d_format(format),
+  d_deps()
 {
 }
 
@@ -53,7 +63,7 @@ ProofManager::~ProofManager() {
     delete it->second;
   }
 
-  for(IdToClause::iterator it = d_theoryLemmas.begin();
+  for(OrderedIdToClause::iterator it = d_theoryLemmas.begin();
       it != d_theoryLemmas.end();
       ++it) {
     delete it->second;
@@ -91,11 +101,10 @@ CnfProof* ProofManager::getCnfProof() {
 }
 
 TheoryProof* ProofManager::getTheoryProof() {
-  Assert (currentPM()->d_theoryProof);
+  //Assert (currentPM()->d_theoryProof);
   return currentPM()->d_theoryProof;
 }
 
-
 void ProofManager::initSatProof(Minisat::Solver* solver) {
   Assert (currentPM()->d_satProof == NULL);
   Assert(currentPM()->d_format == LFSC);
@@ -114,35 +123,101 @@ void ProofManager::initTheoryProof() {
   currentPM()->d_theoryProof = new LFSCTheoryProof();
 }
 
-
-std::string ProofManager::getInputClauseName(ClauseId id) {return append("pb", id); }
-std::string ProofManager::getLemmaClauseName(ClauseId id) { return append("lem", id); }
+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("v", var); }
-std::string ProofManager::getAtomName(prop::SatVariable var) { return append("a", var); }
-std::string ProofManager::getLitName(prop::SatLiteral lit) {return append("l", lit.toInt()); }
+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::getAtomName(TNode atom) {
+  prop::SatLiteral lit = currentPM()->d_cnfProof->getLiteral(atom);
+  Assert(!lit.isNegated());
+  return getAtomName(lit.getSatVariable());
+}
+std::string ProofManager::getLitName(TNode lit) {
+  return getLitName(currentPM()->d_cnfProof->getLiteral(lit));
+}
+
+void ProofManager::traceDeps(TNode n) {
+  Debug("cores") << "trace deps " << n << std::endl;
+  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());
+  } else {
+    Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl;
+    if(d_deps.find(n) == d_deps.end()) {
+      InternalError("Cannot trace dependence information back to input assertion:\n`%s'", n.toString().c_str());
+    }
+    Assert(d_deps.find(n) != d_deps.end());
+    std::vector<Node> deps = (*d_deps.find(n)).second;
+    for(std::vector<Node>::const_iterator i = deps.begin(); i != deps.end(); ++i) {
+      Debug("cores") << " + tracing deps: " << n << " -deps-on- " << *i << std::endl;
+      traceDeps(*i);
+    }
+  }
+}
 
 void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind) {
-  for (unsigned i = 0; i < clause->size(); ++i) {
+  /*for (unsigned i = 0; i < clause->size(); ++i) {
     prop::SatLiteral lit = clause->operator[](i);
     d_propVars.insert(lit.getSatVariable());
-  }
+  }*/
   if (kind == INPUT) {
     d_inputClauses.insert(std::make_pair(id, clause));
-    return;
+    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] & 0xffffffff00000000) >> 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] & 0xffffffff00000000) >> 32) != RULE_INVALID) {
+        // trace dependences back to actual assertions
+        traceDeps(Node::fromExpr(e));
+      }
+    }
+  } else {
+    Assert(kind == THEORY_LEMMA);
+    d_theoryLemmas.insert(std::make_pair(id, clause));
   }
-  Assert (kind == THEORY_LEMMA);
-  d_theoryLemmas.insert(std::make_pair(id, clause));
 }
 
-void ProofManager::addAssertion(Expr formula) {
+void ProofManager::addAssertion(Expr formula, bool inUnsatCore) {
+  Debug("cores") << "assert: " << formula << std::endl;
   d_inputFormulas.insert(formula);
+  d_deps[Node::fromExpr(formula)]; // empty vector of deps
+  if(inUnsatCore || options::dumpUnsatCores()) {
+    Debug("cores") << "adding to input core forms: " << formula << std::endl;
+    d_inputCoreFormulas.insert(formula);
+  }
 }
 
-void ProofManager::setLogic(const std::string& logic_string) {
-  d_logic = logic_string;
+void ProofManager::addDependence(TNode n, TNode dep) {
+  if(dep != n) {
+    Debug("cores") << "dep: " << n << " : " << dep << std::endl;
+    if(d_deps.find(dep) == d_deps.end()) {
+      Debug("cores") << "WHERE DID " << dep << " come from ??" << std::endl;
+    }
+    //Assert(d_deps.find(dep) != d_deps.end());
+    d_deps[n].push_back(dep);
+  }
+}
+
+void ProofManager::setLogic(const LogicInfo& logic) {
+  d_logic = logic;
 }
 
+void ProofManager::printProof(std::ostream& os, TNode n) {
+  // no proofs here yet
+}
 
 LFSCProof::LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory)
   : d_satProof(sat)
@@ -157,17 +232,18 @@ 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();
   }
-  for(LFSCCnfProof::iterator i = d_cnfProof->begin_atom_mapping();
+  /*for(LFSCCnfProof::iterator i = d_cnfProof->begin_atom_mapping();
       i != d_cnfProof->end_atom_mapping();
       ++i) {
     d_theoryProof->addDeclaration(*i);
-  }
+  }*/
   d_theoryProof->printAssertions(out, paren);
+  out << " ;; Proof of empty clause follows\n";
   out << "(: (holds cln)\n";
-  d_cnfProof->printAtomMapping(out, paren);
   d_cnfProof->printClauses(out, paren);
   d_satProof->printResolutions(out, paren);
   paren <<")))\n;;";
@@ -175,5 +251,4 @@ void LFSCProof::toStream(std::ostream& out) {
   out << "\n";
 }
 
-
 } /* CVC4  namespace */
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index f428de36d..d60a3f6e3 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -20,9 +20,12 @@
 #define __CVC4__PROOF_MANAGER_H
 
 #include <iostream>
+#include <map>
 #include "proof/proof.h"
 #include "util/proof.h"
-
+#include "expr/node.h"
+#include "theory/logic_info.h"
+#include "theory/substitutions.h"
 
 // forward declarations
 namespace Minisat {
@@ -63,6 +66,7 @@ enum ProofFormat {
 std::string append(const std::string& str, uint64_t num);
 
 typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause;
+typedef std::map < ClauseId, const prop::SatClause* > OrderedIdToClause;
 typedef __gnu_cxx::hash_set<prop::SatVariable > VarSet;
 typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
 
@@ -74,6 +78,18 @@ enum ClauseKind {
   LEARNT
 };/* enum ClauseKind */
 
+enum ProofRule {
+  RULE_GIVEN,       /* input assertion */
+  RULE_DERIVED,     /* a "macro" rule */
+  RULE_RECONSTRUCT, /* prove equivalence using another method */
+  RULE_TRUST,       /* trust without evidence (escape hatch until proofs are fully supported) */
+  RULE_INVALID,     /* assert-fail if this is ever needed in proof; use e.g. for split lemmas */
+  RULE_CONFLICT,    /* re-construct as a conflict */
+
+  RULE_ARRAYS_EXT,  /* arrays, extensional */
+  RULE_ARRAYS_ROW,  /* arrays, read-over-write */
+};/* enum ProofRules */
+
 class ProofManager {
   SatProof*    d_satProof;
   CnfProof*    d_cnfProof;
@@ -81,15 +97,25 @@ class ProofManager {
 
   // information that will need to be shared across proofs
   IdToClause d_inputClauses;
-  IdToClause d_theoryLemmas;
+  OrderedIdToClause d_theoryLemmas;
+  IdToClause d_theoryPropagations;
   ExprSet    d_inputFormulas;
-  VarSet     d_propVars;
+  ExprSet    d_inputCoreFormulas;
+  ExprSet    d_outputCoreFormulas;
+  //VarSet     d_propVars;
+
+  int d_nextId;
 
   Proof* d_fullProof;
   ProofFormat d_format; // used for now only in debug builds
 
+  __gnu_cxx::hash_map< Node, std::vector<Node>, NodeHashFunction > d_deps;
+
+  // trace dependences back to unsat core
+  void traceDeps(TNode n);
+
 protected:
-  std::string d_logic;
+  LogicInfo d_logic;
 
 public:
   ProofManager(ProofFormat format = LFSC);
@@ -109,35 +135,50 @@ public:
 
   // iterators over data shared by proofs
   typedef IdToClause::const_iterator clause_iterator;
+  typedef OrderedIdToClause::const_iterator ordered_clause_iterator;
   typedef ExprSet::const_iterator assertions_iterator;
   typedef VarSet::const_iterator var_iterator;
 
   clause_iterator begin_input_clauses() const { return d_inputClauses.begin(); }
   clause_iterator end_input_clauses() const { return d_inputClauses.end(); }
+  size_t num_input_clauses() const { return d_inputClauses.size(); }
 
-  clause_iterator begin_lemmas() const { return d_theoryLemmas.begin(); }
-  clause_iterator end_lemmas() const { return d_theoryLemmas.end(); }
+  ordered_clause_iterator begin_lemmas() const { return d_theoryLemmas.begin(); }
+  ordered_clause_iterator end_lemmas() const { return d_theoryLemmas.end(); }
+  size_t num_lemmas() const { return d_theoryLemmas.size(); }
 
   assertions_iterator begin_assertions() const { return d_inputFormulas.begin(); }
   assertions_iterator end_assertions() const { return d_inputFormulas.end(); }
+  size_t num_assertions() const { return d_inputFormulas.size(); }
 
-  var_iterator begin_vars() const { return d_propVars.begin(); }
-  var_iterator end_vars() const { return d_propVars.end(); }
+  void printProof(std::ostream& os, TNode n);
 
-  void addAssertion(Expr formula);
+  void addAssertion(Expr formula, bool inUnsatCore);
   void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind);
+  // note that n depends on dep (for cores)
+  void addDependence(TNode n, TNode dep);
+
+  assertions_iterator begin_unsat_core() const { return d_outputCoreFormulas.begin(); }
+  assertions_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); }
+  size_t size_unsat_core() const { return d_outputCoreFormulas.size(); }
+
+  int nextId() { return d_nextId++; }
 
   // variable prefixes
   static std::string getInputClauseName(ClauseId id);
+  static std::string getLemmaName(ClauseId id);
   static std::string getLemmaClauseName(ClauseId id);
   static std::string getLearntClauseName(ClauseId id);
 
   static std::string getVarName(prop::SatVariable var);
   static std::string getAtomName(prop::SatVariable var);
+  static std::string getAtomName(TNode atom);
   static std::string getLitName(prop::SatLiteral lit);
+  static std::string getLitName(TNode lit);
+
+  void setLogic(const LogicInfo& logic);
+  const std::string getLogic() const { return d_logic.getLogicString(); }
 
-  void setLogic(const std::string& logic_string);
-  const std::string getLogic() const { return d_logic; }
 };/* class ProofManager */
 
 class LFSCProof : public Proof {
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index 0ace84b4d..f7b9c4889 100644
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -57,9 +57,6 @@ void printDebug (Minisat::Clause& c) {
   Debug("proof:sat") << endl;
 }
 
-
-int SatProof::d_idCounter = 0;
-
 /**
  * Converts the clause associated to id to a set of literals
  *
@@ -274,7 +271,7 @@ ClauseId SatProof::getClauseId(::Minisat::Lit lit) {
 
 Minisat::CRef SatProof::getClauseRef(ClauseId id) {
   if (d_idClause.find(id) == d_idClause.end()) {
-    Debug("proof:sat") << "proof:getClauseRef cannot find clause "<<id<<" "
+    Debug("proof:sat") << "proof:getClauseRef cannot find clause " << id << " "
                        << ((d_deleted.find(id) != d_deleted.end()) ? "deleted" : "")
                        << (isUnit(id)? "Unit" : "") << endl;
   }
@@ -318,16 +315,14 @@ bool SatProof::isLemmaClause(ClauseId id) {
   return (d_lemmaClauses.find(id) != d_lemmaClauses.end());
 }
 
-
 void SatProof::print(ClauseId id) {
   if (d_deleted.find(id) != d_deleted.end()) {
-    Debug("proof:sat") << "del"<<id;
+    Debug("proof:sat") << "del" << id;
   } else if (isUnit(id)) {
     printLit(getUnit(id));
   } else if (id == d_emptyClauseId) {
-    Debug("proof:sat") << "empty "<< endl;
-  }
-  else {
+    Debug("proof:sat") << "empty " << endl;
+  } else {
     CRef ref = getClauseRef(id);
     printClause(getClause(ref));
   }
@@ -335,7 +330,7 @@ void SatProof::print(ClauseId id) {
 
 void SatProof::printRes(ClauseId id) {
   Assert(hasResolution(id));
-  Debug("proof:sat") << "id "<< id <<": ";
+  Debug("proof:sat") << "id " << id << ": ";
   printRes(d_resChains[id]);
 }
 
@@ -364,42 +359,44 @@ void SatProof::printRes(ResChain* res) {
 
 /// registration methods
 
-ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind) {
+ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind, uint64_t proof_id) {
+  Debug("cores") << "registerClause " << proof_id << std::endl;
   Assert(clause != CRef_Undef);
   ClauseIdMap::iterator it = d_clauseId.find(clause);
   if (it == d_clauseId.end()) {
-    ClauseId newId = d_idCounter++;
+    ClauseId newId = ProofManager::currentPM()->nextId();
     d_clauseId[clause] = newId;
     d_idClause[newId] = clause;
     if (kind == INPUT) {
       Assert(d_inputClauses.find(newId) == d_inputClauses.end());
-      d_inputClauses.insert(newId);
+      d_inputClauses[newId] = proof_id;
     }
     if (kind == THEORY_LEMMA) {
       Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
-      d_lemmaClauses.insert(newId);
+      d_lemmaClauses[newId] = proof_id;
     }
   }
-  Debug("proof:sat:detailed") <<"registerClause CRef:" << clause <<" id:" << d_clauseId[clause] << " " << kind << "\n";
+  Debug("proof:sat:detailed") << "registerClause CRef:" << clause << " id:" << d_clauseId[clause] << " " << kind << " " << int32_t((proof_id >> 32) & 0xffffffff) << "\n";
   return d_clauseId[clause];
 }
 
-ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind) {
+ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id) {
+  Debug("cores") << "registerUnitClause " << kind << " " << proof_id << std::endl;
   UnitIdMap::iterator it = d_unitId.find(toInt(lit));
   if (it == d_unitId.end()) {
-    ClauseId newId = d_idCounter++;
+    ClauseId newId = ProofManager::currentPM()->nextId();
     d_unitId[toInt(lit)] = newId;
     d_idUnit[newId] = lit;
     if (kind == INPUT) {
       Assert(d_inputClauses.find(newId) == d_inputClauses.end());
-      d_inputClauses.insert(newId);
+      d_inputClauses[newId] = proof_id;
     }
     if (kind == THEORY_LEMMA) {
       Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
-      d_lemmaClauses.insert(newId);
+      d_lemmaClauses[newId] = proof_id;
     }
   }
-  Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << kind <<"\n";
+  Debug("proof:sat:detailed") << "registerUnitClause " << d_unitId[toInt(lit)] << " " << kind << "\n";
   return d_unitId[toInt(lit)];
 }
 
@@ -445,7 +442,7 @@ void SatProof::removeRedundantFromRes(ResChain* res, ClauseId id) {
     removedDfs(*it, removed, removeStack, inClause, seen);
   }
 
-  for (int i = removeStack.size()-1; i >= 0; --i) {
+  for (int i = removeStack.size() - 1; i >= 0; --i) {
     Lit lit = removeStack[i];
     CRef reason_ref = d_solver->reason(var(lit));
     ClauseId reason_id;
@@ -454,7 +451,7 @@ void SatProof::removeRedundantFromRes(ResChain* res, ClauseId id) {
       Assert(isUnit(~lit));
       reason_id = getUnitId(~lit);
     } else {
-      reason_id = registerClause(reason_ref);
+      reason_id = registerClause(reason_ref, LEARNT, uint64_t(-1));
     }
     res->addStep(lit, reason_id, !sign(lit));
   }
@@ -486,14 +483,14 @@ void SatProof::startResChain(::Minisat::CRef start) {
 }
 
 void SatProof::addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign) {
-  ClauseId id = registerClause(clause);
+  ClauseId id = registerClause(clause, LEARNT, uint64_t(-1));
   ResChain* res = d_resStack.back();
   res->addStep(lit, id, sign);
 }
 
 void SatProof::endResChain(CRef clause) {
   Assert(d_resStack.size() > 0);
-  ClauseId id = registerClause(clause);
+  ClauseId id = registerClause(clause, LEARNT, uint64_t(-1));
   ResChain* res = d_resStack.back();
   registerResolution(id, res);
   d_resStack.pop_back();
@@ -502,7 +499,7 @@ void SatProof::endResChain(CRef clause) {
 
 void SatProof::endResChain(::Minisat::Lit lit) {
   Assert(d_resStack.size() > 0);
-  ClauseId id = registerUnitClause(lit);
+  ClauseId id = registerUnitClause(lit, LEARNT, uint64_t(-1));
   ResChain* res = d_resStack.back();
   registerResolution(id, res);
   d_resStack.pop_back();
@@ -523,6 +520,7 @@ void SatProof::resolveOutUnit(::Minisat::Lit lit) {
 }
 
 void SatProof::storeUnitResolution(::Minisat::Lit lit) {
+  Debug("cores") << "STORE UNIT RESOLUTION" << std::endl;
   resolveUnit(lit);
 }
 
@@ -536,7 +534,7 @@ ClauseId SatProof::resolveUnit(::Minisat::Lit lit) {
   CRef reason_ref = d_solver->reason(var(lit));
   Assert(reason_ref != CRef_Undef);
 
-  ClauseId reason_id = registerClause(reason_ref);
+  ClauseId reason_id = registerClause(reason_ref, LEARNT, uint64_t(-1));
 
   ResChain* res = new ResChain(reason_id);
   // Here, the call to resolveUnit() can reallocate memory in the
@@ -551,7 +549,7 @@ ClauseId SatProof::resolveUnit(::Minisat::Lit lit) {
       res->addStep(l, res_id, !sign(l));
     }
   }
-  ClauseId unit_id = registerUnitClause(lit);
+  ClauseId unit_id = registerUnitClause(lit, LEARNT, uint64_t(-1));
   registerResolution(unit_id, res);
   return unit_id;
 }
@@ -561,11 +559,12 @@ void SatProof::toStream(std::ostream& out) {
   Unimplemented("native proof printing not supported yet");
 }
 
-void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit, ClauseKind kind) {
+void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit, ClauseKind kind, uint64_t proof_id) {
+  Debug("cores") << "STORE UNIT CONFLICT" << std::endl;
   Assert(!d_storedUnitConflict);
-  d_unitConflictId = registerUnitClause(conflict_lit, kind);
+  d_unitConflictId = registerUnitClause(conflict_lit, kind, proof_id);
   d_storedUnitConflict = true;
-  Debug("proof:sat:detailed") <<"storeUnitConflict " << d_unitConflictId << "\n";
+  Debug("proof:sat:detailed") << "storeUnitConflict " << d_unitConflictId << "\n";
 }
 
 void SatProof::finalizeProof(::Minisat::CRef conflict_ref) {
@@ -586,7 +585,7 @@ void SatProof::finalizeProof(::Minisat::CRef conflict_ref) {
     return;
   } else {
     Assert(!d_storedUnitConflict);
-    conflict_id = registerClause(conflict_ref); //FIXME
+    conflict_id = registerClause(conflict_ref, LEARNT, uint64_t(-1)); //FIXME
   }
 
   if(Debug.isOn("proof:sat")) {
@@ -652,11 +651,10 @@ std::string SatProof::clauseName(ClauseId id) {
   if (isInputClause(id)) {
     os << ProofManager::getInputClauseName(id);
     return os.str();
-  } else
-  if (isLemmaClause(id)) {
+  } else if (isLemmaClause(id)) {
     os << ProofManager::getLemmaClauseName(id);
     return os.str();
-  }else {
+  } else {
     os << ProofManager::getLearntClauseName(id);
     return os.str();
   }
@@ -728,10 +726,9 @@ void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream&
   ResChain* res = d_resChains[id];
   ResSteps& steps = res->getSteps();
 
-  for (int i = steps.size()-1; i >= 0; i--) {
+  for (int i = steps.size() - 1; i >= 0; --i) {
     out << "(";
     out << (steps[i].sign? "R" : "Q") << " _ _ ";
-
   }
 
   ClauseId start_id = res->getStart();
@@ -742,11 +739,13 @@ void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream&
   out << clauseName(start_id) << " ";
 
   for(unsigned i = 0; i < steps.size(); i++) {
-    out << clauseName(steps[i].id) << " "<<ProofManager::getVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit))) <<")";
+    out << clauseName(steps[i].id) << " "
+        << ProofManager::getVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit)))
+        << ") ";
   }
 
   if (id == d_emptyClauseId) {
-    out <<"(\\empty empty)";
+    out << "(\\empty empty)";
     return;
   }
 
@@ -763,6 +762,4 @@ void LFSCSatProof::printResolutions(std::ostream& out, std::ostream& paren) {
   printResolution(d_emptyClauseId, out, paren);
 }
 
-
 } /* CVC4 namespace */
-
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 7795dfa9c..ef4e7a5aa 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -86,6 +86,7 @@ typedef std::hash_map < ClauseId, ::Minisat::Lit>   IdUnitMap;
 typedef std::hash_map < int, ClauseId>            UnitIdMap; //FIXME
 typedef std::hash_map < ClauseId, ResChain*>      IdResMap;
 typedef std::hash_set < ClauseId >                IdHashSet;
+typedef std::hash_map < ClauseId, uint64_t >      IdProofRuleMap;
 typedef std::vector   < ResChain* >               ResStack;
 typedef std::hash_map <ClauseId, prop::SatClause* >     IdToSatClause;
 typedef std::set < ClauseId >                     IdSet;
@@ -115,14 +116,15 @@ protected:
   UnitIdMap           d_unitId;
   IdHashSet           d_deleted;
   IdToSatClause       d_deletedTheoryLemmas;
-  IdHashSet           d_inputClauses;
-  IdHashSet           d_lemmaClauses;
+public:
+  IdProofRuleMap      d_inputClauses;
+  IdProofRuleMap      d_lemmaClauses;
+protected:
   // resolutions
   IdResMap            d_resChains;
   ResStack            d_resStack;
   bool                d_checkRes;
 
-  static ClauseId     d_idCounter;
   const ClauseId      d_emptyClauseId;
   const ClauseId      d_nullId;
   // proxy class to break circular dependencies
@@ -144,6 +146,7 @@ protected:
   void printRes(ResChain* res);
 
   bool isInputClause(ClauseId id);
+  bool isTheoryConflict(ClauseId id);
   bool isLemmaClause(ClauseId id);
   bool isUnit(ClauseId id);
   bool isUnit(::Minisat::Lit lit);
@@ -207,10 +210,10 @@ public:
   void finalizeProof(::Minisat::CRef conflict);
 
   /// clause registration methods
-  ClauseId registerClause(const ::Minisat::CRef clause, ClauseKind kind = LEARNT);
-  ClauseId registerUnitClause(const ::Minisat::Lit lit, ClauseKind kind = LEARNT);
+  ClauseId registerClause(const ::Minisat::CRef clause, ClauseKind kind, uint64_t proof_id);
+  ClauseId registerUnitClause(const ::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id);
 
-  void storeUnitConflict(::Minisat::Lit lit, ClauseKind kind = LEARNT);
+  void storeUnitConflict(::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id);
 
   /**
    * Marks the deleted clauses as deleted. Note we may still use them in the final
@@ -242,6 +245,7 @@ public:
 protected:
   IdSet              d_seenLearnt;
   IdHashSet          d_seenInput;
+  IdHashSet          d_seenTheoryConflicts;
   IdHashSet          d_seenLemmas;
 
   inline std::string varName(::Minisat::Lit lit);