From c4ebca0e668e83f330cbb777a90c6b02b1c47eb9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 22 Oct 2021 16:25:37 -0500 Subject: 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/theory/quantifiers/quant_conflict_find.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'src/theory/quantifiers/quant_conflict_find.cpp') 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{ -- cgit v1.2.3