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

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

properties parametric
properties check propagate

# constants
constant EMPTYSET \
    ::CVC4::EmptySet \
    ::CVC4::EmptySetHashFunction \
    "util/emptyset.h" \
    "empty set"

# the type
operator SET_TYPE 1 "set type"
cardinality SET_TYPE \
    "::CVC4::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \
    "theory/sets/theory_sets_type_rules.h"
well-founded SET_TYPE \
    "::CVC4::theory::sets::SetsProperties::isWellFounded(%TYPE%)" \
    "::CVC4::theory::sets::SetsProperties::mkGroundTerm(%TYPE%)" \
    "theory/sets/theory_sets_type_rules.h"
enumerator SET_TYPE \
    "::CVC4::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"
operator MEMBER        2  "set membership"
operator SET_SINGLETON 1  "singleton set"

typerule UNION          ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
typerule INTERSECTION   ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
typerule SETMINUS       ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
typerule SUBSET         ::CVC4::theory::sets::SubsetTypeRule
typerule MEMBER         ::CVC4::theory::sets::MemberTypeRule
typerule SET_SINGLETON  ::CVC4::theory::sets::SetSingletonTypeRule
typerule EMPTYSET       ::CVC4::theory::sets::EmptySetTypeRule

construle UNION         ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
construle INTERSECTION  ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
construle SETMINUS      ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
construle SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule

endtheory