diff options
Diffstat (limited to 'src/proof/proof_manager.h')
-rw-r--r-- | src/proof/proof_manager.h | 32 |
1 files changed, 20 insertions, 12 deletions
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index ec845e41d..704d8c45d 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -31,6 +31,7 @@ #include "proof/proof.h" #include "proof/proof_utils.h" #include "proof/skolemization_manager.h" +#include "smt/environment.h" #include "theory/logic_info.h" #include "theory/substitutions.h" #include "util/proof.h" @@ -141,6 +142,8 @@ private: }; class ProofManager { + Environment* d_env; + context::Context* d_context; CoreSatProof* d_satProof; @@ -172,36 +175,39 @@ class ProofManager { protected: LogicInfo d_logic; -public: - ProofManager(context::Context* context, ProofFormat format = LFSC); + public: + ProofManager(Environment* env, + context::Context* context, + ProofFormat format = LFSC); ~ProofManager(); static ProofManager* currentPM(); // initialization - void initSatProof(Minisat::Solver* solver); - static void initCnfProof(CVC4::prop::CnfStream* cnfStream, - context::Context* ctx); - static void initTheoryProofEngine(); + void initSatProof(Minisat::Solver* solver); + static void initCnfProof(CVC4::prop::CnfStream* cnfStream, + context::Context* ctx); + static void initTheoryProofEngine(); // getting various proofs static const Proof& getProof(SmtEngine* smt); - static CoreSatProof* getSatProof(); - static CnfProof* getCnfProof(); + static CoreSatProof* getSatProof(); + static CnfProof* getCnfProof(); static TheoryProofEngine* getTheoryProofEngine(); - static TheoryProof* getTheoryProof( theory::TheoryId id ); + static TheoryProof* getTheoryProof(theory::TheoryId id); static UFProof* getUfProof(); static proof::ResolutionBitVectorProof* getBitVectorProof(); static ArrayProof* getArrayProof(); static ArithProof* getArithProof(); - static SkolemizationManager *getSkolemizationManager(); + static SkolemizationManager* getSkolemizationManager(); // iterators over data shared by proofs typedef ExprSet::const_iterator assertions_iterator; // iterate over the assertions (these are arbitrary boolean formulas) - assertions_iterator begin_assertions() const { + assertions_iterator begin_assertions() const + { return d_inputFormulas.begin(); } assertions_iterator end_assertions() const { return d_inputFormulas.end(); } @@ -350,7 +356,8 @@ public: class LFSCProof : public Proof { public: - LFSCProof(SmtEngine* smtEngine, + LFSCProof(Environment* env, + SmtEngine* smtEngine, CoreSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProofEngine* theory); @@ -367,6 +374,7 @@ class LFSCProof : public Proof void checkUnrewrittenAssertion(const NodeSet& assertions) const; + Environment* d_env; CoreSatProof* d_satProof; LFSCCnfProof* d_cnfProof; LFSCTheoryProofEngine* d_theoryProof; |