From c4ebca0e668e83f330cbb777a90c6b02b1c47eb9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 22 Oct 2021 16:25:37 -0500 Subject: [PATCH] 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. --- src/expr/node_algorithm.cpp | 5 +++++ src/options/uf_options.toml | 8 -------- src/preprocessing/passes/bv_to_int.cpp | 2 +- src/smt/process_assertions.cpp | 2 +- src/smt/set_defaults.cpp | 1 - src/theory/quantifiers/quant_conflict_find.cpp | 3 +-- src/theory/uf/eq_proof.cpp | 6 ++++-- src/theory/uf/theory_uf.cpp | 2 +- 8 files changed, 13 insertions(+), 16 deletions(-) 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 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()) { -- 2.30.2