diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-09-03 16:33:33 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-03 23:33:33 +0000 |
commit | 1eb3c6c8eb3da95cababcc0b1705c0299eee099c (patch) | |
tree | 72233917af15c553dfbbf59f1125952cab83c89b /src/theory | |
parent | 5cef06bd2beff38a911c74ec082d9789eed83421 (diff) |
EnvObj: Add options(), context(), userContext(). (#7137)
This further renames EnvObj::getLogicInfo to EnvObj::logicInfo.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 9 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 55 | ||||
-rw-r--r-- | src/theory/model_manager.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 2 | ||||
-rw-r--r-- | src/theory/sep/theory_sep.cpp | 2 | ||||
-rw-r--r-- | src/theory/sets/theory_sets.cpp | 2 | ||||
-rw-r--r-- | src/theory/sort_inference.cpp | 2 | ||||
-rw-r--r-- | src/theory/theory.cpp | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 45 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 13 | ||||
-rw-r--r-- | src/theory/theory_model_builder.cpp | 12 | ||||
-rw-r--r-- | src/theory/theory_state.cpp | 12 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 25 |
14 files changed, 86 insertions, 100 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index ccdf5a90a..500b1edcd 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -46,7 +46,7 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation) d_eqSolver(nullptr), d_internal(new TheoryArithPrivate(*this, env, d_bab)), d_nonlinearExtension(nullptr), - d_opElim(d_pnm, getLogicInfo()), + d_opElim(d_pnm, logicInfo()), d_arithPreproc(d_astate, d_im, d_pnm, d_opElim), d_rewriter(d_opElim) { @@ -87,8 +87,8 @@ bool TheoryArith::needsEqualityEngine(EeSetupInfo& esi) } void TheoryArith::finishInit() { - if (getLogicInfo().isTheoryEnabled(THEORY_ARITH) - && getLogicInfo().areTranscendentalsUsed()) + const LogicInfo& logic = logicInfo(); + if (logic.isTheoryEnabled(THEORY_ARITH) && logic.areTranscendentalsUsed()) { // witness is used to eliminate square root d_valuation.setUnevaluatedKind(kind::WITNESS); @@ -98,8 +98,7 @@ void TheoryArith::finishInit() d_valuation.setUnevaluatedKind(kind::PI); } // only need to create nonlinear extension if non-linear logic - const LogicInfo& logicInfo = getLogicInfo(); - if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear()) + if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()) { d_nonlinearExtension.reset(new nl::NonlinearExtension(*this, d_astate)); } diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 070300b3b..347a86c1b 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -96,9 +96,9 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager() : nullptr), d_checker(), - d_pfGen(new EagerProofGenerator(d_pnm, d_env.getUserContext())), - d_constraintDatabase(d_env.getContext(), - d_env.getUserContext(), + d_pfGen(new EagerProofGenerator(d_pnm, userContext())), + d_constraintDatabase(context(), + userContext(), d_partialModel, d_congruenceManager, RaiseConflict(*this), @@ -107,15 +107,15 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_qflraStatus(Result::SAT_UNKNOWN), d_unknownsInARow(0), d_hasDoneWorkSinceCut(false), - d_learner(d_env.getUserContext()), - d_assertionsThatDoNotMatchTheirLiterals(d_env.getContext()), + d_learner(userContext()), + d_assertionsThatDoNotMatchTheirLiterals(context()), d_nextIntegerCheckVar(0), - d_constantIntegerVariables(d_env.getContext()), - d_diseqQueue(d_env.getContext(), false), + d_constantIntegerVariables(context()), + d_diseqQueue(context(), false), d_currentPropagationList(), - d_learnedBounds(d_env.getContext()), - d_preregisteredNodes(d_env.getContext()), - d_partialModel(d_env.getContext(), DeltaComputeCallback(*this)), + d_learnedBounds(context()), + d_preregisteredNodes(context()), + d_partialModel(context(), DeltaComputeCallback(*this)), d_errorSet( d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(*this)), d_tableau(), @@ -123,23 +123,22 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_tableau, d_rowTracking, BasicVarModelUpdateCallBack(*this)), - d_diosolver(d_env.getContext()), + d_diosolver(context()), d_restartsCounter(0), d_tableauSizeHasBeenModified(false), d_tableauResetDensity(1.6), d_tableauResetPeriod(10), - d_conflicts(d_env.getContext()), - d_blackBoxConflict(d_env.getContext(), Node::null()), - d_blackBoxConflictPf(d_env.getContext(), - std::shared_ptr<ProofNode>(nullptr)), - d_congruenceManager(d_env.getContext(), - d_env.getUserContext(), + d_conflicts(context()), + d_blackBoxConflict(context(), Node::null()), + d_blackBoxConflictPf(context(), std::shared_ptr<ProofNode>(nullptr)), + d_congruenceManager(context(), + userContext(), d_constraintDatabase, SetupLiteralCallBack(*this), d_partialModel, RaiseEqualityEngineConflict(*this), d_pnm), - d_cmEnabled(d_env.getContext(), options().arith.arithCongMan), + d_cmEnabled(context(), options().arith.arithCongMan), d_dualSimplex( d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), @@ -151,22 +150,22 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), d_pass1SDP(NULL), d_otherSDP(NULL), - d_lastContextIntegerAttempted(d_env.getContext(), -1), + d_lastContextIntegerAttempted(context(), -1), d_DELTA_ZERO(0), - d_approxCuts(d_env.getContext()), + d_approxCuts(context()), d_fullCheckCounter(0), - d_cutCount(d_env.getContext(), 0), - d_cutInContext(d_env.getContext()), - d_likelyIntegerInfeasible(d_env.getContext(), false), - d_guessedCoeffSet(d_env.getContext(), false), + d_cutCount(context(), 0), + d_cutInContext(context()), + d_likelyIntegerInfeasible(context(), false), + d_guessedCoeffSet(context(), false), d_guessedCoeffs(), d_treeLog(NULL), d_replayVariables(), d_replayConstraints(), d_lhsTmp(), d_approxStats(NULL), - d_attemptSolveIntTurnedOff(d_env.getUserContext(), 0), + d_attemptSolveIntTurnedOff(userContext(), 0), d_dioSolveResources(0), d_solveIntMaybeHelp(0u), d_solveIntAttempts(0u), @@ -1153,7 +1152,8 @@ void TheoryArithPrivate::setupVariableList(const VarList& vl){ if(!vl.singleton()){ // vl is the product of at least 2 variables // vl : (* v1 v2 ...) - if(getLogicInfo().isLinear()){ + if (logicInfo().isLinear()) + { throw LogicException("A non-linear fact was asserted to arithmetic in a linear logic."); } d_foundNl = true; @@ -1305,7 +1305,8 @@ void TheoryArithPrivate::releaseArithVar(ArithVar v){ ArithVar TheoryArithPrivate::requestArithVar(TNode x, bool aux, bool internal){ //TODO : The VarList trick is good enough? Assert(isLeaf(x) || VarList::isMember(x) || x.getKind() == PLUS || internal); - if(getLogicInfo().isLinear() && Variable::isDivMember(x)){ + if (logicInfo().isLinear() && Variable::isDivMember(x)) + { stringstream ss; ss << "A non-linear fact (involving div/mod/divisibility) was asserted to " "arithmetic in a linear logic: " diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp index 2b746cba1..dd06d4afd 100644 --- a/src/theory/model_manager.cpp +++ b/src/theory/model_manager.cpp @@ -46,9 +46,8 @@ ModelManager::~ModelManager() {} void ModelManager::finishInit(eq::EqualityEngineNotify* notify) { // construct the model - const LogicInfo& logicInfo = d_env.getLogicInfo(); // Initialize the model and model builder. - if (logicInfo.isQuantified()) + if (logicInfo().isQuantified()) { QuantifiersEngine* qe = d_te.getQuantifiersEngine(); Assert(qe != nullptr); diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 2b6719b27..bcd826799 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -189,7 +189,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, // check whether it is not in the current logic, e.g. non-linear arithmetic. // if so, undo replacements until it is in the current logic. - const LogicInfo& logic = getLogicInfo(); + const LogicInfo& logic = logicInfo(); if (logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear()) { fo_body = fitToLogic(sygusBody, diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 2ad475f01..67c40eaac 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -34,7 +34,7 @@ TheoryQuantifiers::TheoryQuantifiers(Env& env, OutputChannel& out, Valuation valuation) : Theory(THEORY_QUANTIFIERS, env, out, valuation), - d_qstate(env, valuation, getLogicInfo()), + d_qstate(env, valuation, logicInfo()), d_qreg(), d_treg(d_qstate, d_qreg), d_qim(*this, d_qstate, d_qreg, d_treg, d_pnm), diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index ba1680c6b..b19ba68de 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -1208,7 +1208,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { bool tn_is_monotonic = true; if( tn.isSort() ){ //TODO: use monotonicity inference - tn_is_monotonic = !getLogicInfo().isQuantified(); + tn_is_monotonic = !logicInfo().isQuantified(); }else{ tn_is_monotonic = tn.getCardinality().isInfinite(); } diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 23ac08749..8759f7056 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -146,7 +146,7 @@ TrustNode TheorySets::ppRewrite(TNode n, std::vector<SkolemLemma>& lems) if (nk == COMPREHENSION) { // set comprehension is an implicit quantifier, require it in the logic - if (!getLogicInfo().isQuantified()) + if (!logicInfo().isQuantified()) { std::stringstream ss; ss << "Set comprehensions require quantifiers in the background logic."; diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp index db2db9937..b0f2a2472 100644 --- a/src/theory/sort_inference.cpp +++ b/src/theory/sort_inference.cpp @@ -881,7 +881,7 @@ bool SortInference::isMonotonic( TypeNode tn ) { bool SortInference::isHandledApplyUf(Kind k) const { - return k == APPLY_UF && !d_env.getLogicInfo().isHigherOrder(); + return k == APPLY_UF && !logicInfo().isHigherOrder(); } } // namespace theory diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index f6513933f..0c2624d64 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -338,7 +338,7 @@ bool Theory::isLegalElimination(TNode x, TNode val) { return false; } - if (!options::produceModels() && !getLogicInfo().isQuantified()) + if (!options::produceModels() && !logicInfo().isQuantified()) { // Don't care about the model and logic is not quantified, we can eliminate. return true; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 72f3d78ac..13e41978c 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -158,7 +158,7 @@ void TheoryEngine::finishInit() if (options::relevanceFilter()) { d_relManager.reset( - new RelevanceManager(d_env.getUserContext(), theory::Valuation(this))); + new RelevanceManager(userContext(), theory::Valuation(this))); } // initialize the quantifiers engine @@ -208,14 +208,11 @@ void TheoryEngine::finishInit() ProofNodeManager* TheoryEngine::getProofNodeManager() const { return d_pnm; } -context::Context* TheoryEngine::getSatContext() const -{ - return d_env.getContext(); -} +context::Context* TheoryEngine::getSatContext() const { return context(); } context::UserContext* TheoryEngine::getUserContext() const { - return d_env.getUserContext(); + return userContext(); } TheoryEngine::TheoryEngine(Env& env) @@ -224,36 +221,34 @@ TheoryEngine::TheoryEngine(Env& env) d_logicInfo(env.getLogicInfo()), d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager() : nullptr), - d_lazyProof(d_pnm != nullptr - ? new LazyCDProof(d_pnm, - nullptr, - d_env.getUserContext(), - "TheoryEngine::LazyCDProof") - : nullptr), - d_tepg(new TheoryEngineProofGenerator(d_pnm, d_env.getUserContext())), + d_lazyProof( + d_pnm != nullptr ? new LazyCDProof( + d_pnm, nullptr, userContext(), "TheoryEngine::LazyCDProof") + : nullptr), + d_tepg(new TheoryEngineProofGenerator(d_pnm, userContext())), d_tc(nullptr), d_sharedSolver(nullptr), d_quantEngine(nullptr), - d_decManager(new DecisionManager(d_env.getUserContext())), + d_decManager(new DecisionManager(userContext())), d_relManager(nullptr), - d_inConflict(d_env.getContext(), false), + d_inConflict(context(), false), d_inSatMode(false), d_hasShutDown(false), - d_incomplete(d_env.getContext(), false), - d_incompleteTheory(d_env.getContext(), THEORY_BUILTIN), - d_incompleteId(d_env.getContext(), IncompleteId::UNKNOWN), - d_propagationMap(d_env.getContext()), - d_propagationMapTimestamp(d_env.getContext(), 0), - d_propagatedLiterals(d_env.getContext()), - d_propagatedLiteralsIndex(d_env.getContext(), 0), - d_atomRequests(d_env.getContext()), + d_incomplete(context(), false), + d_incompleteTheory(context(), THEORY_BUILTIN), + d_incompleteId(context(), IncompleteId::UNKNOWN), + d_propagationMap(context()), + d_propagationMapTimestamp(context(), 0), + d_propagatedLiterals(context()), + d_propagatedLiteralsIndex(context(), 0), + d_atomRequests(context()), d_combineTheoriesTime(smtStatisticsRegistry().registerTimer( "TheoryEngine::combineTheoriesTime")), d_true(), d_false(), d_interrupted(false), d_inPreregister(false), - d_factsAsserted(d_env.getContext(), false) + d_factsAsserted(context(), false) { for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) @@ -1063,7 +1058,7 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { Debug("theory::propagate") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl; - Trace("dtview::prop") << std::string(d_env.getContext()->getLevel(), ' ') + Trace("dtview::prop") << std::string(context()->getLevel(), ' ') << ":THEORY-PROP: " << literal << endl; // spendResource(); diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 4cc25a887..0c14f329a 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -40,7 +40,7 @@ TheoryModel::TheoryModel(Env& env, std::string name, bool enableFuncModels) d_enableFuncModels(enableFuncModels) { // must use function models when ufHo is enabled - Assert(d_enableFuncModels || !d_env.getLogicInfo().isHigherOrder()); + Assert(d_enableFuncModels || !logicInfo().isHigherOrder()); d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); } @@ -53,7 +53,7 @@ void TheoryModel::finishInit(eq::EqualityEngine* ee) d_equalityEngine = ee; // The kinds we are treating as function application in congruence d_equalityEngine->addFunctionKind( - kind::APPLY_UF, false, d_env.getLogicInfo().isHigherOrder()); + kind::APPLY_UF, false, logicInfo().isHigherOrder()); d_equalityEngine->addFunctionKind(kind::HO_APPLY); d_equalityEngine->addFunctionKind(kind::SELECT); // d_equalityEngine->addFunctionKind(kind::STORE); @@ -294,8 +294,7 @@ Node TheoryModel::getModelValue(TNode n) const // return the representative of the term in the equality engine, if it exists TypeNode t = ret.getType(); bool eeHasTerm; - if (!d_env.getLogicInfo().isHigherOrder() - && (t.isFunction() || t.isPredicate())) + if (!logicInfo().isHigherOrder() && (t.isFunction() || t.isPredicate())) { // functions are in the equality engine, but *not* as first-class members // when higher-order is disabled. In this case, we cannot query @@ -694,7 +693,7 @@ void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) { Trace("model-builder") << " Assigning function (" << f << ") to (" << f_def << ")" << endl; Assert(d_uf_models.find(f) == d_uf_models.end()); - if (d_env.getLogicInfo().isHigherOrder()) + if (logicInfo().isHigherOrder()) { //we must rewrite the function value since the definition needs to be a constant value f_def = Rewriter::rewrite( f_def ); @@ -708,7 +707,7 @@ void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) { d_uf_models[f] = f_def; } - if (d_env.getLogicInfo().isHigherOrder() && d_equalityEngine->hasTerm(f)) + if (logicInfo().isHigherOrder() && d_equalityEngine->hasTerm(f)) { Trace("model-builder-debug") << " ...function is first-class member of equality engine" << std::endl; // assign to representative if higher-order @@ -743,7 +742,7 @@ std::vector< Node > TheoryModel::getFunctionsToAssign() { Assert(d_env.getTopLevelSubstitutions().apply(n) == n); if( !hasAssignedFunctionDefinition( n ) ){ Trace("model-builder-fun-debug") << "Look at function : " << n << std::endl; - if (d_env.getLogicInfo().isHigherOrder()) + if (logicInfo().isHigherOrder()) { // if in higher-order mode, assign function definitions modulo equality Node r = getRepresentative( n ); diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 23a76d273..bbe1588d6 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -130,7 +130,7 @@ bool TheoryEngineModelBuilder::isAssignable(TNode n) { // selectors are always assignable (where we guarantee that they are not // evaluatable here) - if (!d_env.getLogicInfo().isHigherOrder()) + if (!logicInfo().isHigherOrder()) { Assert(!n.getType().isFunction()); return true; @@ -152,7 +152,7 @@ bool TheoryEngineModelBuilder::isAssignable(TNode n) else { // non-function variables, and fully applied functions - if (!d_env.getLogicInfo().isHigherOrder()) + if (!logicInfo().isHigherOrder()) { // no functions exist, all functions are fully applied Assert(n.getKind() != kind::HO_APPLY); @@ -1229,7 +1229,7 @@ bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m) void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f) { - Assert(!d_env.getLogicInfo().isHigherOrder()); + Assert(!logicInfo().isHigherOrder()); uf::UfModelTree ufmt(f); Node default_v; for (size_t i = 0; i < m->d_uf_terms[f].size(); i++) @@ -1274,7 +1274,7 @@ void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f) void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f) { - Assert(d_env.getLogicInfo().isHigherOrder()); + Assert(logicInfo().isHigherOrder()); TypeNode type = f.getType(); std::vector<TypeNode> argTypes = type.getArgTypes(); std::vector<Node> args; @@ -1398,7 +1398,7 @@ void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m) Trace("model-builder") << "Assigning function values..." << std::endl; std::vector<Node> funcs_to_assign = m->getFunctionsToAssign(); - if (d_env.getLogicInfo().isHigherOrder()) + if (logicInfo().isHigherOrder()) { // sort based on type size if higher-order Trace("model-builder") << "Sort functions by type..." << std::endl; @@ -1425,7 +1425,7 @@ void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m) Trace("model-builder") << " Function #" << k << " is " << f << std::endl; // std::map< Node, std::vector< Node > >::iterator itht = // m->d_ho_uf_terms.find( f ); - if (!d_env.getLogicInfo().isHigherOrder()) + if (!logicInfo().isHigherOrder()) { Trace("model-builder") << " Assign function value for " << f << " based on APPLY_UF" << std::endl; diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp index e3655e3ab..ec7955125 100644 --- a/src/theory/theory_state.cpp +++ b/src/theory/theory_state.cpp @@ -21,23 +21,17 @@ namespace cvc5 { namespace theory { TheoryState::TheoryState(Env& env, Valuation val) - : EnvObj(env), - d_valuation(val), - d_ee(nullptr), - d_conflict(d_env.getContext(), false) + : EnvObj(env), d_valuation(val), d_ee(nullptr), d_conflict(context(), false) { } void TheoryState::setEqualityEngine(eq::EqualityEngine* ee) { d_ee = ee; } -context::Context* TheoryState::getSatContext() const -{ - return d_env.getContext(); -} +context::Context* TheoryState::getSatContext() const { return context(); } context::UserContext* TheoryState::getUserContext() const { - return d_env.getUserContext(); + return userContext(); } bool TheoryState::hasTerm(TNode a) const diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 9c506f2ac..bdc5304e4 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -48,8 +48,8 @@ TheoryUF::TheoryUF(Env& env, d_thss(nullptr), d_ho(nullptr), d_functionsTerms(getSatContext()), - d_symb(getUserContext(), instanceName), - d_rewriter(env.getLogicInfo().isHigherOrder()), + d_symb(userContext(), instanceName), + d_rewriter(logicInfo().isHigherOrder()), d_state(env, valuation), d_im(*this, d_state, d_pnm, "theory::uf::" + instanceName, false), d_notify(d_im, *this) @@ -95,9 +95,9 @@ void TheoryUF::finishInit() { d_thss.reset(new CardinalityExtension(d_state, d_im, this)); } // The kinds we are treating as function application in congruence - d_equalityEngine->addFunctionKind( - kind::APPLY_UF, false, getLogicInfo().isHigherOrder()); - if (getLogicInfo().isHigherOrder()) + bool isHo = logicInfo().isHigherOrder(); + d_equalityEngine->addFunctionKind(kind::APPLY_UF, false, isHo); + if (isHo) { d_equalityEngine->addFunctionKind(kind::HO_APPLY); d_ho.reset(new HoExtension(d_state, d_im)); @@ -148,7 +148,7 @@ void TheoryUF::postCheck(Effort level) // check with the higher-order extension at full effort if (!d_state.isInConflict() && fullEffort(level)) { - if (getLogicInfo().isHigherOrder()) + if (logicInfo().isHigherOrder()) { d_ho->check(); } @@ -171,7 +171,7 @@ void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) { case kind::EQUAL: { - if (getLogicInfo().isHigherOrder() && options::ufHoExt()) + if (logicInfo().isHigherOrder() && options::ufHoExt()) { if (!pol && !d_state.isInConflict() && atom[0].getType().isFunction()) { @@ -186,7 +186,7 @@ void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) { if (d_thss == nullptr) { - if (!getLogicInfo().hasCardinalityConstraints()) + if (!logicInfo().hasCardinalityConstraints()) { std::stringstream ss; ss << "Cardinality constraint " << atom @@ -214,7 +214,7 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems) Kind k = node.getKind(); if (k == kind::HO_APPLY) { - if (!getLogicInfo().isHigherOrder()) + if (!logicInfo().isHigherOrder()) { std::stringstream ss; ss << "Partial function applications are only supported with " @@ -234,7 +234,7 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems) // check for higher-order // logic exception if higher-order is not enabled if (isHigherOrderType(node.getOperator().getType()) - && !getLogicInfo().isHigherOrder()) + && !logicInfo().isHigherOrder()) { std::stringstream ss; ss << "UF received an application whose operator has higher-order type " @@ -256,8 +256,7 @@ void TheoryUF::preRegisterTerm(TNode node) } // we always use APPLY_UF if not higher-order, HO_APPLY if higher-order - Assert(node.getKind() != kind::HO_APPLY - || getLogicInfo().isHigherOrder()); + Assert(node.getKind() != kind::HO_APPLY || logicInfo().isHigherOrder()); Kind k = node.getKind(); switch (k) @@ -318,7 +317,7 @@ TrustNode TheoryUF::explain(TNode literal) { return d_im.explainLit(literal); } bool TheoryUF::collectModelValues(TheoryModel* m, const std::set<Node>& termSet) { - if (getLogicInfo().isHigherOrder()) + if (logicInfo().isHigherOrder()) { // must add extensionality disequalities for all pairs of (non-disequal) // function equivalence classes. |