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 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"
# 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 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
typerule BAG_MAP ::cvc5::theory::bags::BagMapTypeRule
construle UNION_DISJOINT ::cvc5::theory::bags::BinaryOperatorTypeRule
construle MK_BAG ::cvc5::theory::bags::MkBagTypeRule
endtheory
|
