diff options
author | lianah <lianahady@gmail.com> | 2013-10-09 15:48:42 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-10-09 15:48:42 -0400 |
commit | 44485520fae92b34e4385d4d2c4774c9dd7d0dc0 (patch) | |
tree | 6a3608afa6276e11e1a72504c439a4991e9dea41 /src/proof/cnf_proof.h | |
parent | 08c8433e4ab849024930a8c4dbe8756e13d08099 (diff) |
cleaned up proof code
Diffstat (limited to 'src/proof/cnf_proof.h')
-rw-r--r-- | src/proof/cnf_proof.h | 15 |
1 files changed, 1 insertions, 14 deletions
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 010b1429d..a550f274a 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -32,26 +32,13 @@ namespace prop { class CnfStream; } -typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause; -typedef __gnu_cxx::hash_set<prop::SatVariable > VarSet; - -class TheoryProof; - class CnfProof { protected: CVC4::prop::CnfStream* d_cnfStream; - IdToClause d_inputClauses; - IdToClause d_theoryLemmas; - VarSet d_propVars; - TheoryProof* d_theoryProof; - TheoryProof* getTheoryProof(); - Expr getAtom(prop::SatVariable var); public: CnfProof(CVC4::prop::CnfStream* cnfStream); - void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind); - void addVariable(prop::SatVariable var); - void setTheoryProof(TheoryProof* theory_proof); + virtual void printAtomMapping(std::ostream& os, std::ostream& paren) = 0; virtual void printClauses(std::ostream& os, std::ostream& paren) = 0; virtual ~CnfProof(); |