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 /src/parser/smt2/Smt2.g | |
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 'src/parser/smt2/Smt2.g')
-rw-r--r-- | src/parser/smt2/Smt2.g | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 5afb2c316..d6b5af324 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2310,8 +2310,10 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] // valid GMP rational string expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); if(expr.getType().isInteger()) { - //must cast to Real to ensure correct type is passed to parametric type constructors - expr = MK_EXPR(kind::TO_REAL, expr); + // Must cast to Real to ensure correct type is passed to parametric type constructors. + // We do this cast using division with 1. + // This has the advantage wrt using TO_REAL since (constant) division is always included in the theory. + expr = MK_EXPR(kind::DIVISION, expr, MK_CONST(Rational(1))); } } |