1# kinds -*- sh -*- 2# 3# For documentation on this file format, please refer to 4# src/theory/builtin/kinds. 5# 6 7theory THEORY_DATATYPES ::CVC4::theory::datatypes::TheoryDatatypes "theory/datatypes/theory_datatypes.h" 8typechecker "theory/datatypes/theory_datatypes_type_rules.h" 9 10properties check presolve parametric propagate 11 12rewriter ::CVC4::theory::datatypes::DatatypesRewriter "theory/datatypes/datatypes_rewriter.h" 13 14# constructor type has a list of selector types followed by a return type 15operator CONSTRUCTOR_TYPE 1: "constructor" 16cardinality CONSTRUCTOR_TYPE \ 17 "::CVC4::theory::datatypes::ConstructorProperties::computeCardinality(%TYPE%)" \ 18 "theory/datatypes/theory_datatypes_type_rules.h" 19 20# selector type has domain type and a range type 21operator SELECTOR_TYPE 2 "selector" 22# can re-use function cardinality 23cardinality SELECTOR_TYPE \ 24 "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \ 25 "theory/builtin/theory_builtin_type_rules.h" 26 27# tester type has a constructor type 28operator TESTER_TYPE 1 "tester" 29# can re-use function cardinality 30cardinality TESTER_TYPE \ 31 "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \ 32 "theory/builtin/theory_builtin_type_rules.h" 33 34parameterized APPLY_CONSTRUCTOR APPLY_TYPE_ASCRIPTION 0: "constructor application; first parameter is the constructor, remaining parameters (if any) are parameters to the constructor" 35 36parameterized APPLY_SELECTOR SELECTOR_TYPE 1 "selector application; parameter is a datatype term (undefined if mis-applied)" 37parameterized APPLY_SELECTOR_TOTAL [SELECTOR_TYPE] 1 "selector application; parameter is a datatype term (defined rigidly if mis-applied)" 38 39parameterized APPLY_TESTER TESTER_TYPE 1 "tester application; first parameter is a tester, second is a datatype term" 40 41constant DATATYPE_TYPE \ 42 ::CVC4::DatatypeIndexConstant \ 43 "::CVC4::DatatypeIndexConstantHashFunction" \ 44 "expr/datatype.h" \ 45 "a datatype type index" 46cardinality DATATYPE_TYPE \ 47 "%TYPE%.getDatatype().getCardinality(%TYPE%.toType())" \ 48 "expr/datatype.h" 49well-founded DATATYPE_TYPE \ 50 "%TYPE%.getDatatype().isWellFounded()" \ 51 "%TYPE%.getDatatype().mkGroundTerm(%TYPE%.toType())" \ 52 "expr/datatype.h" 53 54enumerator DATATYPE_TYPE \ 55 "::CVC4::theory::datatypes::DatatypesEnumerator" \ 56 "theory/datatypes/type_enumerator.h" 57 58operator PARAMETRIC_DATATYPE 1: "parametric datatype" 59cardinality PARAMETRIC_DATATYPE \ 60 "DatatypeType(%TYPE%.toType()).getDatatype().getCardinality(%TYPE%.toType())" \ 61 "expr/datatype.h" 62well-founded PARAMETRIC_DATATYPE \ 63 "DatatypeType(%TYPE%.toType()).getDatatype().isWellFounded()" \ 64 "DatatypeType(%TYPE%.toType()).getDatatype().mkGroundTerm(%TYPE%.toType())" \ 65 "expr/datatype.h" 66 67enumerator PARAMETRIC_DATATYPE \ 68 "::CVC4::theory::datatypes::DatatypesEnumerator" \ 69 "theory/datatypes/type_enumerator.h" 70 71parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \ 72 "type ascription, for datatype constructor applications; first parameter is an ASCRIPTION_TYPE, second is the datatype constructor application being ascribed" 73constant ASCRIPTION_TYPE \ 74 ::CVC4::AscriptionType \ 75 ::CVC4::AscriptionTypeHashFunction \ 76 "expr/ascription_type.h" \ 77 "a type parameter for type ascription; payload is an instance of the CVC4::AscriptionType class" 78 79typerule APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule 80typerule APPLY_SELECTOR ::CVC4::theory::datatypes::DatatypeSelectorTypeRule 81typerule APPLY_SELECTOR_TOTAL ::CVC4::theory::datatypes::DatatypeSelectorTypeRule 82typerule APPLY_TESTER ::CVC4::theory::datatypes::DatatypeTesterTypeRule 83typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionTypeRule 84 85# constructor applications are constant if they are applied only to constants 86construle APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule 87 88constant TUPLE_UPDATE_OP \ 89 ::CVC4::TupleUpdate \ 90 ::CVC4::TupleUpdateHashFunction \ 91 "util/tuple.h" \ 92 "operator for a tuple update; payload is an instance of the CVC4::TupleUpdate class" 93parameterized TUPLE_UPDATE TUPLE_UPDATE_OP 2 "tuple update; first parameter is a TUPLE_UPDATE_OP (which references an index), second is the tuple, third is the element to store in the tuple at the given index" 94typerule TUPLE_UPDATE_OP ::CVC4::theory::datatypes::TupleUpdateOpTypeRule 95typerule TUPLE_UPDATE ::CVC4::theory::datatypes::TupleUpdateTypeRule 96 97constant RECORD_UPDATE_OP \ 98 ::CVC4::RecordUpdate \ 99 ::CVC4::RecordUpdateHashFunction \ 100 "expr/record.h" \ 101 "operator for a record update; payload is an instance CVC4::RecordUpdate class" 102parameterized RECORD_UPDATE RECORD_UPDATE_OP 2 "record update; first parameter is a RECORD_UPDATE_OP (which references a field), second is a record term to update, third is the element to store in the record in the given field" 103typerule RECORD_UPDATE_OP ::CVC4::theory::datatypes::RecordUpdateOpTypeRule 104typerule RECORD_UPDATE ::CVC4::theory::datatypes::RecordUpdateTypeRule 105 106 107operator DT_SIZE 1 "datatypes size" 108typerule DT_SIZE ::CVC4::theory::datatypes::DtSizeTypeRule 109 110operator DT_HEIGHT_BOUND 2 "datatypes height bound" 111typerule DT_HEIGHT_BOUND ::CVC4::theory::datatypes::DtBoundTypeRule 112 113operator DT_SIZE_BOUND 2 "datatypes height bound" 114typerule DT_SIZE_BOUND ::CVC4::theory::datatypes::DtBoundTypeRule 115 116operator DT_SYGUS_BOUND 2 "datatypes sygus bound" 117typerule DT_SYGUS_BOUND ::CVC4::theory::datatypes::DtSygusBoundTypeRule 118 119operator DT_SYGUS_EVAL 1: "datatypes sygus evaluation function" 120typerule DT_SYGUS_EVAL ::CVC4::theory::datatypes::DtSyguEvalTypeRule 121 122endtheory 123