diff options
Diffstat (limited to 'src/proof/cnf_proof.h')
-rw-r--r-- | src/proof/cnf_proof.h | 42 |
1 files changed, 40 insertions, 2 deletions
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 984dc76c6..8acb7a50f 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -16,20 +16,58 @@ ** **/ -#include "cvc4_private.h" -#include "util/proof.h" #ifndef __CVC4__CNF_PROOF_H #define __CVC4__CNF_PROOF_H +#include "cvc4_private.h" +#include "util/proof.h" +#include "proof/sat_proof.h" + +#include <ext/hash_set> +#include <ext/hash_map> #include <iostream> + namespace CVC4 { namespace prop { class CnfStream; } + +typedef __gnu_cxx::hash_map < ClauseId, ::Minisat::Clause > IdToClause; +typedef __gnu_cxx::hash_set<unsigned > 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(unsigned 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 setTheoryProof(TheoryProof* theory_proof); + virtual void printAtomMapping(std::ostream& os, std::ostream& paren) = 0; + virtual void printClauses(std::ostream& os, std::ostream& paren) = 0; + +}; + +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); +public: + LFSCCnfProof(CVC4::prop::CnfStream* cnfStream) + : CnfProof(cnfStream) + {} + virtual void printAtomMapping(std::ostream& os, std::ostream& paren); + virtual void printClauses(std::ostream& os, std::ostream& paren); }; } /* CVC4 namespace */ |