# 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 BAG_EMPTY \
    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 BAG_UNION_MAX         2  "union for bags (max)"
operator BAG_UNION_DISJOINT    2  "disjoint union for bags (sum)"
operator BAG_INTER_MIN         2  "bag intersection (min)"

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

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

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

constant BAG_MAKE_OP \
  class \
	BagMakeOp \
	::cvc5::BagMakeOpHashFunction \
	"theory/bags/bag_make_op.h" \
	"operator for BAG_MAKE; payload is an instance of the cvc5::BagMakeOp class"
parameterized BAG_MAKE BAG_MAKE_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"

# The bag.map operator applies the first argument, a function of type (-> T1 T2), to every element
# of the second argument, a bag of type (Bag T1), and returns a bag of type (Bag T2).
operator BAG_MAP           2  "bag map function"

typerule BAG_UNION_MAX           ::cvc5::theory::bags::BinaryOperatorTypeRule
typerule BAG_UNION_DISJOINT      ::cvc5::theory::bags::BinaryOperatorTypeRule
typerule BAG_INTER_MIN           ::cvc5::theory::bags::BinaryOperatorTypeRule
typerule BAG_DIFFERENCE_SUBTRACT ::cvc5::theory::bags::BinaryOperatorTypeRule
typerule BAG_DIFFERENCE_REMOVE   ::cvc5::theory::bags::BinaryOperatorTypeRule
typerule BAG_SUBBAG              ::cvc5::theory::bags::SubBagTypeRule
typerule BAG_COUNT               ::cvc5::theory::bags::CountTypeRule
typerule BAG_DUPLICATE_REMOVAL   ::cvc5::theory::bags::DuplicateRemovalTypeRule
typerule BAG_MAKE_OP             "SimpleTypeRule<RBuiltinOperator>"
typerule BAG_MAKE                ::cvc5::theory::bags::BagMakeTypeRule
typerule BAG_EMPTY               ::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
typerule BAG_MAP                 ::cvc5::theory::bags::BagMapTypeRule

construle BAG_UNION_DISJOINT     ::cvc5::theory::bags::BinaryOperatorTypeRule
construle BAG_MAKE               ::cvc5::theory::bags::BagMakeTypeRule

endtheory