EnvObj: Add options(), context(), userContext(). (#7137)

This further renames EnvObj::getLogicInfo to EnvObj::logicInfo.

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.