diff options
Diffstat (limited to 'src/theory/uf/theory_uf.cpp')
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 25 |
1 files changed, 12 insertions, 13 deletions
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. |