1 # kinds [for builtin theory] -*- sh -*-
3 # This "kinds" file is written in a domain-specific language for
4 # declaring CVC4 kinds. Comments are marked with #, as this line is.
6 # The first non-blank, non-comment line in this file must be a theory
11 # Thereafter, ID is bound to your theory. It becomes part of an
12 # enumeration that identifies all theories. If your theory has
13 # several, distinct implementations, they still all share a kinds
14 # file, a theory ID, all the defined kinds/operators/types for the
15 # theory, typechecker, etc. They should also share a base class
16 # (that's the T above). The header is the header for this base
19 # The very end of this file should end with:
23 # There are several basic commands:
25 # properties PROPERTIES...
27 # This command declares properties of the theory. It can occur
28 # more than once, in which case the effect is additive.
30 # The current set of properties and their meanings are:
32 # finite the theory is finite
33 # stable-infinite the theory is stably infinite
34 # polite the theory is polite
36 # check the theory supports the check() function
37 # propagate the theory supports propagate() (and explain())
38 # staticLearning the theory supports staticLearning()
39 # notifyRestart the theory supports notifyRestart()
40 # presolve the theory supports presolve()
42 # In the case of the "theory-supports-function" properties, you
43 # need to declare these for your theory or the functions will not
44 # be called! This is used to speed up the core where functionality
49 # This declares a rewriter class T for your theory, declared in
50 # header. Your rewriter class provides four functions:
53 # static void shutdown();
54 # static RewriteResponse preRewrite(TNode node);
55 # static RewriteResponse postRewrite(TNode node);
57 # ...BUT please note that init() and shutdown() may be removed in
58 # future, so if possible, do not rely on them being called (and
59 # implement them as a no-op).
63 # Declare that this theory's typechecker class is defined in the
64 # given header. (#include'd by the TypeChecker class in the expr
67 # variable K ["comment"]
69 # This declares a kind K that has no operator (it's conceptually a
70 # VARIABLE). This is appropriate for things like VARIABLE and
73 # operator K #children ["comment"]
75 # Declares a "built-in" operator kind K. Really this is the same
76 # as "variable" except that it has an operator (automatically
77 # generated by NodeManager).
79 # You can specify an exact # of children required as the second
80 # argument to the operator command. In debug mode, assertions are
81 # automatically included to ensure that no Nodes can ever be
82 # created violating this. (FIXME: the public Expr stuff should
83 # enforce them regardless of whether debugging or not.) For
84 # example, a binary operator could be specified as:
86 # operator LESS_THAN 2 "arithmetic comparison, x < y"
88 # Alternatively, a range can be specified for #children as
89 # "LB:[UB]", LB and UB representing lower and upper bounds on the
90 # number of children (inclusive). If there is no lower bound, put
91 # a "0". If there is no upper bound, leave the colon after LB,
92 # but omit UB. For example, an N-ary operator might be defined
95 # operator PLUS 2: "addition on two or more arguments"
97 # parameterized K #children ["comment"]
99 # Declares a "built-in" parameterized operator kind K. This is a
100 # theory-specific APPLY, e.g., APPLY_UF, which applies its first
101 # parameter (say, "f"), to its operands (say, "x" and "y", making
102 # the full application "f(x,y)"). Nodes with such a kind will
103 # have an operator (Node::hasOperator() returns true, and
104 # Node::getOperator() returns the Node of functional type
105 # representing "f" here), and the "children" are defined to be
106 # this operator's parameters, and don't include the operator
107 # itself (here, there are only two children "x" and "y").
109 # LB and UB are the same as documented for the operator command.
110 # The first parameter (the function being applied) does not count
113 # For consistency these should start with "APPLY_", but this is
116 # constant K T Hasher header ["comment"]
118 # Declares a constant kind K. T is the C++ type representing the
119 # constant internally (and it should be
120 # ::fully::qualified::like::this), and header is the header needed
121 # to define it. Hasher is a hash functor type defined like this:
124 # static size_t hash(const T& val);
127 # For consistency, constants taking a non-void payload should
128 # start with "CONST_", but this is not enforced.
130 # typerule K typechecker-class
132 # Declares that a (previously-declared) kind K is typechecked by
133 # the typechecker-class. This class should be defined by the
134 # header given to the "typechecker" command, above. The
135 # typechecker-class is used this way by the main TypeChecker code:
137 # typechecker-class::computeType(NodeManager* nm, TNode n, bool check)
139 # It returns TypeNode. It should compute the type of n and return it,
140 # and if "check" is true, should actually perform type checking instead
141 # of simply type computation.
143 # sort K cardinality [well-founded ground-term header | not-well-founded] ["comment"]
145 # This creates a kind K that represents a sort (a "type constant").
146 # These kinds of types are "atomic" types; if you need to describe
147 # a complex type that takes type arguments (like arrays), use
148 # "operator"; if you need to describe one that takes "constant"
149 # arguments (like bitvectors), use "constant", and if you invent
150 # one that takes both, you could try "parameterized". In those
151 # cases, you'll want to provide a cardinality separately for your
154 # The cardinality argument is a nonnegative number (if the sort is
155 # finite), or Cardinality::INTEGERS if the sort has the same
156 # cardinality as the integers, or Cardinality::REALS if the sort
157 # has the same cardinality as the reals.
159 # If the sort is well-founded (i.e., there exist ground terms),
160 # then the argument should be the string "well-founded"; if not,
161 # it should be the string "not-well-founded". If well-founded,
162 # two extra arguments immediately follow---a C++ expression that
163 # constructs a ground term (as a Node), and the header that must
164 # be #included for that expression to compile.
166 # For consistency, sorts should end with "_TYPE", but this is not
169 # cardinality K cardinality-computer [header]
171 # This command does not define a kind; the kind K needs to be
172 # defined by one of the other commands above. This command just
173 # provides a cardinality for types of kind K. The
174 # "cardinality-computer" is a C++ expression that will yield a
175 # Cardinality for the type. In that expression, the sequence of
176 # characters "%TYPE%" will be rewritten with a variable containing
177 # a TypeNode of kind K. The optional "header" argument is an
178 # include file necessary to compile the cardinality-computer
181 # If the cardinality need not be computed per-type (i.e., it's the
182 # same for all types of kind K, but the "sort" gesture above could
183 # not be used---in which case it doesn't already have a registered
184 # cardinality), you can simply construct a Cardinality temporary.
187 # cardinality MY_TYPE Cardinality(Cardinality::INTEGERS)
189 # If not, you might opt to use a computer; a common place to put it
190 # is with your type checker:
192 # cardinality MY_TYPE \
193 # ::CVC4::theory::foo::TheoryFoo::CardinalityComputer(%TYPE%) \
194 # "theory/foo/theory_foo_type_rules.h"
196 # well-founded K wellfoundedness-computer ground-term-computer [header]
198 # Analogous to the "cardinality" command above, the well-founded
199 # command provides a well-foundedness computer for the type. A
200 # ground term computer is required unless the
201 # wellfoundedness-computer is the constant "false". The ground
202 # term computer should return a Node, and it should return the
203 # same Node each time for a given type (although usually it's only
204 # ever called once anyway since the result is cached).
207 # Lines may be broken with a backslash between arguments; for example:
209 # constant CONST_INT \
212 # "This is a constant representing an INT.
213 # Its payload is the C++ int type.
214 # It is used by the theory of arithmetic."
216 # As shown in the example, ["comment"] fields may be broken across
217 # multiple lines too.
219 # The expr package guarantees that Nodes built with kinds have the
220 # following constraints imposed on them. (The #children guarantee
221 # only holds when assertions are turned on.)
223 # Node meta-kind has operator? # children
224 # ================== ================= =======================
226 # operator yes as documented above
227 # parameterized yes as documented above
230 # NOTE THAT This file is actually an executable Bourne shell script
231 # (sourced by the processing scripts after defining functions called
232 # "theory," "variable," "operator," "parameterized," and "constant").
233 # Please don't do anything else in this file other than using these
237 theory THEORY_BUILTIN ::CVC4::theory::builtin::TheoryBuiltin "theory/builtin/theory_builtin.h"
238 typechecker "theory/builtin/theory_builtin_type_rules.h"
240 properties stable-infinite
242 # Rewriter responisble for all the terms of the theory
243 rewriter ::CVC4::theory::builtin::TheoryBuiltinRewriter "theory/builtin/theory_builtin_rewriter.h"
245 sort BUILTIN_OPERATOR_TYPE \
246 Cardinality::INTEGERS \
248 "Built in type for built in operators"
250 # Justified because we can have an unbounded-but-finite number of
251 # sorts. Assuming we have |Z| is probably ok for now..
253 Cardinality::INTEGERS \
257 variable SORT_TAG "sort tag"
258 parameterized SORT_TYPE SORT_TAG 0: "sort type"
259 # This is really "unknown" cardinality, but maybe this will be good
260 # enough (for now) ? Once we support quantifiers, maybe reconsider
262 cardinality SORT_TYPE "Cardinality(Cardinality::INTEGERS)"
263 well-founded SORT_TYPE false
266 # A kind representing "inlined" operators defined with OPERATOR
267 # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's
268 # not stored that way. If you ask for the operator of (EQUAL a b),
269 # you'll get a special, singleton (BUILTIN EQUAL) Node.
272 ::CVC4::kind::KindHashStrategy \
274 "The kind of nodes representing built-in operators"
276 variable FUNCTION "function"
277 parameterized APPLY FUNCTION 0: "defined function application"
279 operator EQUAL 2 "equality"
280 operator DISTINCT 2: "disequality"
281 variable SKOLEM "skolem var"
282 variable VARIABLE "variable"
283 operator TUPLE 2: "a tuple"
285 constant TYPE_CONSTANT \
286 ::CVC4::TypeConstant \
287 ::CVC4::TypeConstantHashStrategy \
290 operator FUNCTION_TYPE 2: "function type"
291 cardinality FUNCTION_TYPE \
292 "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
293 "theory/builtin/theory_builtin_type_rules.h"
294 well-founded FUNCTION_TYPE false
295 operator TUPLE_TYPE 2: "tuple type"
296 cardinality TUPLE_TYPE \
297 "::CVC4::theory::builtin::TupleProperties::computeCardinality(%TYPE%)" \
298 "theory/builtin/theory_builtin_type_rules.h"
299 well-founded TUPLE_TYPE \
300 "::CVC4::theory::builtin::TupleProperties::isWellFounded(%TYPE%)" \
301 "::CVC4::theory::builtin::TupleProperties::mkGroundTerm(%TYPE%)" \
302 "theory/builtin/theory_builtin_type_rules.h"
304 # These will eventually move to a theory of strings.
306 # For now these are unbounded strings over a fixed, finite alphabet
309 Cardinality::INTEGERS \
311 "NodeManager::currentNM()->mkConst(::std::string())" \
314 constant CONST_STRING \
316 ::CVC4::StringHashStrategy \
318 "a string of characters"
319 typerule CONST_STRING ::CVC4::theory::builtin::StringConstantTypeRule
321 typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule
322 typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
323 typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
324 typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule