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
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
|
# kinds [for builtin theory] -*- 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 [builtin] T header
#
# The special tag "builtin" declares that this is the builtin theory.
# There can be only one and it should be processed first.
#
# 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 THEORY_BUILTIN ::CVC4::theory::builtin::TheoryBuiltin "theory/builtin/theory_builtin.h"
properties stable-infinite
# Rewriter responisble for all the terms of the theory
rewriter ::CVC4::theory::builtin::TheoryBuiltinRewriter "theory/builtin/theory_builtin_rewriter.h"
sort BUILTIN_OPERATOR_TYPE "Built in type for built in operators"
# 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::KindHashStrategy \
"expr/kind.h" \
"The kind of nodes representing built-in operators"
variable FUNCTION "function"
parameterized APPLY FUNCTION 0: "defined function application"
operator EQUAL 2 "equality"
operator DISTINCT 2: "disequality"
variable SKOLEM "skolem var"
variable VARIABLE "variable"
operator TUPLE 2: "a tuple"
constant TYPE_CONSTANT \
::CVC4::TypeConstant \
::CVC4::TypeConstantHashStrategy \
"expr/kind.h" \
"basic types"
operator FUNCTION_TYPE 2: "function type"
operator TUPLE_TYPE 2: "tuple type"
endtheory
|
