1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
# builtin_kinds -*- sh -*-
#
# This "kinds" file is written in a domain-specific language for
# declaring CVC4 kinds. Comments are marked with #, as this line is.
# There are four basic commands:
#
# special K ["comment"]
# operator K ["comment"]
# parameterized K ["comment"]
# constant K T ["comment"]
#
# special K (with an optional comment) declares a kind K that has no
# operator (it's not conceptually an APPLY of an operator to
# operands). This is appropriate for special built-ins,
# e.g. VARIABLE.
#
# operator K (with an optional comment) declares a "built-in"
# operator. Really this is the same as "special" except that it has
# an operator (automatically generated by NodeManager).
#
# parameterized K (with an optional comment) declares a "built-in"
# parameterized operator. This is a theory-specific APPLY, e.g.,
# APPLY_UF, which applies its first parameter (say, "f"), to its
# operands (say, "x" and "y", making the full application "f(x,y)").
# Nodes with such a kind will have an operator (Node::hasOperator()
# returns true, and Node::getOperator() returns the Node of functional
# type representing "f" here), and the "children" are defined to be
# this operator's parameters, and don't include the operator itself
# (here, there are only two children "x" and "y"). For consistency
# these should probably start with "APPLY_", but this is not enforced.
#
# constant K T (with an optional comment) declares a constant kind. T
# is the C++ type representing the constant internally. For
# consistency, these should probably start with "CONST_", but this is
# not enforced.
#
# This file is actually an executable Bourne shell script (sourced by
# the processing scripts after defining functions called "special,"
# "operator," "parameterized," and "constant"). So if you need a
# multi-line comment string, do it the Bourne-like way. Please don't
# do anything else in this file than using these commands though.
#
operator EQUAL "equality"
operator ITE "if-then-else"
special SKOLEM "skolem var"
special VARIABLE "variable"
operator TUPLE "a tuple"
|
