diff options
| author | Martin <martin.brain@diffblue.com> | 2017-09-15 04:04:20 +0100 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2017-09-14 20:04:20 -0700 |
| commit | 190e5aa70862f40ba96b7dc7add3f11a8143c66f (patch) | |
| tree | f039ee87fa11000355da09e9fd156452e8eecdb9 /src/theory/fp/kinds | |
| parent | e27d7b41dba65c1611bfb536ffe958fa7cad3848 (diff) | |
Make floating-point comparison operators chainable (#1101)
Floating-point comparison operators are chainable according to the standard.
Diffstat (limited to 'src/theory/fp/kinds')
| -rw-r--r-- | src/theory/fp/kinds | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds index 983d5aa5c..a1b28d885 100644 --- a/src/theory/fp/kinds +++ b/src/theory/fp/kinds @@ -94,16 +94,16 @@ operator FLOATINGPOINT_MAX 2 "floating-point maximum" typerule FLOATINGPOINT_MAX ::CVC4::theory::fp::FloatingPointOperationTypeRule -operator FLOATINGPOINT_LEQ 2 "floating-point less than or equal" +operator FLOATINGPOINT_LEQ 2: "floating-point less than or equal" typerule FLOATINGPOINT_LEQ ::CVC4::theory::fp::FloatingPointTestTypeRule -operator FLOATINGPOINT_LT 2 "floating-point less than" +operator FLOATINGPOINT_LT 2: "floating-point less than" typerule FLOATINGPOINT_LT ::CVC4::theory::fp::FloatingPointTestTypeRule -operator FLOATINGPOINT_GEQ 2 "floating-point greater than or equal" +operator FLOATINGPOINT_GEQ 2: "floating-point greater than or equal" typerule FLOATINGPOINT_GEQ ::CVC4::theory::fp::FloatingPointTestTypeRule -operator FLOATINGPOINT_GT 2 "floating-point greater than" +operator FLOATINGPOINT_GT 2: "floating-point greater than" typerule FLOATINGPOINT_GT ::CVC4::theory::fp::FloatingPointTestTypeRule |