diff options
35 files changed, 185 insertions, 315 deletions
diff --git a/src/smt/env.cpp b/src/smt/env.cpp index b6cdfb67b..a4e07d2c9 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -19,6 +19,7 @@ #include "context/context.h" #include "expr/node.h" #include "options/base_options.h" +#include "options/smt_options.h" #include "printer/printer.h" #include "proof/conv_proof_generator.h" #include "smt/dump_manager.h" @@ -80,6 +81,14 @@ NodeManager* Env::getNodeManager() const { return d_nodeManager; } ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; } +bool Env::isTheoryProofProducing() const +{ + return d_proofNodeManager != nullptr + && (!d_options.smt.unsatCores + || d_options.smt.unsatCoresMode + == options::UnsatCoresMode::FULL_PROOF); +} + theory::Rewriter* Env::getRewriter() { return d_rewriter.get(); } theory::TrustSubstitutionMap& Env::getTopLevelSubstitutions() diff --git a/src/smt/env.h b/src/smt/env.h index 57b5ad9c7..fa2fe6ab8 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -82,6 +82,14 @@ class Env */ ProofNodeManager* getProofNodeManager(); + /** + * Check whether theories should produce proofs as well. Other than whether + * the proof node manager is set, theory engine proofs are conditioned on the + * relationship between proofs and unsat cores: the unsat cores are in + * FULL_PROOF mode, no proofs are generated on theory engine. + */ + bool isTheoryProofProducing() const; + /** Get a pointer to the Rewriter owned by this Env. */ theory::Rewriter* getRewriter(); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 503d9d1db..595a3808c 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -52,15 +52,7 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo) { // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) - d_theoryEngine.reset(new TheoryEngine( - d_env, - // Other than whether d_pm is set, theory engine proofs are conditioned on - // the relationshup between proofs and unsat cores: the unsat cores are in - // FULL_PROOF mode, no proofs are generated on theory engine. - (options::unsatCores() - && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF) - ? nullptr - : d_pnm)); + d_theoryEngine.reset(new TheoryEngine(d_env)); // Add the theories for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 2c7187089..8cb607dd7 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -35,24 +35,20 @@ namespace cvc5 { namespace theory { namespace arith { -TheoryArith::TheoryArith(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, pnm), +TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation) + : Theory(THEORY_ARITH, env, out, valuation), d_ppRewriteTimer(smtStatisticsRegistry().registerTimer( "theory::arith::ppRewriteTimer")), - d_astate(c, u, valuation), - d_im(*this, d_astate, pnm), - d_ppre(c, pnm), - d_bab(d_astate, d_im, d_ppre, pnm), + d_astate(getSatContext(), getUserContext(), valuation), + d_im(*this, d_astate, d_pnm), + d_ppre(getSatContext(), d_pnm), + d_bab(d_astate, d_im, d_ppre, d_pnm), d_eqSolver(nullptr), - d_internal(new TheoryArithPrivate(*this, c, u, d_bab, pnm)), + d_internal(new TheoryArithPrivate( + *this, getSatContext(), getUserContext(), d_bab, d_pnm)), d_nonlinearExtension(nullptr), - d_opElim(pnm, logicInfo), - d_arithPreproc(d_astate, d_im, pnm, d_opElim), + d_opElim(d_pnm, getLogicInfo()), + d_arithPreproc(d_astate, d_im, d_pnm, d_opElim), d_rewriter(d_opElim) { // currently a cyclic dependency to TheoryArithPrivate diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index ee99f44e8..4b0c88fd2 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -44,12 +44,7 @@ class TheoryArithPrivate; class TheoryArith : public Theory { friend class TheoryArithPrivate; public: - TheoryArith(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm = nullptr); + TheoryArith(Env& env, OutputChannel& out, Valuation valuation); virtual ~TheoryArith(); //--------------------------------- initialization diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 6c9c162ab..eaa9c9294 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -55,14 +55,11 @@ const bool d_solveWrite2 = false; //bool d_useNonLinearOpt = true; //bool d_eagerIndexSplitting = false; -TheoryArrays::TheoryArrays(context::Context* c, - context::UserContext* u, +TheoryArrays::TheoryArrays(Env& env, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm, std::string name) - : Theory(THEORY_ARRAYS, c, u, out, valuation, logicInfo, pnm, name), + : Theory(THEORY_ARRAYS, env, out, valuation, name), d_numRow( smtStatisticsRegistry().registerInt(name + "number of Row lemmas")), d_numExt( @@ -83,37 +80,37 @@ TheoryArrays::TheoryArrays(context::Context* c, name + "number of setModelVal splits")), d_numSetModelValConflicts(smtStatisticsRegistry().registerInt( name + "number of setModelVal conflicts")), - d_ppEqualityEngine(u, name + "pp", true), - d_ppFacts(u), - d_rewriter(pnm), - d_state(c, u, valuation), - d_im(*this, d_state, pnm), - d_literalsToPropagate(c), - d_literalsToPropagateIndex(c, 0), - d_isPreRegistered(c), - d_mayEqualEqualityEngine(c, name + "mayEqual", true), + d_ppEqualityEngine(getUserContext(), name + "pp", true), + d_ppFacts(getUserContext()), + d_rewriter(d_pnm), + d_state(getSatContext(), getUserContext(), valuation), + d_im(*this, d_state, d_pnm), + d_literalsToPropagate(getSatContext()), + d_literalsToPropagateIndex(getSatContext(), 0), + d_isPreRegistered(getSatContext()), + d_mayEqualEqualityEngine(getSatContext(), name + "mayEqual", true), d_notify(*this), - d_backtracker(c), - d_infoMap(c, &d_backtracker, name), - d_mergeQueue(c), + d_backtracker(getSatContext()), + d_infoMap(getSatContext(), &d_backtracker, name), + d_mergeQueue(getSatContext()), d_mergeInProgress(false), - d_RowQueue(c), - d_RowAlreadyAdded(u), - d_sharedArrays(c), - d_sharedOther(c), - d_sharedTerms(c, false), - d_reads(c), - d_constReadsList(c), + d_RowQueue(getSatContext()), + d_RowAlreadyAdded(getUserContext()), + d_sharedArrays(getSatContext()), + d_sharedOther(getSatContext()), + d_sharedTerms(getSatContext(), false), + d_reads(getSatContext()), + d_constReadsList(getSatContext()), d_constReadsContext(new context::Context()), - d_contextPopper(c, d_constReadsContext), - d_skolemIndex(c, 0), - d_decisionRequests(c), - d_permRef(c), - d_modelConstraints(c), - d_lemmasSaved(c), - d_defValues(c), + d_contextPopper(getSatContext(), d_constReadsContext), + d_skolemIndex(getSatContext(), 0), + d_decisionRequests(getSatContext()), + d_permRef(getSatContext()), + d_modelConstraints(getSatContext()), + d_lemmasSaved(getSatContext()), + d_defValues(getSatContext()), d_readTableContext(new context::Context()), - d_arrayMerges(c), + d_arrayMerges(getSatContext()), d_inCheckModel(false), d_dstrat(new TheoryArraysDecisionStrategy(this)), d_dstratInit(false) diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 772fc1b79..d255e44f1 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -132,12 +132,9 @@ class TheoryArrays : public Theory { IntStat d_numSetModelValConflicts; public: - TheoryArrays(context::Context* c, - context::UserContext* u, + TheoryArrays(Env& env, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm = nullptr, std::string name = "theory::arrays::"); ~TheoryArrays(); diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index 580d26c08..42a1e2c6b 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -27,15 +27,10 @@ namespace cvc5 { namespace theory { namespace bags { -TheoryBags::TheoryBags(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_BAGS, c, u, out, valuation, logicInfo, pnm), - d_state(c, u, valuation), - d_im(*this, d_state, pnm), +TheoryBags::TheoryBags(Env& env, OutputChannel& out, Valuation valuation) + : Theory(THEORY_BAGS, env, out, valuation), + d_state(getSatContext(), getUserContext(), valuation), + d_im(*this, d_state, d_pnm), d_ig(&d_state, &d_im), d_notify(*this, d_im), d_statistics(), diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h index 4ed131e64..671623d05 100644 --- a/src/theory/bags/theory_bags.h +++ b/src/theory/bags/theory_bags.h @@ -36,12 +36,7 @@ class TheoryBags : public Theory { public: /** Constructs a new instance of TheoryBags w.r.t. the provided contexts. */ - TheoryBags(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm); + TheoryBags(Env& env, OutputChannel& out, Valuation valuation); ~TheoryBags() override; //--------------------------------- initialization diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 3aac5ecfb..33bb820b4 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -32,13 +32,8 @@ namespace cvc5 { namespace theory { namespace booleans { -TheoryBool::TheoryBool(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo, pnm) +TheoryBool::TheoryBool(Env& env, OutputChannel& out, Valuation valuation) + : Theory(THEORY_BOOL, env, out, valuation) { } diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index dd574a455..e0b7e6511 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -29,12 +29,7 @@ namespace booleans { class TheoryBool : public Theory { public: - TheoryBool(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm = nullptr); + TheoryBool(Env& env, OutputChannel& out, Valuation valuation); /** get the official theory rewriter of this theory */ TheoryRewriter* getTheoryRewriter() override; diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index 1db03d22b..f12d2caf9 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -25,15 +25,10 @@ namespace cvc5 { namespace theory { namespace builtin { -TheoryBuiltin::TheoryBuiltin(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo, pnm), - d_state(c, u, valuation), - d_im(*this, d_state, pnm, "theory::builtin::") +TheoryBuiltin::TheoryBuiltin(Env& env, OutputChannel& out, Valuation valuation) + : Theory(THEORY_BUILTIN, env, out, valuation), + d_state(getSatContext(), getUserContext(), valuation), + d_im(*this, d_state, d_pnm, "theory::builtin::") { // indicate we are using the default theory state and inference managers d_theoryState = &d_state; diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index 72485f0ea..29a3cfb36 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -31,12 +31,7 @@ namespace builtin { class TheoryBuiltin : public Theory { public: - TheoryBuiltin(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm = nullptr); + TheoryBuiltin(Env& env, OutputChannel& out, Valuation valuation); /** get the official theory rewriter of this theory */ TheoryRewriter* getTheoryRewriter() override; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 547d24b23..1976177b7 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -30,35 +30,33 @@ namespace cvc5 { namespace theory { namespace bv { -TheoryBV::TheoryBV(context::Context* c, - context::UserContext* u, +TheoryBV::TheoryBV(Env& env, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm, std::string name) - : Theory(THEORY_BV, c, u, out, valuation, logicInfo, pnm, name), + : Theory(THEORY_BV, env, out, valuation, name), d_internal(nullptr), d_rewriter(), - d_state(c, u, valuation), + d_state(getSatContext(), getUserContext(), valuation), d_im(*this, d_state, nullptr, "theory::bv::"), d_notify(d_im), - d_invalidateModelCache(c, true), + d_invalidateModelCache(getSatContext(), true), d_stats("theory::bv::") { switch (options::bvSolver()) { case options::BVSolver::BITBLAST: - d_internal.reset(new BVSolverBitblast(&d_state, d_im, pnm)); + d_internal.reset(new BVSolverBitblast(&d_state, d_im, d_pnm)); break; case options::BVSolver::LAYERED: - d_internal.reset(new BVSolverLayered(*this, c, u, pnm, name)); + d_internal.reset(new BVSolverLayered( + *this, getSatContext(), getUserContext(), d_pnm, name)); break; default: AlwaysAssert(options::bvSolver() == options::BVSolver::BITBLAST_INTERNAL); - d_internal.reset(new BVSolverBitblastInternal(&d_state, d_im, pnm)); + d_internal.reset(new BVSolverBitblastInternal(&d_state, d_im, d_pnm)); } d_theoryState = &d_state; d_inferManager = &d_im; diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index da44d7022..b4afb5f5d 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -39,12 +39,9 @@ class TheoryBV : public Theory friend class BVSolverLayered; public: - TheoryBV(context::Context* c, - context::UserContext* u, + TheoryBV(Env& env, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm = nullptr, std::string name = ""); ~TheoryBV(); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 50c955d48..759cc4c87 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -47,24 +47,21 @@ namespace cvc5 { namespace theory { namespace datatypes { -TheoryDatatypes::TheoryDatatypes(Context* c, - UserContext* u, +TheoryDatatypes::TheoryDatatypes(Env& env, OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo, pnm), - d_term_sk(u), - d_labels(c), - d_selector_apps(c), - d_collectTermsCache(c), - d_collectTermsCacheU(u), - d_functionTerms(c), - d_singleton_eq(u), - d_lemmas_produced_c(u), + Valuation valuation) + : Theory(THEORY_DATATYPES, env, out, valuation), + d_term_sk(getUserContext()), + d_labels(getSatContext()), + d_selector_apps(getSatContext()), + d_collectTermsCache(getSatContext()), + d_collectTermsCacheU(getUserContext()), + d_functionTerms(getSatContext()), + d_singleton_eq(getUserContext()), + d_lemmas_produced_c(getUserContext()), d_sygusExtension(nullptr), - d_state(c, u, valuation), - d_im(*this, d_state, pnm), + d_state(getSatContext(), getUserContext(), valuation), + d_im(*this, d_state, d_pnm), d_notify(d_im, *this) { diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 951aea804..ecfa6f02a 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -183,12 +183,7 @@ private: void computeCareGraph() override; public: - TheoryDatatypes(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm = nullptr); + TheoryDatatypes(Env& env, OutputChannel& out, Valuation valuation); ~TheoryDatatypes(); //--------------------------------- initialization diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 9b5ac66d3..a016c7897 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -60,24 +60,19 @@ Node buildConjunct(const std::vector<TNode> &assumptions) { } // namespace helper /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */ -TheoryFp::TheoryFp(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_FP, c, u, out, valuation, logicInfo, pnm), +TheoryFp::TheoryFp(Env& env, OutputChannel& out, Valuation valuation) + : Theory(THEORY_FP, env, out, valuation), d_notification(*this), - d_registeredTerms(u), - d_conv(new FpConverter(u)), + d_registeredTerms(getUserContext()), + d_conv(new FpConverter(getUserContext())), d_expansionRequested(false), - d_realToFloatMap(u), - d_floatToRealMap(u), - d_abstractionMap(u), - d_rewriter(u), - d_state(c, u, valuation), - d_im(*this, d_state, pnm, "theory::fp::", false), - d_wbFactsCache(u) + d_realToFloatMap(getUserContext()), + d_floatToRealMap(getUserContext()), + d_abstractionMap(getUserContext()), + d_rewriter(getUserContext()), + d_state(getSatContext(), getUserContext(), valuation), + d_im(*this, d_state, d_pnm, "theory::fp::", false), + d_wbFactsCache(getUserContext()) { // indicate we are using the default theory state and inference manager d_theoryState = &d_state; diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 14779cc3d..1e1041980 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -39,12 +39,7 @@ class TheoryFp : public Theory { public: /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */ - TheoryFp(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm = nullptr); + TheoryFp(Env& env, OutputChannel& out, Valuation valuation); //--------------------------------- initialization /** Get the official theory rewriter of this theory. */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index c74146c9c..3adf53b57 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -30,17 +30,14 @@ namespace cvc5 { namespace theory { namespace quantifiers { -TheoryQuantifiers::TheoryQuantifiers(Context* c, - context::UserContext* u, +TheoryQuantifiers::TheoryQuantifiers(Env& env, OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm), - d_qstate(c, u, valuation, logicInfo), + Valuation valuation) + : Theory(THEORY_QUANTIFIERS, env, out, valuation), + d_qstate(getSatContext(), getUserContext(), valuation, getLogicInfo()), d_qreg(), d_treg(d_qstate, d_qreg), - d_qim(*this, d_qstate, d_qreg, d_treg, pnm), + d_qim(*this, d_qstate, d_qreg, d_treg, d_pnm), d_qengine(nullptr) { out.handleUserAttribute( "fun-def", this ); @@ -50,7 +47,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, out.handleUserAttribute( "quant-elim-partial", this ); // construct the quantifiers engine - d_qengine.reset(new QuantifiersEngine(d_qstate, d_qreg, d_treg, d_qim, pnm)); + d_qengine.reset( + new QuantifiersEngine(d_qstate, d_qreg, d_treg, d_qim, d_pnm)); // indicate we are using the quantifiers theory state object d_theoryState = &d_qstate; diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 544be84d6..0ef5cfcbb 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -37,12 +37,7 @@ class QuantifiersMacros; class TheoryQuantifiers : public Theory { public: - TheoryQuantifiers(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm = nullptr); + TheoryQuantifiers(Env& env, OutputChannel& out, Valuation valuation); ~TheoryQuantifiers(); //--------------------------------- initialization diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 98130beb5..0b16ddd27 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -42,20 +42,15 @@ namespace cvc5 { namespace theory { namespace sep { -TheorySep::TheorySep(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_SEP, c, u, out, valuation, logicInfo, pnm), - d_lemmas_produced_c(u), +TheorySep::TheorySep(Env& env, OutputChannel& out, Valuation valuation) + : Theory(THEORY_SEP, env, out, valuation), + d_lemmas_produced_c(getUserContext()), d_bounds_init(false), - d_state(c, u, valuation), - d_im(*this, d_state, pnm, "theory::sep::"), + d_state(getSatContext(), getUserContext(), valuation), + d_im(*this, d_state, d_pnm, "theory::sep::"), d_notify(*this), - d_reduce(u), - d_spatial_assertions(c) + d_reduce(getUserContext()), + d_spatial_assertions(getSatContext()) { d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index b028f0686..985513fd8 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -77,12 +77,7 @@ class TheorySep : public Theory { bool underSpatial); public: - TheorySep(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm = nullptr); + TheorySep(Env& env, OutputChannel& out, Valuation valuation); ~TheorySep(); /** diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 718077888..5ea13ea4d 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -27,17 +27,12 @@ namespace cvc5 { namespace theory { namespace sets { -TheorySets::TheorySets(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm), +TheorySets::TheorySets(Env& env, OutputChannel& out, Valuation valuation) + : Theory(THEORY_SETS, env, out, valuation), d_skCache(), - d_state(c, u, valuation, d_skCache), - d_im(*this, d_state, pnm), - d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache, pnm)), + d_state(getSatContext(), getUserContext(), valuation, d_skCache), + d_im(*this, d_state, d_pnm), + d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache, d_pnm)), d_notify(*d_internal.get(), d_im) { // use the official theory state and inference manager objects diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index e99d25d36..e9510d70e 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -41,12 +41,7 @@ class TheorySets : public Theory friend class TheorySetsRels; public: /** Constructs a new instance of TheorySets w.r.t. the provided contexts. */ - TheorySets(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm); + TheorySets(Env& env, OutputChannel& out, Valuation valuation); ~TheorySets() override; //--------------------------------- initialization diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index c526decf1..319a6698b 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -50,21 +50,16 @@ struct SeqModelVarAttributeId }; using SeqModelVarAttribute = expr::Attribute<SeqModelVarAttributeId, Node>; -TheoryStrings::TheoryStrings(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, pnm), +TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) + : Theory(THEORY_STRINGS, env, out, valuation), d_notify(*this), d_statistics(), - d_state(c, u, d_valuation), + d_state(getSatContext(), getUserContext(), d_valuation), d_eagerSolver(d_state), - d_termReg(d_state, d_statistics, pnm), + d_termReg(d_state, d_statistics, d_pnm), d_extTheoryCb(), - d_extTheory(d_extTheoryCb, c, u, out), - d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, pnm), + d_extTheory(d_extTheoryCb, getSatContext(), getUserContext(), out), + d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, d_pnm), d_rewriter(&d_statistics.d_rewrites), d_bsolver(d_state, d_im), d_csolver(d_state, d_im, d_termReg, d_bsolver), @@ -82,8 +77,8 @@ TheoryStrings::TheoryStrings(context::Context* c, d_csolver, d_esolver, d_statistics), - d_regexp_elim(options::regExpElimAgg(), pnm, u), - d_stringsFmf(c, u, valuation, d_termReg) + d_regexp_elim(options::regExpElimAgg(), d_pnm, getUserContext()), + d_stringsFmf(getSatContext(), getUserContext(), valuation, d_termReg) { d_termReg.finishInit(&d_im); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index fc5e47194..c1ce71cef 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -64,12 +64,7 @@ class TheoryStrings : public Theory { typedef context::CDHashSet<TypeNode, std::hash<TypeNode>> TypeNodeSet; public: - TheoryStrings(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm); + TheoryStrings(Env& env, OutputChannel& out, Valuation valuation); ~TheoryStrings(); //--------------------------------- initialization /** get the official theory rewriter of this theory */ diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 96bc85336..b774d456a 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -60,27 +60,22 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){ }/* ostream& operator<<(ostream&, Theory::Effort) */ Theory::Theory(TheoryId id, - context::Context* satContext, - context::UserContext* userContext, + Env& env, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm, std::string name) : d_id(id), - d_satContext(satContext), - d_userContext(userContext), - d_logicInfo(logicInfo), - d_facts(satContext), - d_factsHead(satContext, 0), - d_sharedTermsIndex(satContext, 0), + d_env(env), + d_facts(d_env.getContext()), + d_factsHead(d_env.getContext(), 0), + d_sharedTermsIndex(d_env.getContext(), 0), d_careGraph(nullptr), d_instanceName(name), d_checkTime(smtStatisticsRegistry().registerTimer(getStatsPrefix(id) + name + "checkTime")), d_computeCareGraphTime(smtStatisticsRegistry().registerTimer( getStatsPrefix(id) + name + "computeCareGraphTime")), - d_sharedTerms(satContext), + d_sharedTerms(d_env.getContext()), d_out(&out), d_valuation(valuation), d_equalityEngine(nullptr), @@ -88,7 +83,8 @@ Theory::Theory(TheoryId id, d_theoryState(nullptr), d_inferManager(nullptr), d_quantEngine(nullptr), - d_pnm(pnm) + d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager() + : nullptr) { } @@ -135,9 +131,12 @@ void Theory::finishInitStandalone() EeSetupInfo esi; if (needsEqualityEngine(esi)) { - // always associated with the same SAT context as the theory (d_satContext) - d_allocEqualityEngine.reset(new eq::EqualityEngine( - *esi.d_notify, d_satContext, esi.d_name, esi.d_constantsAreTriggers)); + // always associated with the same SAT context as the theory + d_allocEqualityEngine.reset( + new eq::EqualityEngine(*esi.d_notify, + getSatContext(), + esi.d_name, + esi.d_constantsAreTriggers)); // use it as the official equality engine setEqualityEngine(d_allocEqualityEngine.get()); } @@ -339,7 +338,7 @@ bool Theory::isLegalElimination(TNode x, TNode val) { return false; } - if (!options::produceModels() && !d_logicInfo.isQuantified()) + if (!options::produceModels() && !getLogicInfo().isQuantified()) { // Don't care about the model and logic is not quantified, we can eliminate. return true; @@ -467,7 +466,7 @@ void Theory::getCareGraph(CareGraph* careGraph) { bool Theory::proofsEnabled() const { - return d_pnm != nullptr; + return d_env.getProofNodeManager() != nullptr; } EqualityStatus Theory::getEqualityStatus(TNode a, TNode b) diff --git a/src/theory/theory.h b/src/theory/theory.h index 41f35601b..a857931a8 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -29,6 +29,7 @@ #include "expr/node.h" #include "options/theory_options.h" #include "proof/trust_node.h" +#include "smt/env.h" #include "theory/assertion.h" #include "theory/care_graph.h" #include "theory/logic_info.h" @@ -105,14 +106,8 @@ class Theory { /** An integer identifying the type of the theory. */ TheoryId d_id; - /** The SAT search context for the Theory. */ - context::Context* d_satContext; - - /** The user level assertion context for the Theory. */ - context::UserContext* d_userContext; - - /** Information about the logic we're operating within. */ - const LogicInfo& d_logicInfo; + /** The environment class */ + Env& d_env; /** * The assertFact() queue. @@ -169,12 +164,9 @@ class Theory { * w.r.t. the SmtEngine. */ Theory(TheoryId id, - context::Context* satContext, - context::UserContext* userContext, + Env& env, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm, std::string instance = ""); // taking : No default. /** @@ -241,9 +233,7 @@ class Theory { */ inline Assertion get(); - const LogicInfo& getLogicInfo() const { - return d_logicInfo; - } + const LogicInfo& getLogicInfo() const { return d_env.getLogicInfo(); } /** * Set separation logic heap. This is called when the location and data @@ -455,17 +445,20 @@ class Theory { } /** + * Get a reference to the environment. + */ + Env& getEnv() const { return d_env; } + + /** * Get the SAT context associated to this Theory. */ - context::Context* getSatContext() const { - return d_satContext; - } + context::Context* getSatContext() const { return d_env.getContext(); } /** * Get the context associated to this Theory. */ context::UserContext* getUserContext() const { - return d_userContext; + return d_env.getUserContext(); } /** @@ -512,7 +505,7 @@ class Theory { */ void assertFact(TNode assertion, bool isPreregistered) { Trace("theory") << "Theory<" << getId() << ">::assertFact[" - << d_satContext->getLevel() << "](" << assertion << ", " + << getSatContext()->getLevel() << "](" << assertion << ", " << (isPreregistered ? "true" : "false") << ")" << std::endl; d_facts.push_back(Assertion(assertion, isPreregistered)); } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 233ea64ed..21c22586b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -218,12 +218,12 @@ context::UserContext* TheoryEngine::getUserContext() const return d_env.getUserContext(); } -TheoryEngine::TheoryEngine(Env& env, - ProofNodeManager* pnm) +TheoryEngine::TheoryEngine(Env& env) : d_propEngine(nullptr), d_env(env), d_logicInfo(env.getLogicInfo()), - d_pnm(pnm), + d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager() + : nullptr), d_lazyProof(d_pnm != nullptr ? new LazyCDProof(d_pnm, nullptr, diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 0c4a80c98..1c42e336f 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -295,7 +295,7 @@ class TheoryEngine { public: /** Constructs a theory engine */ - TheoryEngine(Env& env, ProofNodeManager* pnm); + TheoryEngine(Env& env); /** Destroys a theory engine */ ~TheoryEngine(); @@ -314,12 +314,8 @@ class TheoryEngine { { Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL); d_theoryOut[theoryId] = new theory::EngineOutputChannel(this, theoryId); - d_theoryTable[theoryId] = new TheoryClass(getSatContext(), - getUserContext(), - *d_theoryOut[theoryId], - theory::Valuation(this), - d_logicInfo, - d_pnm); + d_theoryTable[theoryId] = + new TheoryClass(d_env, *d_theoryOut[theoryId], theory::Valuation(this)); theory::Rewriter::registerTheoryRewriter( theoryId, d_theoryTable[theoryId]->getTheoryRewriter()); } diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 4224ec854..633934f61 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -40,20 +40,17 @@ namespace theory { namespace uf { /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ -TheoryUF::TheoryUF(context::Context* c, - context::UserContext* u, +TheoryUF::TheoryUF(Env& env, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm, std::string instanceName) - : Theory(THEORY_UF, c, u, out, valuation, logicInfo, pnm, instanceName), + : Theory(THEORY_UF, env, out, valuation, instanceName), d_thss(nullptr), d_ho(nullptr), - d_functionsTerms(c), - d_symb(u, instanceName), - d_state(c, u, valuation), - d_im(*this, d_state, pnm, "theory::uf::" + instanceName, false), + d_functionsTerms(getSatContext()), + d_symb(getUserContext(), instanceName), + d_state(getSatContext(), getUserContext(), valuation), + d_im(*this, d_state, d_pnm, "theory::uf::" + instanceName, false), d_notify(d_im, *this) { d_true = NodeManager::currentNM()->mkConst( true ); diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index c953cfe5c..6f04035ed 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -98,12 +98,9 @@ private: public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUF(context::Context* c, - context::UserContext* u, + TheoryUF(Env& env, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm = nullptr, std::string instanceName = ""); ~TheoryUF(); diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index 4226f8095..c27c02925 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -206,14 +206,9 @@ template <theory::TheoryId theoryId> class DummyTheory : public theory::Theory { public: - DummyTheory(context::Context* ctxt, - context::UserContext* uctxt, - theory::OutputChannel& out, - theory::Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo, pnm), - d_state(ctxt, uctxt, valuation) + DummyTheory(Env& env, theory::OutputChannel& out, theory::Valuation valuation) + : Theory(theoryId, env, out, valuation), + d_state(getSatContext(), getUserContext(), valuation) { // use a default theory state object d_theoryState = &d_state; diff --git a/test/unit/theory/theory_white.cpp b/test/unit/theory/theory_white.cpp index 94021a9e3..915b469db 100644 --- a/test/unit/theory/theory_white.cpp +++ b/test/unit/theory/theory_white.cpp @@ -37,30 +37,19 @@ class TestTheoryWhite : public TestSmtNoFinishInit void SetUp() override { TestSmtNoFinishInit::SetUp(); - d_context = d_smtEngine->getContext(); - d_user_context = d_smtEngine->getUserContext(); - d_logicInfo.reset(new LogicInfo()); - d_logicInfo->lock(); d_smtEngine->finishInit(); delete d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN]; delete d_smtEngine->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN]; d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN] = nullptr; d_smtEngine->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN] = nullptr; - d_dummy_theory.reset(new DummyTheory<THEORY_BUILTIN>(d_context, - d_user_context, - d_outputChannel, - Valuation(nullptr), - *d_logicInfo, - nullptr)); + d_dummy_theory.reset(new DummyTheory<THEORY_BUILTIN>( + d_smtEngine->getEnv(), d_outputChannel, Valuation(nullptr))); d_outputChannel.clear(); d_atom0 = d_nodeManager->mkConst(true); d_atom1 = d_nodeManager->mkConst(false); } - Context* d_context; - UserContext* d_user_context; - std::unique_ptr<LogicInfo> d_logicInfo; DummyOutputChannel d_outputChannel; std::unique_ptr<DummyTheory<THEORY_BUILTIN>> d_dummy_theory; Node d_atom0; |