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

1 files changed, 8 insertions, 32 deletions

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 */