diff options
| author | Martin <martin.brain@cs.ox.ac.uk> | 2018-05-15 00:18:31 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-15 00:18:31 +0100 |
| commit | 4e96b1d5e01260acc79bdbb86322e23c7cf9567f (patch) | |
| tree | 283fa5091023234bbc601b87d62e4610c05a4981 /src/printer | |
| parent | 0c6681152ca422f7ace1bd1d3c3dac7823de2c14 (diff) | |
Floating point theory solver based on SymFPU (#1895)
* Add some symfpu accessor functions to reduce the size of the literal 'back-end'.
* Enable the bit-vector theory when setting the logic, not in expandDefinition.
This is needed because it is possible to add variables of float or rounding mode
sort but not use any theory specific functions or predicates and thus not enable
the bit-vector theory.
* Use symfpu to implement the literal floating-point objects.
* Add kinds for bit-blasted components.
* Print the new kinds.
* Typing rules for the new kinds.
* Constant folding for the component kinds.
* Add support for components to the theory solver.
* Add explicit equivalences between classification functions and equalities.
* Use symfpu to do symbolic conversions of floating-point operations.
* Implement conversions via (over-)approximation and refinement.
* Correct a copy and paste error in the generation of uninterpretted functions for conversions.
Diffstat (limited to 'src/printer')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index af51ccd45..73357bdef 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -636,6 +636,13 @@ void Smt2Printer::toStream(std::ostream& out, case kind::FLOATINGPOINT_ISNEG: case kind::FLOATINGPOINT_ISPOS: case kind::FLOATINGPOINT_TO_REAL: + case kind::FLOATINGPOINT_COMPONENT_NAN: + case kind::FLOATINGPOINT_COMPONENT_INF: + case kind::FLOATINGPOINT_COMPONENT_ZERO: + case kind::FLOATINGPOINT_COMPONENT_SIGN: + case kind::FLOATINGPOINT_COMPONENT_EXPONENT: + case kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND: + case kind::ROUNDINGMODE_BITBLAST: out << smtKindString(k, d_variant) << ' '; break; @@ -1055,6 +1062,15 @@ static string smtKindString(Kind k, Variant v) case kind::FLOATINGPOINT_TO_REAL: return "fp.to_real"; case kind::FLOATINGPOINT_TO_REAL_TOTAL: return "fp.to_real_total"; + case kind::FLOATINGPOINT_COMPONENT_NAN: return "NAN"; + case kind::FLOATINGPOINT_COMPONENT_INF: return "INF"; + case kind::FLOATINGPOINT_COMPONENT_ZERO: return "ZERO"; + case kind::FLOATINGPOINT_COMPONENT_SIGN: return "SIGN"; + case kind::FLOATINGPOINT_COMPONENT_EXPONENT: return "EXPONENT"; + case kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND: return "SIGNIFICAND"; + case kind::ROUNDINGMODE_BITBLAST: + return "RMBITBLAST"; + //string theory case kind::STRING_CONCAT: return "str.++"; case kind::STRING_LENGTH: return v == z3str_variant ? "Length" : "str.len"; |