diff options
| author | Martin <martin.brain@cs.ox.ac.uk> | 2017-10-03 01:41:24 +0100 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2017-10-02 17:41:24 -0700 |
| commit | 6861f66d2e2b54fc31d9151b4dbeb2964ea07f94 (patch) | |
| tree | 4b4e5fe368f5531f0b43045ac339c4b94124c7b1 /src/theory/fp/kinds | |
| parent | fad765a539f8732461340980477ffe3f8c672fb2 (diff) | |
Add 5 FP kinds for partial to total fn conversion (#1128)
- Add new kinds for partially defined functions
- Print the new kinds
- Type rules for the new total kinds
- Constant folding and rewrites for the new total kinds
Diffstat (limited to 'src/theory/fp/kinds')
| -rw-r--r-- | src/theory/fp/kinds | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds index 61a291b53..144e5736f 100644 --- a/src/theory/fp/kinds +++ b/src/theory/fp/kinds @@ -110,6 +110,12 @@ typerule FLOATINGPOINT_MIN ::CVC4::theory::fp::FloatingPointOperationTypeRule operator FLOATINGPOINT_MAX 2 "floating-point maximum" typerule FLOATINGPOINT_MAX ::CVC4::theory::fp::FloatingPointOperationTypeRule +operator FLOATINGPOINT_MIN_TOTAL 3 "floating-point minimum (defined for all inputs)" +typerule FLOATINGPOINT_MIN_TOTAL ::CVC4::theory::fp::FloatingPointPartialOperationTypeRule + +operator FLOATINGPOINT_MAX_TOTAL 3 "floating-point maximum (defined for all inputs)" +typerule FLOATINGPOINT_MAX_TOTAL ::CVC4::theory::fp::FloatingPointPartialOperationTypeRule + operator FLOATINGPOINT_LEQ 2: "floating-point less than or equal" typerule FLOATINGPOINT_LEQ ::CVC4::theory::fp::FloatingPointTestTypeRule @@ -236,6 +242,17 @@ parameterized FLOATINGPOINT_TO_UBV FLOATINGPOINT_TO_UBV_OP 2 "convert a floating typerule FLOATINGPOINT_TO_UBV ::CVC4::theory::fp::FloatingPointToUBVTypeRule +constant FLOATINGPOINT_TO_UBV_TOTAL_OP \ + ::CVC4::FloatingPointToUBVTotal \ + "::CVC4::FloatingPointToBVHashFunction<0x4>" \ + "util/floatingpoint.h" \ + "operator for to_ubv_total" +typerule FLOATINGPOINT_TO_UBV_TOTAL_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule + +parameterized FLOATINGPOINT_TO_UBV_TOTAL FLOATINGPOINT_TO_UBV_TOTAL_OP 3 "convert a floating-point value to an unsigned bit vector (defined for all inputs)" +typerule FLOATINGPOINT_TO_UBV_TOTAL ::CVC4::theory::fp::FloatingPointToUBVTotalTypeRule + + constant FLOATINGPOINT_TO_SBV_OP \ ::CVC4::FloatingPointToSBV \ @@ -248,8 +265,22 @@ parameterized FLOATINGPOINT_TO_SBV FLOATINGPOINT_TO_SBV_OP 2 "convert a floating typerule FLOATINGPOINT_TO_SBV ::CVC4::theory::fp::FloatingPointToSBVTypeRule +constant FLOATINGPOINT_TO_SBV_TOTAL_OP \ + ::CVC4::FloatingPointToSBVTotal \ + "::CVC4::FloatingPointToBVHashFunction<0x8>" \ + "util/floatingpoint.h" \ + "operator for to_sbv_total" +typerule FLOATINGPOINT_TO_SBV_TOTAL_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule + +parameterized FLOATINGPOINT_TO_SBV_TOTAL FLOATINGPOINT_TO_SBV_TOTAL_OP 3 "convert a floating-point value to a signed bit vector (defined for all inputs)" +typerule FLOATINGPOINT_TO_SBV_TOTAL ::CVC4::theory::fp::FloatingPointToSBVTotalTypeRule + + operator FLOATINGPOINT_TO_REAL 1 "floating-point to real" typerule FLOATINGPOINT_TO_REAL ::CVC4::theory::fp::FloatingPointToRealTypeRule +operator FLOATINGPOINT_TO_REAL_TOTAL 2 "floating-point to real (defined for all inputs)" +typerule FLOATINGPOINT_TO_REAL_TOTAL ::CVC4::theory::fp::FloatingPointToRealTotalTypeRule + endtheory |