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)\) |
|
duplicate elimination \(\delta(m)\) |
bag.duplicate_removal |
\(\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 * Top contributors (to current version):
3 * Mudathir Mohamed
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * A simple demonstration of reasoning about bags.
14 */
15
16#include <cvc5/cvc5.h>
17
18#include <iostream>
19
20using namespace std;
21using namespace cvc5;
22
23int main()
24{
25 Solver slv;
26 slv.setLogic("ALL");
27 // Produce models
28 slv.setOption("produce-models", "true");
29 slv.setOption("incremental", "true");
30
31 Sort bag = slv.mkBagSort(slv.getStringSort());
32 Term A = slv.mkConst(bag, "A");
33 Term B = slv.mkConst(bag, "B");
34 Term C = slv.mkConst(bag, "C");
35 Term x = slv.mkConst(slv.getStringSort(), "x");
36
37 Term intersectionAC = slv.mkTerm(Kind::BAG_INTER_MIN, {A, C});
38 Term intersectionBC = slv.mkTerm(Kind::BAG_INTER_MIN, {B, C});
39
40 // union disjoint does not distribute over intersection
41 {
42 Term unionDisjointAB = slv.mkTerm(Kind::BAG_UNION_DISJOINT, {A, B});
43 Term lhs = slv.mkTerm(Kind::BAG_INTER_MIN, {unionDisjointAB, C});
44 Term rhs =
45 slv.mkTerm(Kind::BAG_UNION_DISJOINT, {intersectionAC, intersectionBC});
46 Term guess = slv.mkTerm(Kind::EQUAL, {lhs, rhs});
47 cout << "cvc5 reports: " << guess.notTerm() << " is "
48 << slv.checkSatAssuming(guess.notTerm()) << "." << endl;
49
50 cout << A << ": " << slv.getValue(A) << endl;
51 cout << B << ": " << slv.getValue(B) << endl;
52 cout << C << ": " << slv.getValue(C) << endl;
53 cout << lhs << ": " << slv.getValue(lhs) << endl;
54 cout << rhs << ": " << slv.getValue(rhs) << endl;
55 }
56
57 // union max distributes over intersection
58 {
59 Term unionMaxAB = slv.mkTerm(Kind::BAG_UNION_MAX, {A, B});
60 Term lhs = slv.mkTerm(Kind::BAG_INTER_MIN, {unionMaxAB, C});
61 Term rhs =
62 slv.mkTerm(Kind::BAG_UNION_MAX, {intersectionAC, intersectionBC});
63 Term theorem = slv.mkTerm(Kind::EQUAL, {lhs, rhs});
64 cout << "cvc5 reports: " << theorem.notTerm() << " is "
65 << slv.checkSatAssuming(theorem.notTerm()) << "." << endl;
66 }
67
68 // Verify emptbag is a subbag of any bag
69 {
70 Term emptybag = slv.mkEmptyBag(bag);
71 Term theorem = slv.mkTerm(Kind::BAG_SUBBAG, {emptybag, A});
72
73 cout << "cvc5 reports: " << theorem.notTerm() << " is "
74 << slv.checkSatAssuming(theorem.notTerm()) << "." << endl;
75 }
76
77 // find an element with multiplicity 4 in the disjoint union of
78 // ; {|"a", "a", "b", "b", "b"|} and {|"b", "c", "c"|}
79
80 {
81 Term one = slv.mkInteger(1);
82 Term two = slv.mkInteger(2);
83 Term three = slv.mkInteger(3);
84 Term four = slv.mkInteger(4);
85 Term a = slv.mkString("a");
86 Term b = slv.mkString("b");
87 Term c = slv.mkString("c");
88
89 Term bag_a_2 = slv.mkTerm(Kind::BAG_MAKE, {a, two});
90 Term bag_b_3 = slv.mkTerm(Kind::BAG_MAKE, {b, three});
91 Term bag_b_1 = slv.mkTerm(Kind::BAG_MAKE, {b, one});
92 Term bag_c_2 = slv.mkTerm(Kind::BAG_MAKE, {c, two});
93 Term bag_a_2_b_3 = slv.mkTerm(Kind::BAG_UNION_DISJOINT, {bag_a_2, bag_b_3});
94 Term bag_b_1_c_2 = slv.mkTerm(Kind::BAG_UNION_DISJOINT, {bag_b_1, bag_c_2});
95 Term union_disjoint =
96 slv.mkTerm(Kind::BAG_UNION_DISJOINT, {bag_a_2_b_3, bag_b_1_c_2});
97
98 Term count_x = slv.mkTerm(Kind::BAG_COUNT, {x, union_disjoint});
99 Term e = slv.mkTerm(Kind::EQUAL, {four, count_x});
100 Result result = slv.checkSatAssuming(e);
101
102 cout << "cvc5 reports: " << e << " is " << result << "." << endl;
103 if (result.isSat())
104 {
105 cout << x << ": " << slv.getValue(x) << endl;
106 }
107 }
108}
1/******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Andres Noetzli
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * A simple demonstration of reasoning about bags with cvc5.
14 */
15
16import static io.github.cvc5.Kind.*;
17
18import io.github.cvc5.*;
19
20public class Bags
21{
22 public static void main(String args[]) throws CVC5ApiException
23
24 {
25 Solver slv = new Solver();
26 {
27 slv.setLogic("ALL");
28
29 // Produce models
30 slv.setOption("produce-models", "true");
31 slv.setOption("incremental", "true");
32
33 Sort bag = slv.mkBagSort(slv.getStringSort());
34 Term A = slv.mkConst(bag, "A");
35 Term B = slv.mkConst(bag, "B");
36 Term C = slv.mkConst(bag, "C");
37 Term x = slv.mkConst(slv.getStringSort(), "x");
38
39 Term intersectionAC = slv.mkTerm(BAG_INTER_MIN, new Term[] {A, C});
40 Term intersectionBC = slv.mkTerm(BAG_INTER_MIN, new Term[] {B, C});
41
42 // union disjoint does not distribute over intersection
43 {
44 Term unionDisjointAB = slv.mkTerm(BAG_UNION_DISJOINT, new Term[] {A, B});
45 Term lhs = slv.mkTerm(BAG_INTER_MIN, new Term[] {unionDisjointAB, C});
46 Term rhs = slv.mkTerm(BAG_UNION_DISJOINT, new Term[] {intersectionAC, intersectionBC});
47 Term guess = slv.mkTerm(EQUAL, new Term[] {lhs, rhs});
48
49 System.out.println("cvc5 reports: " + guess.notTerm() + " is "
50 + slv.checkSatAssuming(guess.notTerm()) + ".");
51
52 System.out.println(A + ": " + slv.getValue(A));
53 System.out.println(B + ": " + slv.getValue(B));
54 System.out.println(C + ": " + slv.getValue(C));
55 System.out.println(lhs + ": " + slv.getValue(lhs));
56 System.out.println(rhs + ": " + slv.getValue(rhs));
57 }
58
59 // union max distributes over intersection
60 {
61 Term unionMaxAB = slv.mkTerm(BAG_UNION_MAX, new Term[] {A, B});
62 Term lhs = slv.mkTerm(BAG_INTER_MIN, new Term[] {unionMaxAB, C});
63 Term rhs = slv.mkTerm(BAG_UNION_MAX, new Term[] {intersectionAC, intersectionBC});
64 Term theorem = slv.mkTerm(EQUAL, new Term[] {lhs, rhs});
65 System.out.println("cvc5 reports: " + theorem.notTerm() + " is "
66 + slv.checkSatAssuming(theorem.notTerm()) + ".");
67 }
68
69 // Verify emptbag is a subbag of any bag
70 {
71 Term emptybag = slv.mkEmptyBag(bag);
72 Term theorem = slv.mkTerm(BAG_SUBBAG, new Term[] {emptybag, A});
73
74 System.out.println("cvc5 reports: " + theorem.notTerm() + " is "
75 + slv.checkSatAssuming(theorem.notTerm()) + ".");
76 }
77
78 // find an element with multiplicity 4 in the disjoint union of
79 // ; {|"a", "a", "b", "b", "b"|} and {|"b", "c", "c"|}
80 {
81 Term one = slv.mkInteger(1);
82 Term two = slv.mkInteger(2);
83 Term three = slv.mkInteger(3);
84 Term four = slv.mkInteger(4);
85 Term a = slv.mkString("a");
86 Term b = slv.mkString("b");
87 Term c = slv.mkString("c");
88
89 Term bag_a_2 = slv.mkTerm(BAG_MAKE, new Term[] {a, two});
90 Term bag_b_3 = slv.mkTerm(BAG_MAKE, new Term[] {b, three});
91 Term bag_b_1 = slv.mkTerm(BAG_MAKE, new Term[] {b, one});
92 Term bag_c_2 = slv.mkTerm(BAG_MAKE, new Term[] {c, two});
93
94 Term bag_a_2_b_3 = slv.mkTerm(BAG_UNION_DISJOINT, new Term[] {bag_a_2, bag_b_3});
95
96 Term bag_b_1_c_2 = slv.mkTerm(BAG_UNION_DISJOINT, new Term[] {bag_b_1, bag_c_2});
97
98 Term union_disjoint = slv.mkTerm(BAG_UNION_DISJOINT, new Term[] {bag_a_2_b_3, bag_b_1_c_2});
99
100 Term count_x = slv.mkTerm(BAG_COUNT, new Term[] {x, union_disjoint});
101 Term e = slv.mkTerm(EQUAL, new Term[] {four, count_x});
102 Result result = slv.checkSatAssuming(e);
103
104 System.out.println("cvc5 reports: " + e + " is " + result + ".");
105 if (result.isSat())
106 {
107 System.out.println(x + ": " + slv.getValue(x));
108 }
109 }
110 }
111 }
112}
1#!/usr/bin/env python
2###############################################################################
3# Top contributors (to current version):
4# Mudathir Mohamed, Aina Niemetz
5#
6# This file is part of the cvc5 project.
7#
8# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
9# in the top-level source directory and their institutional affiliations.
10# All rights reserved. See the file COPYING in the top-level source
11# directory for licensing information.
12# #############################################################################
13#
14# A simple demonstration of reasoning about bags.
15##
16
17import cvc5
18from cvc5 import Kind
19
20if __name__ == "__main__":
21 slv = cvc5.Solver()
22 slv.setLogic("ALL")
23
24 # Produce models
25 slv.setOption("produce-models", "true")
26 slv.setOption("incremental", "true")
27
28 bag = slv.mkBagSort(slv.getStringSort())
29 A = slv.mkConst(bag, "A")
30 B = slv.mkConst(bag, "B")
31 C = slv.mkConst(bag, "C")
32 x = slv.mkConst(slv.getStringSort(), "x")
33
34 intersectionAC = slv.mkTerm(Kind.BAG_INTER_MIN, A, C)
35 intersectionBC = slv.mkTerm(Kind.BAG_INTER_MIN, B, C)
36
37 # union disjoint does not distribute over intersection
38 unionDisjointAB = slv.mkTerm(Kind.BAG_UNION_DISJOINT, A, B)
39 lhs = slv.mkTerm(Kind.BAG_INTER_MIN, unionDisjointAB, C)
40 rhs = slv.mkTerm(Kind.BAG_UNION_DISJOINT, intersectionAC, intersectionBC)
41 guess = slv.mkTerm(Kind.EQUAL, lhs, rhs)
42 print("cvc5 reports: {} is {}".format(
43 guess.notTerm(), slv.checkSatAssuming(guess.notTerm())))
44
45 print("{}: {}".format(A, slv.getValue(A)))
46 print("{}: {}".format(B, slv.getValue(B)))
47 print("{}: {}".format(C, slv.getValue(C)))
48 print("{}: {}".format(lhs, slv.getValue(lhs)))
49 print("{}: {}".format(rhs, slv.getValue(rhs)))
50
51 # union max distributes over intersection
52 unionMaxAB = slv.mkTerm(Kind.BAG_UNION_MAX, A, B)
53 lhs = slv.mkTerm(Kind.BAG_INTER_MIN, unionMaxAB, C)
54 rhs = slv.mkTerm(Kind.BAG_UNION_MAX, intersectionAC, intersectionBC)
55 theorem = slv.mkTerm(Kind.EQUAL, lhs, rhs)
56 print("cvc5 reports: {} is {}.".format(
57 theorem.notTerm(), slv.checkSatAssuming(theorem.notTerm())))
58
59 # Verify emptbag is a subbag of any bag
60 emptybag = slv.mkEmptyBag(bag)
61 theorem = slv.mkTerm(Kind.BAG_SUBBAG, emptybag, A)
62 print("cvc5 reports: {} is {}.".format(
63 theorem.notTerm(), slv.checkSatAssuming(theorem.notTerm())))
64
65 # find an element with multiplicity 4 in the disjoint union of
66 # {|"a", "a", "b", "b", "b"|} and {|"b", "c", "c"|}
67 one = slv.mkInteger(1)
68 two = slv.mkInteger(2)
69 three = slv.mkInteger(3)
70 four = slv.mkInteger(4)
71 a = slv.mkString("a")
72 b = slv.mkString("b")
73 c = slv.mkString("c")
74
75 bag_a_2 = slv.mkTerm(Kind.BAG_MAKE, a, two)
76 bag_b_3 = slv.mkTerm(Kind.BAG_MAKE, b, three)
77 bag_b_1 = slv.mkTerm(Kind.BAG_MAKE, b, one)
78 bag_c_2 = slv.mkTerm(Kind.BAG_MAKE, c, two)
79 bag_a_2_b_3 = slv.mkTerm(Kind.BAG_UNION_DISJOINT, bag_a_2, bag_b_3)
80 bag_b_1_c_2 = slv.mkTerm(Kind.BAG_UNION_DISJOINT, bag_b_1, bag_c_2)
81 UnionDisjoint = slv.mkTerm(
82 Kind.BAG_UNION_DISJOINT, bag_a_2_b_3, bag_b_1_c_2)
83
84 count_x = slv.mkTerm(Kind.BAG_COUNT, x, UnionDisjoint)
85 e = slv.mkTerm(Kind.EQUAL, four, count_x)
86 result = slv.checkSatAssuming(e)
87
88 print("cvc5 reports: {} is {}.".format(e, result))
89 if result.isSat():
90 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))