This PR changes the Theory base class and the constructors of all theories to use the Env class to access contexts, logic information and the proof node manager.
#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"
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()
*/
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();
{
// 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;
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
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
//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(
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)
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();
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(),
{
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
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)
{
}
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;
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;
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;
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;
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();
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)
{
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
} // 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;
{
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. */
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 );
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;
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
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);
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();
/**
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
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
};
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),
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);
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 */
}/* 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),
d_theoryState(nullptr),
d_inferManager(nullptr),
d_quantEngine(nullptr),
- d_pnm(pnm)
+ d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
+ : nullptr)
{
}
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());
}
{
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;
bool Theory::proofsEnabled() const
{
- return d_pnm != nullptr;
+ return d_env.getProofNodeManager() != nullptr;
}
EqualityStatus Theory::getEqualityStatus(TNode a, TNode b)
#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"
/** 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.
* 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.
/**
*/
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
return d_id;
}
+ /**
+ * 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();
}
/**
*/
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));
}
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,
public:
/** Constructs a theory engine */
- TheoryEngine(Env& env, ProofNodeManager* pnm);
+ TheoryEngine(Env& env);
/** Destroys a theory engine */
~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());
}
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 );
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();
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;
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;
projects / cvc5.git / commitdiff