diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-11-09 18:41:24 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-11-09 18:41:24 +0000 |
| commit | 63e4a6775daa1b7a986cc9dec0bd178b7e023c47 (patch) | |
| tree | 21022ef535c947c074060d11a0ea1ef8dd4c4b45 /src/cvc4.i | |
| parent | d11716a24a2b70b7c3681e52de51bd622c4f6447 (diff) | |
In non-linear logics, rewrite DIVISION, INTS_DIVISION, and INTS_MODULUS into ITEs of the form:
IF (denom = 0) THEN divByZero(num) ELSE (DIVISION_TOTAL num denom) ENDIF
where divByZero is an uninterpreted function symbol (there's one for each of the partial operators).
In linear logics, don't do any of this.
Bitvector partial functions to come, if this is successful for Tim.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/cvc4.i')
0 files changed, 0 insertions, 0 deletions