summaryrefslogtreecommitdiff
path: root/src/theory/arith/kinds
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/kinds')
-rw-r--r--src/theory/arith/kinds16
1 files changed, 0 insertions, 16 deletions
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 0884083c0..34ae30f4c 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -51,19 +51,6 @@ sort INTEGER_TYPE \
"expr/node_manager.h" \
"integer type"
-constant SUBRANGE_TYPE \
- ::CVC4::SubrangeBounds \
- ::CVC4::SubrangeBoundsHashFunction \
- "util/subrange_bound.h" \
- "the type of an integer subrange"
-cardinality SUBRANGE_TYPE \
- "::CVC4::theory::arith::SubrangeProperties::computeCardinality(%TYPE%)" \
- "theory/arith/theory_arith_type_rules.h"
-well-founded SUBRANGE_TYPE \
- true \
- "::CVC4::theory::arith::SubrangeProperties::mkGroundTerm(%TYPE%)" \
- "theory/arith/theory_arith_type_rules.h"
-
constant CONST_RATIONAL \
::CVC4::Rational \
::CVC4::RationalHashFunction \
@@ -76,9 +63,6 @@ enumerator REAL_TYPE \
enumerator INTEGER_TYPE \
"::CVC4::theory::arith::IntegerEnumerator" \
"theory/arith/type_enumerator.h"
-enumerator SUBRANGE_TYPE \
- "::CVC4::theory::arith::SubrangeEnumerator" \
- "theory/arith/type_enumerator.h"
operator LT 2 "less than, x < y"
operator LEQ 2 "less than or equal, x <= y"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback