Partial merge from kind-backend branch, including Minisat and CNF work to

[cvc5.git] / src / theory / builtin / kinds

# 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 ID T header
#
#     Thereafter, ID is bound to your theory.  It becomes part of an
#     enumeration that identifies all theories.  If your theory has
#     several, distinct implementations, they still all share a kinds
#     file, a theory ID, all the defined kinds/operators/types for the
#     theory, typechecker, etc.  They should also share a base class
#     (that's the T above).  The header is the header for this base
#     class.
#
# The very end of this file should end with:
#
#   endtheory
#
# There are several basic commands:
#
#   properties PROPERTIES...
#
#     This command declares properties of the theory.  It can occur
#     more than once, in which case the effect is additive.
#
#     The current set of properties and their meanings are:
#
#       finite            the theory is finite
#       stable-infinite   the theory is stably infinite
#       polite            the theory is polite
#
#       check             the theory supports the check() function
#       propagate         the theory supports propagate() (and explain())
#       staticLearning    the theory supports staticLearning()
#       notifyRestart     the theory supports notifyRestart()
#       presolve          the theory supports presolve()
#
#     In the case of the "theory-supports-function" properties, you
#     need to declare these for your theory or the functions will not
#     be called!  This is used to speed up the core where functionality
#     is not needed.
#
#   rewriter T header
#
#     This declares a rewriter class T for your theory, declared in
#     header.  Your rewriter class provides four functions:
#
#       static void init();
#       static void shutdown();
#       static RewriteResponse preRewrite(TNode node);
#       static RewriteResponse postRewrite(TNode node);
#
#     ...BUT please note that init() and shutdown() may be removed in
#     future, so if possible, do not rely on them being called (and
#     implement them as a no-op).
#
#   typechecker header
#
#     Declare that this theory's typechecker class is defined in the
#     given header.  (#include'd by the TypeChecker class in the expr
#     package.)
#
#   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 "1" (operators must have at least one child).  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,
#     except that parameterized operators may have zero children.  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.
#
#   typerule K typechecker-class
#
#     Declares that a (previously-declared) kind K is typechecked by
#     the typechecker-class.  This class should be defined by the
#     header given to the "typechecker" command, above.  The
#     typechecker-class is used this way by the main TypeChecker code:
#
#       typechecker-class::computeType(NodeManager* nm, TNode n, bool check)
#
#     It returns TypeNode.  It should compute the type of n and return it,
#     and if "check" is true, should actually perform type checking instead
#     of simply type computation.
#
#   sort K cardinality [well-founded ground-term header | not-well-founded] ["comment"]
#
#     This creates a kind K that represents a sort (a "type constant").
#     These kinds of types are "atomic" types; if you need to describe
#     a complex type that takes type arguments (like arrays), use
#     "operator"; if you need to describe one that takes "constant"
#     arguments (like bitvectors), use "constant", and if you invent
#     one that takes both, you could try "parameterized".  In those
#     cases, you'll want to provide a cardinality separately for your
#     type.
#
#     The cardinality argument is a nonnegative number (if the sort is
#     finite), or Cardinality::INTEGERS if the sort has the same
#     cardinality as the integers, or Cardinality::REALS if the sort
#     has the same cardinality as the reals.
#
#     If the sort is well-founded (i.e., there exist ground terms),
#     then the argument should be the string "well-founded"; if not,
#     it should be the string "not-well-founded".  If well-founded,
#     two extra arguments immediately follow---a C++ expression that
#     constructs a ground term (as a Node), and the header that must
#     be #included for that expression to compile.
#
#     For consistency, sorts should end with "_TYPE", but this is not
#     enforced.
#
#   cardinality K cardinality-computer [header]
#
#     This command does not define a kind; the kind K needs to be
#     defined by one of the other commands above.  This command just
#     provides a cardinality for types of kind K.  The
#     "cardinality-computer" is a C++ expression that will yield a
#     Cardinality for the type.  In that expression, the sequence of
#     characters "%TYPE%" will be rewritten with a variable containing
#     a TypeNode of kind K.  The optional "header" argument is an
#     include file necessary to compile the cardinality-computer
#     expression.
#
#     If the cardinality need not be computed per-type (i.e., it's the
#     same for all types of kind K, but the "sort" gesture above could
#     not be used---in which case it doesn't already have a registered
#     cardinality), you can simply construct a Cardinality temporary.
#     For example:
#
#       cardinality MY_TYPE Cardinality(Cardinality::INTEGERS)
#
#     If not, you might opt to use a computer; a common place to put it
#     is with your type checker:
#
#       cardinality MY_TYPE \
#           ::CVC4::theory::foo::TheoryFoo::CardinalityComputer(%TYPE%) \
#           "theory/foo/theory_foo_type_rules.h"
#
#   well-founded K wellfoundedness-computer ground-term-computer [header]
#
#     Analogous to the "cardinality" command above, the well-founded
#     command provides a well-foundedness computer for the type.  A
#     ground term computer is required unless the
#     wellfoundedness-computer is the constant "false".  The ground
#     term computer should return a Node, and it should return the
#     same Node each time for a given type (although usually it's only
#     ever called once anyway since the result is cached).
#
#
# 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"
typechecker "theory/builtin/theory_builtin_type_rules.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 \
    Cardinality::INTEGERS \
    not-well-founded \
    "Built in type for built in operators"

