From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 22 Oct 2021 21:25:37 +0000 (-0500)
Subject: Remove `--uf-ho` option (#7463)
X-Git-Tag: cvc5-1.0.0~999
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c4ebca0e668e83f330cbb777a90c6b02b1c47eb9;p=cvc5.git

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 2220caff9..13265db71 100644
--- 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 239628e28..7392dd50c 100644
--- 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 f6a65f90a..6515ef90a 100644
--- 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 b08e6f298..67e83bcd1 100644
--- 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 31ccaacac..6fdd45c4e 100644
--- 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 323398879..f04514480 100644
--- 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 27b61e87d..06750c7ed 100644
--- 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 498fe765e..1e240a254 100644
--- 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())
         {