projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 30673d6) | patch
Do not parse ->/lambda unless --uf-ho enabled (#4544)
authorAndres Noetzli <andres.noetzli@gmail.com>
Mon, 1 Jun 2020 16:41:16 +0000 (09:41 -0700)
committerGitHub <noreply@github.com>
Mon, 1 Jun 2020 16:41:16 +0000 (11:41 -0500)
commit7c2045123b177334cc47b24266225d6b38599bf5
tree2509c9b0ce6a527cb04d52cb9d585eb0058015d6tree
parent30673d6ce9a5a1444b33fb11367914df0399e824commit | diff
Do not parse ->/lambda unless --uf-ho enabled (#4544)

Fixes #4477. Logic ALL includes higher-order but we currently do not
support solving higher-order problems unless --uf-ho is enabled. This
commit changes the condition under which we parse -> and lambda to
only enabled parsing of those symbols if the logic allows higher-order
constraints and --uf-ho is enabled.
src/parser/smt2/Smt2.g diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/parser/smt2/smt2.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/ho/issue4477.smt2 [new file with mode: 0644] blob