1 files changed, 94 insertions, 7 deletions

diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index efd39a118..82a1bd6be 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -23,6 +23,8 @@
 
 #include <iostream> 
 #include "proof/proof.h"
+#include "util/proof.h"
+
 
 // forward declarations
 namespace Minisat {
@@ -35,9 +37,24 @@ namespace prop {
   class CnfStream;
 }
 
+class SmtEngine; 
+
+typedef int ClauseId;
+
 class Proof;
 class SatProof;
 class CnfProof;
+class TheoryProof;
+
+class LFSCSatProof;
+class LFSCCnfProof;
+class LFSCTheoryProof;
+
+namespace prop {
+typedef uint64_t SatVariable;
+class SatLiteral;
+typedef std::vector<SatLiteral> SatClause; 
+}
 
 // different proof modes
 enum ProofFormat {
@@ -45,26 +62,96 @@ enum ProofFormat {
   NATIVE
 };/* 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;
   
   static ProofManager* proofManager; 
   static bool isInitialized; 
   ProofManager(ProofFormat format = LFSC);
+  ~ProofManager(); 
+protected:
+  std::string d_logic;
 public:
   static ProofManager* currentPM();
+  // initialization 
+  static void         initSatProof(Minisat::Solver* solver); 
+  static void         initCnfProof(CVC4::prop::CnfStream* cnfStream);
+  static void         initTheoryProof();
+  
+  static Proof*       getProof(SmtEngine* smt);
+  static SatProof*    getSatProof();
+  static CnfProof*    getCnfProof();
+  static TheoryProof* getTheoryProof();
 
-  static void      initSatProof(Minisat::Solver* solver); 
-  static void      initCnfProof(CVC4::prop::CnfStream* cnfStream);
+  // 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(); }
 
-  static Proof* getProof();
-  static SatProof* getSatProof();
-  static CnfProof* getCnfProof();
+  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 getInputClauseName(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 getLitName(prop::SatLiteral lit);
+  
+  void setLogic(const std::string& logic_string);
+  const std::string getLogic() const { return d_logic; }
 };/* class ProofManager */
 
+class LFSCProof : public Proof {
+  LFSCSatProof* d_satProof;
+  LFSCCnfProof* d_cnfProof;
+  LFSCTheoryProof* d_theoryProof;
+  SmtEngine* d_smtEngine; 
+public:
+  LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory); 
+  virtual void toStream(std::ostream& out);
+  virtual ~LFSCProof() {}
+};
+  
 }/* CVC4 namespace */
 
 #endif /* __CVC4__PROOF_MANAGER_H */