diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-09-14 14:12:22 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-09-14 14:12:22 -0500 |
| commit | ab2924e8a6cc34f29167b1ff50273d59dd7a6707 (patch) | |
| tree | d9902a389ae70a21f2d5a3f7acde2ce658fb534d /src/parser/smt2/Smt2.g | |
| parent | e4fc6c7b57668f18ce087c45e001c101375c20ea (diff) | |
Remove unhandled subtypes (#1098)
* Remove unhandled subtypes, which consequently makes typing rules uniformly stricter based on weakening the subtype relation. Ensure coercions in the smt2 and cvc parser for Real decimal constants whose type is Integer. Ensure type annotations are computed during preRewrite to ensure rewriting (which does not preserve types) does not impact term construction for parametric datatypes. This fixes issue #1048 (we now give an type exception).
* Update unit test for parametric datatypes to reflect new subtyping relation.
* Remove deprecated test.
* Make array construction for lambdas work with new subtype relations to handle lambdas like (lambda ((x Int) (y Int)) (ite (= x 0) 0.5 0.0)).
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 86c0b3126..92f6b36d8 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2254,7 +2254,12 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | DECIMAL_LITERAL { // FIXME: This doesn't work because an SMT rational is not a // valid GMP rational string - expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); } + 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); + } + } | LPAREN_TOK INDEX_TOK ( bvLit=SIMPLE_SYMBOL size=INTEGER_LITERAL |