Remove more instances of ufHo (#7087)

Towards replacing that option with a logic check throughout.

1 files changed, 14 insertions, 9 deletions

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 3525786d5..9c506f2ac 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -49,6 +49,7 @@ TheoryUF::TheoryUF(Env& env,
       d_ho(nullptr),
       d_functionsTerms(getSatContext()),
       d_symb(getUserContext(), instanceName),
+      d_rewriter(env.getLogicInfo().isHigherOrder()),
       d_state(env, valuation),
       d_im(*this, d_state, d_pnm, "theory::uf::" + instanceName, false),
       d_notify(d_im, *this)
@@ -94,8 +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, options::ufHo());
-  if (options::ufHo())
+  d_equalityEngine->addFunctionKind(
+      kind::APPLY_UF, false, getLogicInfo().isHigherOrder());
+  if (getLogicInfo().isHigherOrder())
   {
     d_equalityEngine->addFunctionKind(kind::HO_APPLY);
     d_ho.reset(new HoExtension(d_state, d_im));
@@ -146,7 +148,7 @@ void TheoryUF::postCheck(Effort level)
   // check with the higher-order extension at full effort
   if (!d_state.isInConflict() && fullEffort(level))
   {
-    if (options::ufHo())
+    if (getLogicInfo().isHigherOrder())
     {
       d_ho->check();
     }
@@ -169,7 +171,7 @@ void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
   {
     case kind::EQUAL:
     {
-      if (options::ufHo() && options::ufHoExt())
+      if (getLogicInfo().isHigherOrder() && options::ufHoExt())
       {
         if (!pol && !d_state.isInConflict() && atom[0].getType().isFunction())
         {
@@ -212,7 +214,8 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
   Kind k = node.getKind();
   if (k == kind::HO_APPLY)
   {
-    if( !options::ufHo() ){
+    if (!getLogicInfo().isHigherOrder())
+    {
       std::stringstream ss;
       ss << "Partial function applications are only supported with "
             "higher-order logic. Try adding the logic prefix HO_.";
@@ -230,7 +233,8 @@ 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()) && !options::ufHo())
+    if (isHigherOrderType(node.getOperator().getType())
+        && !getLogicInfo().isHigherOrder())
     {
       std::stringstream ss;
       ss << "UF received an application whose operator has higher-order type "
@@ -252,8 +256,8 @@ void TheoryUF::preRegisterTerm(TNode node)
   }
 
   // we always use APPLY_UF if not higher-order, HO_APPLY if higher-order
-  //Assert( node.getKind()!=kind::APPLY_UF || !options::ufHo() );
-  Assert(node.getKind() != kind::HO_APPLY || options::ufHo());
+  Assert(node.getKind() != kind::HO_APPLY
+         || getLogicInfo().isHigherOrder());
 
   Kind k = node.getKind();
   switch (k)
@@ -314,7 +318,8 @@ TrustNode TheoryUF::explain(TNode literal) { return d_im.explainLit(literal); }
 
 bool TheoryUF::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
 {
-  if( options::ufHo() ){
+  if (getLogicInfo().isHigherOrder())
+  {
     // must add extensionality disequalities for all pairs of (non-disequal)
     // function equivalence classes.
     if (!d_ho->collectModelInfoHo(m, termSet))