diff options
Diffstat (limited to 'src/expr/builtin_kinds')
-rw-r--r-- | src/expr/builtin_kinds | 53 |
1 files changed, 48 insertions, 5 deletions
diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds index 806f4f402..f687e3b81 100644 --- a/src/expr/builtin_kinds +++ b/src/expr/builtin_kinds @@ -1,5 +1,48 @@ -EQUAL -ITE -SKOLEM -VARIABLE -TUPLE +# 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" |