diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-06-17 10:38:40 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-17 10:38:40 -0300 |
| commit | 5915a62d767dd8a33dd13be7c6545c6553442878 (patch) | |
| tree | e2ac8e63946ad0bade14cfec8c1bd40ca1f38da5 /test/regress/regress0/fp/ext-rew-test.smt2 | |
| parent | 2e4d33f5ec1b097075fe0ad334e4f4f354e30679 (diff) | |
Improve polynomial anyterm grammar (#3566)
This changes the grammar construction in the case of anyterm + polynomial grammar so that the binary predicates EQUAL and LEQ are changed to unary predicates lambda x : ANYTERM. P(x, ZERO) rather than lambda xy. P(ANYTERM, ANYTERM), in which ZERO is a 0 constant of the respective type. Currently integer and bit-vectors are supported for this transformation.
This avoid enumerating spurious terms and can lead to significant improvements in enumeration (although not necessarily in solving speed given the current unstable nature of ANYTERM usage).
Diffstat (limited to 'test/regress/regress0/fp/ext-rew-test.smt2')
0 files changed, 0 insertions, 0 deletions