Remove `--uf-ho` option (#7463)

This option was previously a way of knowing whether higher-order was enabled, which now should be queried via LogicInfo::isHigherOrder.

It also adds an optimization to hasFreeVar required for QCF to be robust and not take a performance hit due to HO operators.

diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 2220caff916ed01f6427744db54a1a246e6b9873..13265db7108b4c297a3d45c16154e3ef2e11fcdf 100644 (file)
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -283,6 +283,11 @@ bool hasBoundVar(TNode n)
 
 bool hasFreeVar(TNode n)
 {
+  // optimization for variables and constants
+  if (n.getNumChildren() == 0)
+  {
+    return n.getKind() == kind::BOUND_VARIABLE;
+  }
   std::unordered_set<Node> fvs;
   return getFreeVariables(n, fvs, false);
 }

diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml
index 239628e283f5c391419cd889099323885a847ca2..7392dd50c799f85679d6d30d0d18a10b92fe0ce9 100644 (file)
--- a/src/options/uf_options.toml
+++ b/src/options/uf_options.toml
@@ -52,14 +52,6 @@ name   = "Uninterpreted Functions Theory"
   default    = "false"
   help       = "group monotone sorts when enforcing fairness for finite model finding"
 
-[[option]]
-  name       = "ufHo"
-  category   = "regular"
-  long       = "uf-ho"
-  type       = "bool"
-  default    = "false"
-  help       = "enable support for higher-order reasoning"
-
 [[option]]
   name       = "ufHoExt"
   category   = "regular"

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index f6a65f90a1ea7f494e9b487f2d74c499366d6427..6515ef90a70cf0e82aab715d934e4109cb6cd47f 100644 (file)
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -657,7 +657,7 @@ Node BVToInt::translateWithChildren(Node original,
        * of the bounds that were relevant for the original
        * bit-vectors.
        */
-      if (childrenTypesChanged(original) && options().uf.ufHo)
+      if (childrenTypesChanged(original) && logicInfo().isHigherOrder())
       {
         throw TypeCheckingExceptionPrivate(
             original,

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index b08e6f298f8ca279b21e56d583cafcc71b687f09..67e83bcd1864193d38cac8f29e6b03164a5edfdb 100644 (file)
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -311,7 +311,7 @@ bool ProcessAssertions::apply(Assertions& as)
   }
   dumpAssertions("post-repeat-simplify", as);
 
-  if (options().uf.ufHo)
+  if (logicInfo().isHigherOrder())
   {
     d_passes["ho-elim"]->apply(&assertions);
   }

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 31ccaacacab166ae6c952d437172cdbd29a92f69..6fdd45c4e7a336e37b8bcaf6eed4803a6d4aca17 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -692,7 +692,6 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
 
   if (logic.isHigherOrder())
   {
-    opts.uf.ufHo = true;
     if (!opts.theory.assignFunctionValues)
     {
       // must assign function values

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 3233988796ca0ea1c2ed433aa343a26db011ea43..f045144800faad2bd3f1290a0fe27882dde30878 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -995,8 +995,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
     Assert(qi->d_var_num.find(n) != qi->d_var_num.end());
     // rare case where we have a free variable in an operator, we are invalid
     if (n.getKind() == ITE
-        || (options::ufHo() && n.getKind() == APPLY_UF
-            && expr::hasFreeVar(n.getOperator())))
+        || (n.getKind() == APPLY_UF && expr::hasFreeVar(n.getOperator())))
     {
       d_type = typ_invalid;
     }else{

diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp
index 27b61e87d09fe7145c45d65632d317d9b5399aae..06750c7edbc2594af307fecac48257951abc0747 100644 (file)
--- a/src/theory/uf/eq_proof.cpp
+++ b/src/theory/uf/eq_proof.cpp
@@ -703,8 +703,10 @@ void EqProof::reduceNestedCongruence(
         << transitivityMatrix[i].back() << "\n";
     // if i == 0, first child must be REFL step, standing for (= f f), which can
     // be ignored in a first-order calculus
-    Assert(i > 0 || d_children[0]->d_id == MERGED_THROUGH_REFLEXIVITY
-           || options::ufHo());
+    // Notice if higher-order is disabled, the following holds:
+    //   i > 0 || d_children[0]->d_id == MERGED_THROUGH_REFLEXIVITY
+    // We don't have access to whether we are higher-order in this context,
+    // so the above cannot be an assertion.
     // recurse
     if (i > 1)
     {

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 498fe765e785a625c0b21284549238b37c8a1861..1e240a254a4dc0fd54222dbe5f3604e68acdd591 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -171,7 +171,7 @@ void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
   {
     case kind::EQUAL:
     {
-      if (logicInfo().isHigherOrder() && options::ufHoExt())
+      if (logicInfo().isHigherOrder() && options().uf.ufHoExt)
       {
         if (!pol && !d_state.isInConflict() && atom[0].getType().isFunction())
         {