projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bdc1671) | patch
Remove `--uf-ho` option (#7463)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 22 Oct 2021 21:25:37 +0000 (16:25 -0500)
committerGitHub <noreply@github.com>
Fri, 22 Oct 2021 21:25:37 +0000 (21:25 +0000)
commitc4ebca0e668e83f330cbb777a90c6b02b1c47eb9
treeb53b2319fd8e2b39256bc53b8039848fcbd93f0ftree
parentbdc1671342704ffa8113cbb6f3b5f07af25d564bcommit | 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.
src/expr/node_algorithm.cpp diff | blob | history
src/options/uf_options.toml diff | blob | history
src/preprocessing/passes/bv_to_int.cpp diff | blob | history
src/smt/process_assertions.cpp diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/theory/quantifiers/quant_conflict_find.cpp diff | blob | history
src/theory/uf/eq_proof.cpp diff | blob | history
src/theory/uf/theory_uf.cpp diff | blob | history