# Justified because we can have an unbounded-but-finite number of
# sorts.  Assuming we have |Z| is probably ok for now..
sort KIND_TYPE \
    Cardinality::INTEGERS \
    not-well-founded \
    "Uninterpreted Sort"

variable SORT_TAG "sort tag"
parameterized SORT_TYPE SORT_TAG 0: "sort type"
# This is really "unknown" cardinality, but maybe this will be good
# enough (for now) ?  Once we support quantifiers, maybe reconsider
# this..
cardinality SORT_TYPE "Cardinality(Cardinality::INTEGERS)"
well-founded SORT_TYPE \
    "::CVC4::theory::builtin::SortProperties::isWellFounded(%TYPE%)" \
    "::CVC4::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)"

# 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"
cardinality FUNCTION_TYPE \
    "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
    "theory/builtin/theory_builtin_type_rules.h"
well-founded FUNCTION_TYPE false
operator TUPLE_TYPE 2: "tuple type"
cardinality TUPLE_TYPE \
    "::CVC4::theory::builtin::TupleProperties::computeCardinality(%TYPE%)" \
    "theory/builtin/theory_builtin_type_rules.h"
well-founded TUPLE_TYPE \
    "::CVC4::theory::builtin::TupleProperties::isWellFounded(%TYPE%)" \
    "::CVC4::theory::builtin::TupleProperties::mkGroundTerm(%TYPE%)" \
    "theory/builtin/theory_builtin_type_rules.h"

# These will eventually move to a theory of strings.
#
# For now these are unbounded strings over a fixed, finite alphabet
# (this may change).
sort STRING_TYPE \
    Cardinality::INTEGERS \
    well-founded \
        "NodeManager::currentNM()->mkConst(::std::string())" \
        "string" \
    "String type"
constant CONST_STRING \
    ::std::string \
    ::CVC4::StringHashStrategy \
    "util/hash.h" \
    "a string of characters"
typerule CONST_STRING ::CVC4::theory::builtin::StringConstantTypeRule

typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule
typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule

constant SUBTYPE_TYPE \
    ::CVC4::Predicate \
    ::CVC4::PredicateHashStrategy \
    "util/predicate.h" \
    "predicate subtype"
cardinality SUBTYPE_TYPE \
    "::CVC4::theory::builtin::SubtypeProperties::computeCardinality(%TYPE%)" \
    "theory/builtin/theory_builtin_type_rules.h"
well-founded SUBTYPE_TYPE \
    "::CVC4::theory::builtin::SubtypeProperties::isWellFounded(%TYPE%)" \
    "::CVC4::theory::builtin::SubtypeProperties::mkGroundTerm(%TYPE%)" \
    "theory/builtin/theory_builtin_type_rules.h"

endtheory