diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-12 08:35:03 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-12 08:50:58 -0500 |
| commit | 360d6ee8d3cdd5ddb47c328043eaed3a107b8db1 (patch) | |
| tree | 9e1fb4d128a62ca3e9152530dbfadb448ed49a45 /src/theory/arith/kinds | |
| parent | d6d34604fa6d4c260edfc10a5b7f543540be75f4 (diff) | |
Make type rules more strict for operators whose type rules involve subtypes. Disable support for subrange and predicate subtypes (which were only partially supported previously).
Diffstat (limited to 'src/theory/arith/kinds')
| -rw-r--r-- | src/theory/arith/kinds | 16 |
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" |