diff options
Diffstat (limited to 'src/proof/cnf_proof.h')
-rw-r--r-- | src/proof/cnf_proof.h | 42 |
1 files changed, 37 insertions, 5 deletions
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 9a2dbe655..0a932f906 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -13,7 +13,7 @@ ** ** A manager for CnfProofs. ** - ** + ** **/ #ifndef __CVC4__CNF_PROOF_H @@ -25,36 +25,68 @@ #include <ext/hash_set> #include <ext/hash_map> -#include <iostream> +#include <iostream> namespace CVC4 { namespace prop { -class CnfStream; + class CnfStream; } +class CnfProof; + +class AtomIterator { + CnfProof& d_cnf; + ProofManager::var_iterator d_it; + +public: + AtomIterator(CnfProof& cnf, const ProofManager::var_iterator& it) + : d_cnf(cnf), d_it(it) + {} + inline Expr operator*(); + AtomIterator& operator++() { ++d_it; return *this; } + AtomIterator operator++(int) { AtomIterator x = *this; ++d_it; return x; } + bool operator==(const AtomIterator& it) const { return &d_cnf == &it.d_cnf && d_it == it.d_it; } + bool operator!=(const AtomIterator& it) const { return !(*this == it); } +};/* class AtomIterator */ + class CnfProof { protected: CVC4::prop::CnfStream* d_cnfStream; Expr getAtom(prop::SatVariable var); + friend class AtomIterator; public: CnfProof(CVC4::prop::CnfStream* cnfStream); + typedef AtomIterator iterator; + virtual iterator begin_atom_mapping() = 0; + virtual iterator end_atom_mapping() = 0; + virtual void printAtomMapping(std::ostream& os, std::ostream& paren) = 0; virtual void printClauses(std::ostream& os, std::ostream& paren) = 0; - virtual ~CnfProof(); + virtual ~CnfProof(); }; -class LFSCCnfProof: public CnfProof { +class LFSCCnfProof : public CnfProof { void printInputClauses(std::ostream& os, std::ostream& paren); void printTheoryLemmas(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) {} + + virtual iterator begin_atom_mapping(); + virtual iterator end_atom_mapping(); + virtual void printAtomMapping(std::ostream& os, std::ostream& paren); virtual void printClauses(std::ostream& os, std::ostream& paren); }; +inline Expr AtomIterator::operator*() { + return d_cnf.getAtom(*d_it); +} + } /* CVC4 namespace */ + #endif /* __CVC4__CNF_PROOF_H */ |