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