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/printer | |
| 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/printer')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 2f2a6ff18..ae65311de 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -202,7 +202,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, break; } case kind::CONST_FLOATINGPOINT: - out << n.getConst<FloatingPoint>().getLiteral(); + out << n.getConst<FloatingPoint>(); break; case kind::CONST_ROUNDINGMODE: switch (n.getConst<RoundingMode>()) { |