# kinds                                                               -*- sh -*-
#
# For documentation on this file format, please refer to
# src/theory/builtin/kinds.
#

theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h"
typechecker "theory/uf/theory_uf_type_rules.h"

properties stable-infinite parametric
properties check propagate ppStaticLearn presolve

rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h"
parameterized APPLY_UF VARIABLE 1: "application of an uninterpreted function; first parameter is the function, remaining ones are parameters to that function"

typerule APPLY_UF ::CVC4::theory::uf::UfTypeRule

variable BOOLEAN_TERM_VARIABLE "Boolean term variable"

operator CARDINALITY_CONSTRAINT 2 "cardinality constraint on sort S: first parameter is (any) term of sort S, second is a positive integer constant k that bounds the cardinality of S"
typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRule

operator COMBINED_CARDINALITY_CONSTRAINT 1 "combined cardinality constraint; parameter is a positive integer constant k that bounds the sum of the cardinalities of all sorts in the signature"
typerule COMBINED_CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CombinedCardinalityConstraintTypeRule

parameterized PARTIAL_APPLY_UF APPLY_UF 1: "partial uninterpreted function application"
typerule PARTIAL_APPLY_UF ::CVC4::theory::uf::PartialTypeRule

operator CARDINALITY_VALUE 1 "cardinality value of sort S: first parameter is (any) term of sort S"
typerule CARDINALITY_VALUE ::CVC4::theory::uf::CardinalityValueTypeRule

operator HO_APPLY 2 "higher-order (partial) function application"
typerule HO_APPLY ::CVC4::theory::uf::HoApplyTypeRule

endtheory