# 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"