diff options
Diffstat (limited to 'src/theory/builtin/kinds')
| -rw-r--r-- | src/theory/builtin/kinds | 130 |
1 files changed, 130 insertions, 0 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds new file mode 100644 index 000000000..1f22ebef1 --- /dev/null +++ b/src/theory/builtin/kinds @@ -0,0 +1,130 @@ +# 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 builtin ::CVC4::theory::builtin::TheoryBuiltin "theory_builtin.h" + +# 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" + +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/type_constant.h" \ + "basic types" +operator FUNCTION_TYPE 2: "function type" +variable SORT_TYPE "sort type" |