diff options
| author | Martin <martin.brain@diffblue.com> | 2017-09-19 01:14:05 +0100 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2017-09-18 17:14:05 -0700 |
| commit | 61a846a4998be697867292924454893271eb6496 (patch) | |
| tree | 7d1c5a5cadb8a5c538efea00abdd82b5681b809a /src/parser/smt2/Smt2.g | |
| parent | 053003a64bde91aa32f688d248d83c3d4f271250 (diff) | |
Floating point symfpu support (#1103)
- Update the parser to the new constant construction
- Fix the problem with parsing +/-zero and remove some dead code
- Extend the interface for literal floating-point values.
- Add a constructor so that a parameteric operator structure can be created from a type
- Add constructors so parametric operator constants can be easily converted
- Update SMT2 printing so that it uses the informative output
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 46 |
1 files changed, 17 insertions, 29 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 92f6b36d8..2aa85fbe3 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2271,17 +2271,25 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] } } | FP_PINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb), - +INFINITY)); } + { expr = MK_CONST(FloatingPoint::makeInf(FloatingPointSize(AntlrInput::tokenToUnsigned($eb), + AntlrInput::tokenToUnsigned($sb)), + false)); } | FP_NINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb), - -INFINITY)); } + { expr = MK_CONST(FloatingPoint::makeInf(FloatingPointSize(AntlrInput::tokenToUnsigned($eb), + AntlrInput::tokenToUnsigned($sb)), + true)); } | FP_NAN_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb), - NAN)); } + { expr = MK_CONST(FloatingPoint::makeNaN(FloatingPointSize(AntlrInput::tokenToUnsigned($eb), + AntlrInput::tokenToUnsigned($sb)))); } + + | FP_PZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL + { expr = MK_CONST(FloatingPoint::makeZero(FloatingPointSize(AntlrInput::tokenToUnsigned($eb), + AntlrInput::tokenToUnsigned($sb)), + false)); } + | FP_NZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL + { expr = MK_CONST(FloatingPoint::makeZero(FloatingPointSize(AntlrInput::tokenToUnsigned($eb), + AntlrInput::tokenToUnsigned($sb)), + true)); } // NOTE: Theory parametric constants go here ) @@ -2505,26 +2513,6 @@ indexedFunctionName[CVC4::Expr& op, CVC4::Kind& kind] "bv2nat and int2bv are not part of SMT-LIB, and aren't available " "in SMT-LIB strict compliance mode"); } } - | FP_PINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb), - +INFINITY)); } - | FP_NINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb), - -INFINITY)); } - | FP_NAN_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb), - NAN)); } - | FP_PZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb), - +0.0)); } - | FP_NZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb), - -0.0)); } | FP_TO_FP_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL { op = MK_CONST(FloatingPointToFPGeneric( AntlrInput::tokenToUnsigned($eb), |