diff options
Diffstat (limited to 'src/proof/cnf_proof.h')
-rw-r--r-- | src/proof/cnf_proof.h | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 8acb7a50f..010b1429d 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -32,8 +32,8 @@ namespace prop { class CnfStream; } -typedef __gnu_cxx::hash_map < ClauseId, ::Minisat::Clause > IdToClause; -typedef __gnu_cxx::hash_set<unsigned > VarSet; +typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause; +typedef __gnu_cxx::hash_set<prop::SatVariable > VarSet; class TheoryProof; @@ -46,22 +46,21 @@ protected: TheoryProof* d_theoryProof; TheoryProof* getTheoryProof(); - Expr getAtom(unsigned var); + Expr getAtom(prop::SatVariable var); public: CnfProof(CVC4::prop::CnfStream* cnfStream); - void addInputClause(ClauseId id, const ::Minisat::Clause& clause); - void addTheoryLemma(ClauseId id, const ::Minisat::Clause& clause); - void addVariable(unsigned var); + 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(); }; class LFSCCnfProof: public CnfProof { void printInputClauses(std::ostream& os, std::ostream& paren); void printTheoryLemmas(std::ostream& os, std::ostream& paren); - void printClause(const Minisat::Clause& clause, std::ostream& os, std::ostream& paren); + void printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren); public: LFSCCnfProof(CVC4::prop::CnfStream* cnfStream) : CnfProof(cnfStream) |