diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-09-13 16:08:01 -0500 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2017-09-13 14:08:01 -0700 |
| commit | 85a1160aa4cced39808e3e73ceff0e0b5ddc6f66 (patch) | |
| tree | a1e4dfc3fe59f5af0bf5e6bff581f61fcbe9e2e4 /.travis.yml | |
| parent | 3a00b0c4586ef61c93b7b7320cce4d720014f2bf (diff) | |
Modify equality engine to allow operators to be marked as external terms (#1082)
This is required for reasoning higher-order, since we may have equalities between functions, which are operators of APPLY_UF terms.
This commit gets around the previous 1% slowdown by modifying the changes to the equality engine to be minimal impact. Previously the "isInternal" flag could be reset to false after a term is marked as internal=true. This provides an interface for whether operators of a kind should be marked as internal=false from the start. When using higher-order, APPLY_UF operators will be marked as being external when the higher-order option ufHo is set to true.
This has <.001% impact on performance on QF smtlib : https://www.starexec.org/starexec/secure/details/job.jsp?id=24445
Diffstat (limited to '.travis.yml')
0 files changed, 0 insertions, 0 deletions