Theory Reference: Bags
Finite Bags
cvc5 supports the theory of finite bags using the following sorts, constants, functions and predicates.
For the C++ API examples in the table below, we assume that we have created a cvc5::Solver solver object.
|
SMTLIB language |
C++ API |
|
|
Logic String |
|
|
|
Sort |
|
|
|
Constants |
|
|
|
Union disjoint |
|
|
|
Union max |
|
|
|
Intersection min |
|
|
|
Difference subtract |
|
|
|
Duplicate elimination |
|
|
|
Membership |
|
|
|
Subbag |
|
|
|
Emptybag |
|
|
|
Make bag |
|
|
Semantics
A bag (or a multiset) \(m\) can be defined as a function from the domain of its elements to the set of natural numbers (i.e., \(m : D \rightarrow \mathbb{N}\) ), where \(m(e)\) represents the multiplicity of element \(e\) in the bag \(m\) .
The semantics of supported bag operators is given in the table below.
|
Bag operator |
cvc5 operator |
Semantics |
|
union disjoint \(m_1 \uplus m_2\) |
bag.union_disjoint |
\(\forall e. \; (m_1 \uplus m_2)(e) = m_1(e) + m_2 (e)\) |
|
union max \(m_1 \cup m_2\) |
bag.union_max |
\(\forall e. \; (m_1 \cup m_2)(e) = max(m_1(e), m_2 (e))\) |
|
intersection \(m_1 \cap m_2\) |
bag.inter_min |
\(\forall e. \; (m_1 \cap m_2)(e) = min(m_1(e), m_2 (e))\) |
|
difference subtract \(m_1 \setminus m_2\) |
bag.difference_subtract |
\(\forall e. \; (m_1 \setminus m_2)(e) = max(m_1(e) - m_2 (e), 0)\) |
|
difference remove \(m_1 \setminus\setminus m_2\) |
bag.difference_remove |
\(\forall e. \; (m_1 \setminus\setminus m_2)(e) = ite(m_2(e) = 0, m_1(e), 0)\) |
|
setof \(\delta(m)\) |
bag.setof |
\(\forall e. \; (\delta(m))(e) = ite(1 \leq m(e), 1, 0)\) |
|
subbag \(m_1 \subseteq m_2\) |
bag.subbag |
\(\forall e. \; m_1(e) \leq m_2(e)\) |
|
equality \(m_1 = m_2\) |
= |
\(\forall e. \; m_1(e) = m_2(e)\) |
|
membership \(e \in m\) |
bag.member |
\(m(e) \geq 1\) |
Below is a more extensive example on how to use finite bags:
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of reasoning about bags.
11 */
12
13#include <cvc5/cvc5.h>
14
15#include <iostream>
16
17using namespace std;
18using namespace cvc5;
19
20int main()
21{
22 TermManager tm;
23 Solver slv(tm);
24 slv.setLogic("ALL");
25 // Produce models
26 slv.setOption("produce-models", "true");
27 slv.setOption("incremental", "true");
28
29 Sort bag = tm.mkBagSort(tm.getStringSort());
30 Term A = tm.mkConst(bag, "A");
31 Term B = tm.mkConst(bag, "B");
32 Term C = tm.mkConst(bag, "C");
33 Term x = tm.mkConst(tm.getStringSort(), "x");
34
35 Term intersectionAC = tm.mkTerm(Kind::BAG_INTER_MIN, {A, C});
36 Term intersectionBC = tm.mkTerm(Kind::BAG_INTER_MIN, {B, C});
37
38 // union disjoint does not distribute over intersection
39 {
40 Term unionDisjointAB = tm.mkTerm(Kind::BAG_UNION_DISJOINT, {A, B});
41 Term lhs = tm.mkTerm(Kind::BAG_INTER_MIN, {unionDisjointAB, C});
42 Term rhs =
43 tm.mkTerm(Kind::BAG_UNION_DISJOINT, {intersectionAC, intersectionBC});
44 Term guess = tm.mkTerm(Kind::EQUAL, {lhs, rhs});
45 cout << "cvc5 reports: " << guess.notTerm() << " is "
46 << slv.checkSatAssuming(guess.notTerm()) << "." << endl;
47
48 cout << A << ": " << slv.getValue(A) << endl;
49 cout << B << ": " << slv.getValue(B) << endl;
50 cout << C << ": " << slv.getValue(C) << endl;
51 cout << lhs << ": " << slv.getValue(lhs) << endl;
52 cout << rhs << ": " << slv.getValue(rhs) << endl;
53 }
54
55 // union max distributes over intersection
56 {
57 Term unionMaxAB = tm.mkTerm(Kind::BAG_UNION_MAX, {A, B});
58 Term lhs = tm.mkTerm(Kind::BAG_INTER_MIN, {unionMaxAB, C});
59 Term rhs = tm.mkTerm(Kind::BAG_UNION_MAX, {intersectionAC, intersectionBC});
60 Term theorem = tm.mkTerm(Kind::EQUAL, {lhs, rhs});
61 cout << "cvc5 reports: " << theorem.notTerm() << " is "
62 << slv.checkSatAssuming(theorem.notTerm()) << "." << endl;
63 }
64
65 // Verify emptbag is a subbag of any bag
66 {
67 Term emptybag = tm.mkEmptyBag(bag);
68 Term theorem = tm.mkTerm(Kind::BAG_SUBBAG, {emptybag, A});
69
70 cout << "cvc5 reports: " << theorem.notTerm() << " is "
71 << slv.checkSatAssuming(theorem.notTerm()) << "." << endl;
72 }
73
74 // find an element with multiplicity 4 in the disjoint union of
75 // ; {|"a", "a", "b", "b", "b"|} and {|"b", "c", "c"|}
76
77 {
78 Term one = tm.mkInteger(1);
79 Term two = tm.mkInteger(2);
80 Term three = tm.mkInteger(3);
81 Term four = tm.mkInteger(4);
82 Term a = tm.mkString("a");
83 Term b = tm.mkString("b");
84 Term c = tm.mkString("c");
85
86 Term bag_a_2 = tm.mkTerm(Kind::BAG_MAKE, {a, two});
87 Term bag_b_3 = tm.mkTerm(Kind::BAG_MAKE, {b, three});
88 Term bag_b_1 = tm.mkTerm(Kind::BAG_MAKE, {b, one});
89 Term bag_c_2 = tm.mkTerm(Kind::BAG_MAKE, {c, two});
90 Term bag_a_2_b_3 = tm.mkTerm(Kind::BAG_UNION_DISJOINT, {bag_a_2, bag_b_3});
91 Term bag_b_1_c_2 = tm.mkTerm(Kind::BAG_UNION_DISJOINT, {bag_b_1, bag_c_2});
92 Term union_disjoint =
93 tm.mkTerm(Kind::BAG_UNION_DISJOINT, {bag_a_2_b_3, bag_b_1_c_2});
94
95 Term count_x = tm.mkTerm(Kind::BAG_COUNT, {x, union_disjoint});
96 Term e = tm.mkTerm(Kind::EQUAL, {four, count_x});
97 Result result = slv.checkSatAssuming(e);
98
99 cout << "cvc5 reports: " << e << " is " << result << "." << endl;
100 if (result.isSat())
101 {
102 cout << x << ": " << slv.getValue(x) << endl;
103 }
104 }
105}
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of reasoning about bags.
11 */
12
13#include <cvc5/c/cvc5.h>
14#include <stdio.h>
15
16int main()
17{
18 Cvc5TermManager* tm = cvc5_term_manager_new();
19 Cvc5* slv = cvc5_new(tm);
20 cvc5_set_logic(slv, "ALL");
21 // Produce models
22 cvc5_set_option(slv, "produce-models", "true");
23 cvc5_set_option(slv, "incremental", "true");
24
25 Cvc5Sort bag = cvc5_mk_bag_sort(tm, cvc5_get_string_sort(tm));
26 Cvc5Term A = cvc5_mk_const(tm, bag, "A");
27 Cvc5Term B = cvc5_mk_const(tm, bag, "B");
28 Cvc5Term C = cvc5_mk_const(tm, bag, "C");
29 Cvc5Term x = cvc5_mk_const(tm, cvc5_get_string_sort(tm), "x");
30
31 Cvc5Term args[2];
32
33 args[0] = A;
34 args[1] = C;
35 Cvc5Term interAC = cvc5_mk_term(tm, CVC5_KIND_BAG_INTER_MIN, 2, args);
36 args[0] = B;
37 args[1] = C;
38 Cvc5Term interBC = cvc5_mk_term(tm, CVC5_KIND_BAG_INTER_MIN, 2, args);
39
40 // union disjoint does not distribute over intersection
41 {
42 args[0] = A;
43 args[1] = B;
44 Cvc5Term union_disAB =
45 cvc5_mk_term(tm, CVC5_KIND_BAG_UNION_DISJOINT, 2, args);
46
47 args[0] = union_disAB;
48 args[1] = C;
49 Cvc5Term lhs = cvc5_mk_term(tm, CVC5_KIND_BAG_INTER_MIN, 2, args);
50
51 args[0] = interAC;
52 args[1] = interBC;
53 Cvc5Term rhs = cvc5_mk_term(tm, CVC5_KIND_BAG_UNION_DISJOINT, 2, args);
54
55 args[0] = lhs;
56 args[1] = rhs;
57 Cvc5Term guess = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args);
58
59 Cvc5Term args_not[1] = {guess};
60 Cvc5Term not_guess = cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args_not);
61
62 Cvc5Term assumptions[1] = {not_guess};
63 printf("cvc5 reports: %s is %s.\n",
64 cvc5_term_to_string(not_guess),
65 cvc5_result_to_string(cvc5_check_sat_assuming(slv, 1, assumptions)));
66
67 // Note: The const char* returned by cvc5_term_to_string is only valid
68 // until the next call to cvc5_term_to_string. Thus, we cannot
69 // chain calls to this function like this:
70 // printf("%s: %s\n",
71 // cvc5_term_to_string(A),
72 // cvc5_term_to_string(cvc5_get_value(slv, A)));
73 // Instead, we have to split such printf calls into two.
74 printf("%s: ", cvc5_term_to_string(A));
75 printf("%s\n", cvc5_term_to_string(cvc5_get_value(slv, A)));
76
77 printf("%s: ", cvc5_term_to_string(B));
78 printf("%s\n", cvc5_term_to_string(cvc5_get_value(slv, B)));
79
80 printf("%s: ", cvc5_term_to_string(C));
81 printf("%s\n", cvc5_term_to_string(cvc5_get_value(slv, C)));
82
83 printf("%s: ", cvc5_term_to_string(lhs));
84 printf("%s\n", cvc5_term_to_string(cvc5_get_value(slv, lhs)));
85
86 printf("%s: ", cvc5_term_to_string(rhs));
87 printf("%s\n", cvc5_term_to_string(cvc5_get_value(slv, rhs)));
88 }
89
90 // union max distributes over intersection
91 {
92 args[0] = A;
93 args[1] = B;
94 Cvc5Term union_maxAB = cvc5_mk_term(tm, CVC5_KIND_BAG_UNION_MAX, 2, args);
95
96 args[0] = union_maxAB;
97 args[1] = C;
98 Cvc5Term lhs = cvc5_mk_term(tm, CVC5_KIND_BAG_INTER_MIN, 2, args);
99
100 args[0] = interAC;
101 args[1] = interBC;
102 Cvc5Term rhs = cvc5_mk_term(tm, CVC5_KIND_BAG_UNION_MAX, 2, args);
103
104 args[0] = lhs;
105 args[1] = rhs;
106 Cvc5Term theorem = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args);
107
108 Cvc5Term not_args[1] = {theorem};
109 Cvc5Term not_theorem = cvc5_mk_term(tm, CVC5_KIND_NOT, 1, not_args);
110 Cvc5Term assumptions[1] = {not_theorem};
111 printf("cvc5 reports: %s is %s.\n",
112 cvc5_term_to_string(not_theorem),
113 cvc5_result_to_string(cvc5_check_sat_assuming(slv, 1, assumptions)));
114 }
115
116 // Verify emptbag is a subbag of any bag
117 {
118 Cvc5Term empty_bag = cvc5_mk_empty_bag(tm, bag);
119 args[0] = empty_bag;
120 args[1] = A;
121 Cvc5Term theorem = cvc5_mk_term(tm, CVC5_KIND_BAG_SUBBAG, 2, args);
122
123 Cvc5Term not_args[1] = {theorem};
124 Cvc5Term not_theorem = cvc5_mk_term(tm, CVC5_KIND_NOT, 1, not_args);
125 Cvc5Term assumptions[1] = {not_theorem};
126 printf("cvc5 reports: %s is %s.\n",
127 cvc5_term_to_string(not_theorem),
128 cvc5_result_to_string(cvc5_check_sat_assuming(slv, 1, assumptions)));
129 }
130
131 // find an element with multiplicity 4 in the disjoint union of
132 // ; {|"a", "a", "b", "b", "b"|} and {|"b", "c", "c"|}
133
134 {
135 Cvc5Term one = cvc5_mk_integer_int64(tm, 1);
136 Cvc5Term two = cvc5_mk_integer_int64(tm, 2);
137 Cvc5Term three = cvc5_mk_integer_int64(tm, 3);
138 Cvc5Term four = cvc5_mk_integer_int64(tm, 4);
139
140 Cvc5Term a = cvc5_mk_string(tm, "a", false);
141 Cvc5Term b = cvc5_mk_string(tm, "b", false);
142 Cvc5Term c = cvc5_mk_string(tm, "c", false);
143
144 args[0] = a;
145 args[1] = two;
146 Cvc5Term bag_a_2 = cvc5_mk_term(tm, CVC5_KIND_BAG_MAKE, 2, args);
147
148 args[0] = b;
149 args[1] = three;
150 Cvc5Term bag_b_3 = cvc5_mk_term(tm, CVC5_KIND_BAG_MAKE, 2, args);
151
152 args[0] = b;
153 args[1] = one;
154 Cvc5Term bag_b_1 = cvc5_mk_term(tm, CVC5_KIND_BAG_MAKE, 2, args);
155
156 args[0] = c;
157 args[1] = two;
158 Cvc5Term bag_c_2 = cvc5_mk_term(tm, CVC5_KIND_BAG_MAKE, 2, args);
159
160 args[0] = bag_a_2;
161 args[1] = bag_b_3;
162 Cvc5Term bag_a_2_b_3 =
163 cvc5_mk_term(tm, CVC5_KIND_BAG_UNION_DISJOINT, 2, args);
164
165 args[0] = bag_b_1;
166 args[1] = bag_c_2;
167 Cvc5Term bag_b_1_c_2 =
168 cvc5_mk_term(tm, CVC5_KIND_BAG_UNION_DISJOINT, 2, args);
169
170 args[0] = bag_a_2_b_3;
171 args[1] = bag_b_1_c_2;
172 Cvc5Term union_disjoint =
173 cvc5_mk_term(tm, CVC5_KIND_BAG_UNION_DISJOINT, 2, args);
174
175 args[0] = x;
176 args[1] = union_disjoint;
177 Cvc5Term count_x = cvc5_mk_term(tm, CVC5_KIND_BAG_COUNT, 2, args);
178
179 args[0] = four;
180 args[1] = count_x;
181 Cvc5Term e = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args);
182
183 Cvc5Term assumptions[1] = {e};
184 Cvc5Result result = cvc5_check_sat_assuming(slv, 1, assumptions);
185
186 printf("cvc5 reports: %s is %s.\n",
187 cvc5_term_to_string(e),
188 cvc5_result_to_string(result));
189
190 if (cvc5_result_is_sat(result))
191 {
192 printf("%s: ", cvc5_term_to_string(x));
193 printf("%s\n", cvc5_term_to_string(cvc5_get_value(slv, x)));
194 }
195 }
196
197 cvc5_delete(slv);
198 cvc5_term_manager_delete(tm);
199}
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of reasoning about bags with cvc5.
11 */
12
13import static io.github.cvc5.Kind.*;
14
15import io.github.cvc5.*;
16
17public class Bags
18{
19 public static void main(String args[]) throws CVC5ApiException
20
21 {
22 TermManager tm = new TermManager();
23 Solver slv = new Solver(tm);
24 {
25 slv.setLogic("ALL");
26
27 // Produce models
28 slv.setOption("produce-models", "true");
29 slv.setOption("incremental", "true");
30
31 Sort bag = tm.mkBagSort(tm.getStringSort());
32 Term A = tm.mkConst(bag, "A");
33 Term B = tm.mkConst(bag, "B");
34 Term C = tm.mkConst(bag, "C");
35 Term x = tm.mkConst(tm.getStringSort(), "x");
36
37 Term intersectionAC = tm.mkTerm(BAG_INTER_MIN, new Term[] {A, C});
38 Term intersectionBC = tm.mkTerm(BAG_INTER_MIN, new Term[] {B, C});
39
40 // union disjoint does not distribute over intersection
41 {
42 Term unionDisjointAB = tm.mkTerm(BAG_UNION_DISJOINT, new Term[] {A, B});
43 Term lhs = tm.mkTerm(BAG_INTER_MIN, new Term[] {unionDisjointAB, C});
44 Term rhs = tm.mkTerm(BAG_UNION_DISJOINT, new Term[] {intersectionAC, intersectionBC});
45 Term guess = tm.mkTerm(EQUAL, new Term[] {lhs, rhs});
46
47 System.out.println("cvc5 reports: " + guess.notTerm() + " is "
48 + slv.checkSatAssuming(guess.notTerm()) + ".");
49
50 System.out.println(A + ": " + slv.getValue(A));
51 System.out.println(B + ": " + slv.getValue(B));
52 System.out.println(C + ": " + slv.getValue(C));
53 System.out.println(lhs + ": " + slv.getValue(lhs));
54 System.out.println(rhs + ": " + slv.getValue(rhs));
55 }
56
57 // union max distributes over intersection
58 {
59 Term unionMaxAB = tm.mkTerm(BAG_UNION_MAX, new Term[] {A, B});
60 Term lhs = tm.mkTerm(BAG_INTER_MIN, new Term[] {unionMaxAB, C});
61 Term rhs = tm.mkTerm(BAG_UNION_MAX, new Term[] {intersectionAC, intersectionBC});
62 Term theorem = tm.mkTerm(EQUAL, new Term[] {lhs, rhs});
63 System.out.println("cvc5 reports: " + theorem.notTerm() + " is "
64 + slv.checkSatAssuming(theorem.notTerm()) + ".");
65 }
66
67 // Verify emptbag is a subbag of any bag
68 {
69 Term emptybag = tm.mkEmptyBag(bag);
70 Term theorem = tm.mkTerm(BAG_SUBBAG, new Term[] {emptybag, A});
71
72 System.out.println("cvc5 reports: " + theorem.notTerm() + " is "
73 + slv.checkSatAssuming(theorem.notTerm()) + ".");
74 }
75
76 // find an element with multiplicity 4 in the disjoint union of
77 // ; {|"a", "a", "b", "b", "b"|} and {|"b", "c", "c"|}
78 {
79 Term one = tm.mkInteger(1);
80 Term two = tm.mkInteger(2);
81 Term three = tm.mkInteger(3);
82 Term four = tm.mkInteger(4);
83 Term a = tm.mkString("a");
84 Term b = tm.mkString("b");
85 Term c = tm.mkString("c");
86
87 Term bag_a_2 = tm.mkTerm(BAG_MAKE, new Term[] {a, two});
88 Term bag_b_3 = tm.mkTerm(BAG_MAKE, new Term[] {b, three});
89 Term bag_b_1 = tm.mkTerm(BAG_MAKE, new Term[] {b, one});
90 Term bag_c_2 = tm.mkTerm(BAG_MAKE, new Term[] {c, two});
91
92 Term bag_a_2_b_3 = tm.mkTerm(BAG_UNION_DISJOINT, new Term[] {bag_a_2, bag_b_3});
93
94 Term bag_b_1_c_2 = tm.mkTerm(BAG_UNION_DISJOINT, new Term[] {bag_b_1, bag_c_2});
95
96 Term union_disjoint = tm.mkTerm(BAG_UNION_DISJOINT, new Term[] {bag_a_2_b_3, bag_b_1_c_2});
97
98 Term count_x = tm.mkTerm(BAG_COUNT, new Term[] {x, union_disjoint});
99 Term e = tm.mkTerm(EQUAL, new Term[] {four, count_x});
100 Result result = slv.checkSatAssuming(e);
101
102 System.out.println("cvc5 reports: " + e + " is " + result + ".");
103 if (result.isSat())
104 {
105 System.out.println(x + ": " + slv.getValue(x));
106 }
107 }
108 }
109 Context.deletePointers();
110 }
111}
1#!/usr/bin/env python
2###############################################################################
3# This file is part of the cvc5 project.
4#
5# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
6# in the top-level source directory and their institutional affiliations.
7# All rights reserved. See the file COPYING in the top-level source
8# directory for licensing information.
9# #############################################################################
10#
11# A simple demonstration of reasoning about bags.
12##
13
14import cvc5
15from cvc5 import Kind
16
17if __name__ == "__main__":
18 tm = cvc5.TermManager()
19 slv = cvc5.Solver(tm)
20 slv.setLogic("ALL")
21
22 # Produce models
23 slv.setOption("produce-models", "true")
24 slv.setOption("incremental", "true")
25
26 bag = tm.mkBagSort(tm.getStringSort())
27 A = tm.mkConst(bag, "A")
28 B = tm.mkConst(bag, "B")
29 C = tm.mkConst(bag, "C")
30 x = tm.mkConst(tm.getStringSort(), "x")
31
32 intersectionAC = tm.mkTerm(Kind.BAG_INTER_MIN, A, C)
33 intersectionBC = tm.mkTerm(Kind.BAG_INTER_MIN, B, C)
34
35 # union disjoint does not distribute over intersection
36 unionDisjointAB = tm.mkTerm(Kind.BAG_UNION_DISJOINT, A, B)
37 lhs = tm.mkTerm(Kind.BAG_INTER_MIN, unionDisjointAB, C)
38 rhs = tm.mkTerm(Kind.BAG_UNION_DISJOINT, intersectionAC, intersectionBC)
39 guess = tm.mkTerm(Kind.EQUAL, lhs, rhs)
40 print("cvc5 reports: {} is {}".format(
41 guess.notTerm(), slv.checkSatAssuming(guess.notTerm())))
42
43 print("{}: {}".format(A, slv.getValue(A)))
44 print("{}: {}".format(B, slv.getValue(B)))
45 print("{}: {}".format(C, slv.getValue(C)))
46 print("{}: {}".format(lhs, slv.getValue(lhs)))
47 print("{}: {}".format(rhs, slv.getValue(rhs)))
48
49 # union max distributes over intersection
50 unionMaxAB = tm.mkTerm(Kind.BAG_UNION_MAX, A, B)
51 lhs = tm.mkTerm(Kind.BAG_INTER_MIN, unionMaxAB, C)
52 rhs = tm.mkTerm(Kind.BAG_UNION_MAX, intersectionAC, intersectionBC)
53 theorem = tm.mkTerm(Kind.EQUAL, lhs, rhs)
54 print("cvc5 reports: {} is {}.".format(
55 theorem.notTerm(), slv.checkSatAssuming(theorem.notTerm())))
56
57 # Verify emptbag is a subbag of any bag
58 emptybag = tm.mkEmptyBag(bag)
59 theorem = tm.mkTerm(Kind.BAG_SUBBAG, emptybag, A)
60 print("cvc5 reports: {} is {}.".format(
61 theorem.notTerm(), slv.checkSatAssuming(theorem.notTerm())))
62
63 # find an element with multiplicity 4 in the disjoint union of
64 # {|"a", "a", "b", "b", "b"|} and {|"b", "c", "c"|}
65 one = tm.mkInteger(1)
66 two = tm.mkInteger(2)
67 three = tm.mkInteger(3)
68 four = tm.mkInteger(4)
69 a = tm.mkString("a")
70 b = tm.mkString("b")
71 c = tm.mkString("c")
72
73 bag_a_2 = tm.mkTerm(Kind.BAG_MAKE, a, two)
74 bag_b_3 = tm.mkTerm(Kind.BAG_MAKE, b, three)
75 bag_b_1 = tm.mkTerm(Kind.BAG_MAKE, b, one)
76 bag_c_2 = tm.mkTerm(Kind.BAG_MAKE, c, two)
77 bag_a_2_b_3 = tm.mkTerm(Kind.BAG_UNION_DISJOINT, bag_a_2, bag_b_3)
78 bag_b_1_c_2 = tm.mkTerm(Kind.BAG_UNION_DISJOINT, bag_b_1, bag_c_2)
79 UnionDisjoint = tm.mkTerm(
80 Kind.BAG_UNION_DISJOINT, bag_a_2_b_3, bag_b_1_c_2)
81
82 count_x = tm.mkTerm(Kind.BAG_COUNT, x, UnionDisjoint)
83 e = tm.mkTerm(Kind.EQUAL, four, count_x)
84 result = slv.checkSatAssuming(e)
85
86 print("cvc5 reports: {} is {}.".format(e, result))
87 if result.isSat():
88 print("{}: {} ".format(x, slv.getValue(x)))
1(set-logic ALL)
2
3(set-option :produce-models true)
4(set-option :incremental true)
5
6(declare-const A (Bag String))
7(declare-const B (Bag String))
8(declare-const C (Bag String))
9(declare-const x String)
10
11; union disjoint does not distribute over intersection
12; sat
13(check-sat-assuming
14 ((distinct
15 (bag.inter_min (bag.union_disjoint A B) C)
16 (bag.union_disjoint (bag.inter_min A C) (bag.inter_min B C)))))
17
18
19(get-value (A))
20(get-value (B))
21(get-value (C))
22(get-value ((bag.inter_min (bag.union_disjoint A B) C)))
23(get-value ((bag.union_disjoint (bag.inter_min A C) (bag.inter_min B C))))
24
25; union max distributes over intersection
26; unsat
27(check-sat-assuming
28 ((distinct
29 (bag.inter_min (bag.union_max A B) C)
30 (bag.union_max (bag.inter_min A C) (bag.inter_min B C)))))
31
32; Verify emptbag is a subbag of any bag
33; unsat
34(check-sat-assuming
35 ((not (bag.subbag (as bag.empty (Bag String)) A))))
36
37; find an element with multiplicity 4 in the disjoint union of
38; {|"a", "a", "b", "b", "b"|} and {|"b", "c", "c"|}
39(check-sat-assuming
40 ((= 4
41 (bag.count x
42 (bag.union_disjoint
43 (bag.union_disjoint (bag "a" 2) (bag "b" 3))
44 (bag.union_disjoint (bag "b" 1) (bag "c" 2)))))))
45
46; x is "b"
47(get-value (x))