diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-21 17:52:26 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-21 15:52:26 -0700 |
| commit | e50e09efa679c2d0c835cbf794a7b0743347552a (patch) | |
| tree | 43b362a297ba4b460e38d38a3dca5ad6f5c582fc /test | |
| parent | 4e56fd1578c51544d879cf84a4ea48c5f09a1d97 (diff) | |
Improvements in parsing and printing related to mixed int/real (#1879)
This eliminates some hacks for dealing with Int/Real.
- Eliminates the use of "to_real" to cast decimals like "2.0" that happen to be Int. We now replace these by (/ 2 1) instead of (to_real 2), which has the advantage of being smt-lib compliant for all theories, including QF_LRA.
- Eliminates the use of a hack to use "type ascriptions" when returning values from a get-value command. Instead, we use division with 1 when necessary. This affects the output of a few regressions, but we remain smt-lib compliant.
- Addresses a bug with printing arbitrary type ascriptions for smt2 terms. This partially addresses #1852.
- Updates our printing of negative rationals to be (/ (- n) m) instead of (- (/ n m)), which is consistent with the smt lib standard for real values (http://smtlib.cs.uiowa.edu/theories-Reals.shtml).
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/get-value-reals-ints.smt2 | 4 | ||||
| -rw-r--r-- | test/regress/regress0/get-value-reals.smt2 | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/test/regress/regress0/get-value-reals-ints.smt2 b/test/regress/regress0/get-value-reals-ints.smt2 index 53337c5d3..8dec35073 100644 --- a/test/regress/regress0/get-value-reals-ints.smt2 +++ b/test/regress/regress0/get-value-reals-ints.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: ; EXPECT: sat -; EXPECT: ((pos_int 5) (pos_real_int_value 3.0) (pos_rat (/ 1 3)) (zero 0.0) (neg_rat (- (/ 2 3))) (neg_real_int_value (- 2.0)) (neg_int (- 6))) +; EXPECT: ((pos_int 5) (pos_real_int_value (/ 3 1)) (pos_rat (/ 1 3)) (zero (/ 0 1)) (neg_rat (/ (- 2) 3)) (neg_real_int_value (/ (- 2) 1)) (neg_int (- 6))) (set-info :smt-lib-version 2.0) (set-option :produce-models true) (set-logic QF_LIRA) @@ -24,4 +24,4 @@ (assert (= neg_int (- 6))) (check-sat) -(get-value (pos_int pos_real_int_value pos_rat zero neg_rat neg_real_int_value neg_int))
\ No newline at end of file +(get-value (pos_int pos_real_int_value pos_rat zero neg_rat neg_real_int_value neg_int)) diff --git a/test/regress/regress0/get-value-reals.smt2 b/test/regress/regress0/get-value-reals.smt2 index 487670158..6fa542668 100644 --- a/test/regress/regress0/get-value-reals.smt2 +++ b/test/regress/regress0/get-value-reals.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: ; EXPECT: sat -; EXPECT: ((pos_int 3.0) (pos_rat (/ 1 3)) (zero 0.0) (neg_rat (- (/ 2 3))) (neg_int (- 2.0))) +; EXPECT: ((pos_int (/ 3 1)) (pos_rat (/ 1 3)) (zero (/ 0 1)) (neg_rat (/ (- 2) 3)) (neg_int (/ (- 2) 1))) (set-info :smt-lib-version 2.0) (set-option :produce-models true) (set-logic QF_LRA) @@ -19,4 +19,4 @@ (assert (= neg_int (- 2))) (check-sat) -(get-value (pos_int pos_rat zero neg_rat neg_int))
\ No newline at end of file +(get-value (pos_int pos_rat zero neg_rat neg_int)) |