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/theory/fp/kinds | |
| 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/theory/fp/kinds')
| -rw-r--r-- | src/theory/fp/kinds | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds index 966ed4d71..b1170b42c 100644 --- a/src/theory/fp/kinds +++ b/src/theory/fp/kinds @@ -283,4 +283,28 @@ operator FLOATINGPOINT_TO_REAL_TOTAL 2 "floating-point to real (defined for all typerule FLOATINGPOINT_TO_REAL_TOTAL ::CVC4::theory::fp::FloatingPointToRealTotalTypeRule + +operator FLOATINGPOINT_COMPONENT_NAN 1 "NaN component of a word-blasted floating-point number" +typerule FLOATINGPOINT_COMPONENT_NAN ::CVC4::theory::fp::FloatingPointComponentBit + +operator FLOATINGPOINT_COMPONENT_INF 1 "Inf component of a word-blasted floating-point number" +typerule FLOATINGPOINT_COMPONENT_INF ::CVC4::theory::fp::FloatingPointComponentBit + +operator FLOATINGPOINT_COMPONENT_ZERO 1 "Zero component of a word-blasted floating-point number" +typerule FLOATINGPOINT_COMPONENT_ZERO ::CVC4::theory::fp::FloatingPointComponentBit + +operator FLOATINGPOINT_COMPONENT_SIGN 1 "Sign component of a word-blasted floating-point number" +typerule FLOATINGPOINT_COMPONENT_SIGN ::CVC4::theory::fp::FloatingPointComponentBit + +operator FLOATINGPOINT_COMPONENT_EXPONENT 1 "Exponent component of a word-blasted floating-point number" +typerule FLOATINGPOINT_COMPONENT_EXPONENT ::CVC4::theory::fp::FloatingPointComponentExponent + +operator FLOATINGPOINT_COMPONENT_SIGNIFICAND 1 "Significand component of a word-blasted floating-point number" +typerule FLOATINGPOINT_COMPONENT_SIGNIFICAND ::CVC4::theory::fp::FloatingPointComponentSignificand + + +operator ROUNDINGMODE_BITBLAST 1 "The bit-vector for a non-deterministic rounding mode" +typerule ROUNDINGMODE_BITBLAST ::CVC4::theory::fp::RoundingModeBitBlast + + endtheory |