cleaned up proof code

1 files changed, 55 insertions, 14 deletions

diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index d4f1d6528..7642ba776 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -50,6 +50,7 @@ class LFSCTheoryProof;
 namespace prop {
 typedef uint64_t SatVariable;
 class SatLiteral;
+typedef std::vector<SatLiteral> SatClause; 
 }
 
 // different proof modes
@@ -60,11 +61,29 @@ enum ProofFormat {
 
 std::string append(const std::string& str, uint64_t num);
 
+typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause; 
+typedef __gnu_cxx::hash_set<prop::SatVariable > VarSet;
+typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
+
+typedef int ClauseId;
+
+enum ClauseKind {
+  INPUT,
+  THEORY_LEMMA,
+  LEARNT
+};
+
 class ProofManager {
-  SatProof*   d_satProof;
-  CnfProof*   d_cnfProof;
+  SatProof*    d_satProof;
+  CnfProof*    d_cnfProof;
   TheoryProof* d_theoryProof; 
 
+  // information that will need to be shared across proofs
+  IdToClause d_inputClauses;
+  IdToClause d_theoryLemmas;
+  ExprSet    d_inputFormulas;
+  VarSet     d_propVars;
+  
   Proof* d_fullProof; 
   ProofFormat d_format;
   
@@ -74,22 +93,44 @@ class ProofManager {
   ~ProofManager(); 
 public:
   static ProofManager* currentPM();
-  static void      initSatProof(Minisat::Solver* solver); 
-  static void      initCnfProof(CVC4::prop::CnfStream* cnfStream);
-  static void      initTheoryProof();
-  static Proof*    getProof();
-  static SatProof* getSatProof();
-  static CnfProof* getCnfProof();
+  // initialization 
+  static void         initSatProof(Minisat::Solver* solver); 
+  static void         initCnfProof(CVC4::prop::CnfStream* cnfStream);
+  static void         initTheoryProof();
+  
+  static Proof*       getProof();
+  static SatProof*    getSatProof();
+  static CnfProof*    getCnfProof();
   static TheoryProof* getTheoryProof();
 
+  // iterators over data shared by proofs
+  typedef IdToClause::const_iterator 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(); }
+
+  clause_iterator begin_lemmas() const { return d_theoryLemmas.begin(); }
+  clause_iterator end_lemmas() const { return d_theoryLemmas.end(); }
+
+  assertions_iterator begin_assertions() const { return d_inputFormulas.begin(); }
+  assertions_iterator end_assertions() const { return d_inputFormulas.end(); }
+
+  var_iterator begin_vars() const { return d_propVars.begin(); }
+  var_iterator end_vars() const { return d_propVars.end(); }
+  
+  void addAssertion(Expr formula);
+  void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind); 
+  
   // variable prefixes
-  static std::string printInputClauseName(ClauseId id);
-  static std::string printLemmaClauseName(ClauseId id);
-  static std::string printLearntClauseName(ClauseId id);
+  static std::string getInputClauseName(ClauseId id);
+  static std::string getLemmaClauseName(ClauseId id);
+  static std::string getLearntClauseName(ClauseId id);
 
-  static std::string printVarName(prop::SatVariable var);
-  static std::string printAtomName(prop::SatVariable var);
-  static std::string printLitName(prop::SatLiteral lit);
+  static std::string getVarName(prop::SatVariable var);
+  static std::string getAtomName(prop::SatVariable var);
+  static std::string getLitName(prop::SatLiteral lit);
 };/* class ProofManager */
 
 class LFSCProof : public Proof {