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

theory THEORY_SETS \
    ::cvc5::theory::sets::TheorySets \
    "theory/sets/theory_sets.h"
typechecker "theory/sets/theory_sets_type_rules.h"
rewriter ::cvc5::theory::sets::TheorySetsRewriter \
    "theory/sets/theory_sets_rewriter.h"

properties parametric
properties check presolve

# constants
constant EMPTYSET \
    ::cvc5::EmptySet \
    ::cvc5::EmptySetHashFunction \
    "expr/emptyset.h" \
    "the empty set constant; payload is an instance of the cvc5::EmptySet class"

# the type
operator SET_TYPE 1 "set type, takes as parameter the type of the elements"
cardinality SET_TYPE \
    "::cvc5::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \
    "theory/sets/theory_sets_type_rules.h"
well-founded SET_TYPE \
    "::cvc5::theory::sets::SetsProperties::isWellFounded(%TYPE%)" \
    "::cvc5::theory::sets::SetsProperties::mkGroundTerm(%TYPE%)" \
    "theory/sets/theory_sets_type_rules.h"
enumerator SET_TYPE \
    "::cvc5::theory::sets::SetEnumerator" \
    "theory/sets/theory_sets_type_enumerator.h"

# operators
operator UNION          2  "set union"
operator INTERSECTION   2  "set intersection"
operator SETMINUS       2  "set subtraction"
operator SUBSET         2  "subset predicate; first parameter a subset of second"
operator MEMBER         2  "set membership predicate; first parameter a member of second"

constant SINGLETON_OP \
	::cvc5::SingletonOp \
	::cvc5::SingletonOpHashFunction \
	"theory/sets/singleton_op.h" \
	"operator for singletons; payload is an instance of the cvc5::SingletonOp class"
parameterized SINGLETON SINGLETON_OP 1  \
"constructs a set of a single element. First parameter is a SingletonOp. Second is a term"

operator INSERT         2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)"
operator CARD           1  "set cardinality operator"
operator COMPLEMENT     1  "set COMPLEMENT (with respect to finite universe)"
nullaryoperator UNIVERSE_SET "(finite) universe set, all set variables must be interpreted as subsets of it."

# A set comprehension is specified by:
# (1) a bound variable list x1 ... xn,
# (2) a predicate P[x1...xn], and
# (3) a term t[x1...xn].
# A comprehension C with the above form has members given by the following
# semantics:
# forall y. ( exists x1...xn. P[x1...xn] ^ t[x1...xn] = y ) <=> (member y C)
# where y ranges over the element type of the (set) type of the comprehension.
# Notice that since all sets must be interpreted as finite, this means that
# cvc5 will not be able to construct a model for any set comprehension such
# that there are infinitely many y that satisfy the left hand side of the
# equivalence above. The same limitation occurs more generally when combining
# finite sets with quantified formulas.
operator COMPREHENSION 3 "set comprehension specified by a bound variable list, a predicate, and a term."

# The operator choose returns an element from a given set.
# If set A = {x}, then the term (choose A) is equivalent to the term x.
# If the set is empty, then (choose A) is an arbitrary value.
# If the set has cardinality > 1, then (choose A) will deterministically return an element in A.
operator CHOOSE        1  "return an element in the set given as a parameter"

# The operator is_singleton returns whether the given set is a singleton
operator IS_SINGLETON  1  "return whether the given set is a singleton"

operator JOIN 		   2  "set join"
operator PRODUCT 	   2  "set cartesian product"
operator TRANSPOSE 	   1  "set transpose"
operator TCLOSURE      1  "set transitive closure"
operator JOIN_IMAGE	   2  "set join image"
operator IDEN 	   	   1  "set identity"

typerule UNION          ::cvc5::theory::sets::SetsBinaryOperatorTypeRule
typerule INTERSECTION   ::cvc5::theory::sets::SetsBinaryOperatorTypeRule
typerule SETMINUS       ::cvc5::theory::sets::SetsBinaryOperatorTypeRule
typerule SUBSET         ::cvc5::theory::sets::SubsetTypeRule
typerule MEMBER         ::cvc5::theory::sets::MemberTypeRule
typerule SINGLETON_OP   "SimpleTypeRule<RBuiltinOperator>"
typerule SINGLETON      ::cvc5::theory::sets::SingletonTypeRule
typerule EMPTYSET       ::cvc5::theory::sets::EmptySetTypeRule
typerule INSERT         ::cvc5::theory::sets::InsertTypeRule
typerule CARD           ::cvc5::theory::sets::CardTypeRule
typerule COMPLEMENT     ::cvc5::theory::sets::ComplementTypeRule
typerule UNIVERSE_SET   ::cvc5::theory::sets::UniverseSetTypeRule
typerule COMPREHENSION  ::cvc5::theory::sets::ComprehensionTypeRule
typerule CHOOSE         ::cvc5::theory::sets::ChooseTypeRule
typerule IS_SINGLETON   ::cvc5::theory::sets::IsSingletonTypeRule

typerule JOIN 			::cvc5::theory::sets::RelBinaryOperatorTypeRule
typerule PRODUCT 		::cvc5::theory::sets::RelBinaryOperatorTypeRule
typerule TRANSPOSE 		::cvc5::theory::sets::RelTransposeTypeRule
typerule TCLOSURE 	    ::cvc5::theory::sets::RelTransClosureTypeRule
typerule JOIN_IMAGE	    ::cvc5::theory::sets::JoinImageTypeRule
typerule IDEN 			::cvc5::theory::sets::RelIdenTypeRule

construle UNION         ::cvc5::theory::sets::SetsBinaryOperatorTypeRule
construle SINGLETON     ::cvc5::theory::sets::SingletonTypeRule

endtheory