1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
|
# 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
|
