diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-22 16:25:37 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-22 21:25:37 +0000 |
| commit | c4ebca0e668e83f330cbb777a90c6b02b1c47eb9 (patch) | |
| tree | b53b2319fd8e2b39256bc53b8039848fcbd93f0f /src/theory/quantifiers/quant_conflict_find.cpp | |
| parent | bdc1671342704ffa8113cbb6f3b5f07af25d564b (diff) | |
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.
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.cpp')
| -rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 3 |
1 files changed, 1 insertions, 2 deletions
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{ |