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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
|
# 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.
#
# The first non-blank, non-comment line in this file must be a theory
# declaration:
#
# theory T header
#
# There are four basic commands for declaring kinds:
#
# variable K ["comment"]
#
# This declares a kind K that has no operator (it's conceptually a
# VARIABLE). This is appropriate for things like VARIABLE and
# SKOLEM.
#
# operator K #children ["comment"]
#
# Declares a "built-in" operator kind K. Really this is the same
# as "variable" except that it has an operator (automatically
# generated by NodeManager).
#
# You can specify an exact # of children required as the second
# argument to the operator command. In debug mode, assertions are
# automatically included to ensure that no Nodes can ever be
# created violating this. (FIXME: the public Expr stuff should
# enforce them regardless of whether debugging or not.) For
# example, a binary operator could be specified as:
#
# operator LESS_THAN 2 "arithmetic comparison, x < y"
#
# Alternatively, a range can be specified for #children as
# "LB:[UB]", LB and UB representing lower and upper bounds on the
# number of children (inclusive). If there is no lower bound, put
# a "0". If there is no upper bound, leave the colon after LB,
# but omit UB. For example, an N-ary operator might be defined
# as:
#
# operator PLUS 2: "addition on two or more arguments"
#
# parameterized K #children ["comment"]
#
# Declares a "built-in" parameterized operator kind K. 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").
#
# LB and UB are the same as documented for the operator command.
# The first parameter (the function being applied) does not count
# as a child.
#
# For consistency these should start with "APPLY_", but this is
# not enforced.
#
# constant K T Hasher header ["comment"]
#
# Declares a constant kind K. T is the C++ type representing the
# constant internally (and it should be
# ::fully::qualified::like::this), and header is the header needed
# to define it. Hasher is a hash functor type defined like this:
#
# struct MyHashFcn {
# static size_t hash(const T& val);
# };
#
# For consistency, constants taking a non-void payload should
# start with "CONST_", but this is not enforced.
#
# Lines may be broken with a backslash between arguments; for example:
#
# constant CONST_INT \
# int IntHash \
# "" \
# "This is a constant representing an INT.
# Its payload is the C++ int type.
# It is used by the theory of arithmetic."
#
# As shown in the example, ["comment"] fields may be broken across
# multiple lines too.
#
# The expr package guarantees that Nodes built with kinds have the
# following constraints imposed on them. (The #children guarantee
# only holds when assertions are turned on.)
#
# Node meta-kind has operator? # children
# ================== ================= =======================
# variable no zero
# operator yes as documented above
# parameterized yes as documented above
# constant no zero
#
# NOTE THAT This file is actually an executable Bourne shell script
# (sourced by the processing scripts after defining functions called
# "theory," "variable," "operator," "parameterized," and "constant").
# Please don't do anything else in this file other than using these
# commands.
#
theory builtin
# A kind representing "inlined" operators defined with OPERATOR
# Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's
# not stored that way. If you ask for the operator of (EQUAL a b),
# you'll get a special, singleton (BUILTIN EQUAL) Node.
constant BUILTIN ::CVC4::Kind ::CVC4::kind::KindHashFcn \
"expr/kind.h" "The kind of nodes representing built-in operators"
operator EQUAL 2 "equality"
operator DISTINCT 2: "disequality"
operator ITE 3 "if-then-else"
variable SKOLEM "skolem var"
variable VARIABLE "variable"
operator TUPLE 2: "a tuple"
|
