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/builtin/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/builtin/kinds')
| -rw-r--r-- | src/theory/builtin/kinds | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 0ebebf1dd..12e897189 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -336,17 +336,4 @@ typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule -constant SUBTYPE_TYPE \ - ::CVC4::Predicate \ - ::CVC4::PredicateHashFunction \ - "expr/predicate.h" \ - "predicate subtype; payload is an instance of the CVC4::Predicate class" -cardinality SUBTYPE_TYPE \ - "::CVC4::theory::builtin::SubtypeProperties::computeCardinality(%TYPE%)" \ - "theory/builtin/theory_builtin_type_rules.h" -well-founded SUBTYPE_TYPE \ - "::CVC4::theory::builtin::SubtypeProperties::isWellFounded(%TYPE%)" \ - "::CVC4::theory::builtin::SubtypeProperties::mkGroundTerm(%TYPE%)" \ - "theory/builtin/theory_builtin_type_rules.h" - endtheory |