diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-08-05 18:29:34 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-23 13:21:47 -0500 |
commit | ff7d33c2f75668fde0f149943e3cf1bedad1102f (patch) | |
tree | b2533c2a7bf09602d567379ea1dc3bacc9f059c3 /src/proof/cnf_proof.h | |
parent | b2bb2138543e75f64c3a794df940a221e4b5a97b (diff) |
Proof-checking code; fixups of segfaults and missing functionality in proof generation; fix bug 285.
* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line
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 */ |