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

theory THEORY_BAGS \
    ::cvc5::theory::bags::TheoryBags \
    "theory/bags/theory_bags.h"
typechecker "theory/bags/theory_bags_type_rules.h"
rewriter ::cvc5::theory::bags::BagsRewriter \
    "theory/bags/bags_rewriter.h"

properties parametric
properties check presolve

# constants
constant EMPTYBAG \
    class \
    EmptyBag \
    ::cvc5::EmptyBagHashFunction \
    "expr/emptybag.h" \
    "the empty bag constant; payload is an instance of the cvc5::EmptyBag class"

# the type
operator BAG_TYPE 1 "bag type, takes as parameter the type of the elements"
cardinality BAG_TYPE \
    "::cvc5::theory::bags::BagsProperties::computeCardinality(%TYPE%)" \
    "theory/bags/theory_bags_type_rules.h"
well-founded BAG_TYPE \
    "::cvc5::theory::bags::BagsProperties::isWellFounded(%TYPE%)" \
    "::cvc5::theory::bags::BagsProperties::mkGroundTerm(%TYPE%)" \
    "theory/bags/theory_bags_type_rules.h"
enumerator BAG_TYPE \
    "::cvc5::theory::bags::BagEnumerator" \
    "theory/bags/theory_bags_type_enumerator.h"

# operators
operator UNION_MAX         2  "union for bags (max)"
operator UNION_DISJOINT    2  "disjoint union for bags (sum)"
operator INTERSECTION_MIN  2  "bag intersection (min)"

# {("a", 2), ("b", 3)} \ {("a", 1)} = {("a", 1), ("b", 3)}
operator DIFFERENCE_SUBTRACT    2  "bag difference1 (subtracts multiplicities)"

# {("a", 2), ("b", 3)} \\ {("a", 1)} = {("b", 3)}
operator DIFFERENCE_REMOVE 2  "bag difference remove (removes shared elements)"

operator SUBBAG            2  "inclusion predicate for bags (less than or equal multiplicities)"
operator BAG_COUNT         2  "multiplicity of an element in a bag"
operator DUPLICATE_REMOVAL 1  "eliminate duplicates in a bag (also known as the delta operator,or the squash operator)"

constant MK_BAG_OP \
  class \
	MakeBagOp \
	::cvc5::MakeBagOpHashFunction \
	"theory/bags/make_bag_op.h" \
	"operator for MK_BAG; payload is an instance of the cvc5::MakeBagOp class"
parameterized MK_BAG MK_BAG_OP 2 \
"constructs a bag from one element along with its multiplicity"

# The operator bag-is-singleton returns whether the given bag is a singleton
operator BAG_IS_SINGLETON  1  "return whether the given bag is a singleton"

operator BAG_CARD          1  "bag cardinality operator"
operator BAG_FROM_SET      1  "converts a set to a bag"
operator BAG_TO_SET        1  "converts a bag to a set"

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

typerule UNION_MAX           ::cvc5::theory::bags::BinaryOperatorTypeRule
typerule UNION_DISJOINT      ::cvc5::theory::bags::BinaryOperatorTypeRule
typerule INTERSECTION_MIN    ::cvc5::theory::bags::BinaryOperatorTypeRule
typerule DIFFERENCE_SUBTRACT ::cvc5::theory::bags::BinaryOperatorTypeRule
typerule DIFFERENCE_REMOVE   ::cvc5::theory::bags::BinaryOperatorTypeRule
typerule SUBBAG              ::cvc5::theory::bags::SubBagTypeRule
typerule BAG_COUNT           ::cvc5::theory::bags::CountTypeRule
typerule DUPLICATE_REMOVAL   ::cvc5::theory::bags::DuplicateRemovalTypeRule
typerule MK_BAG_OP           "SimpleTypeRule<RBuiltinOperator>"
typerule MK_BAG              ::cvc5::theory::bags::MkBagTypeRule
typerule EMPTYBAG            ::cvc5::theory::bags::EmptyBagTypeRule
typerule BAG_CARD            ::cvc5::theory::bags::CardTypeRule
typerule BAG_CHOOSE          ::cvc5::theory::bags::ChooseTypeRule
typerule BAG_IS_SINGLETON    ::cvc5::theory::bags::IsSingletonTypeRule
typerule BAG_FROM_SET        ::cvc5::theory::bags::FromSetTypeRule
typerule BAG_TO_SET          ::cvc5::theory::bags::ToSetTypeRule

construle UNION_DISJOINT     ::cvc5::theory::bags::BinaryOperatorTypeRule
construle MK_BAG             ::cvc5::theory::bags::MkBagTypeRule

endtheory