diff options
Diffstat (limited to 'src/expr/builtin_kinds')
| -rw-r--r-- | src/expr/builtin_kinds | 156 |
1 files changed, 114 insertions, 42 deletions
diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds index f687e3b81..bb224aa91 100644 --- a/src/expr/builtin_kinds +++ b/src/expr/builtin_kinds @@ -2,47 +2,119 @@ # # 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. # +# 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 "equality" -operator ITE "if-then-else" -special SKOLEM "skolem var" -special VARIABLE "variable" -operator TUPLE "a tuple" +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" |