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

(set-logic ALL)

solver.setLogic("ALL");

Sort

(Bag <Sort>)

solver.mkBagSort(cvc5::Sort elementSort);

Constants

(declare-const X (Bag String)

Sort s = solver.mkBagSort(solver.getStringSort());

Term X = solver.mkConst(s, "X");

Union disjoint

(bag.union_disjoint X Y)

Term Y = solver.mkConst(s, "Y");

Term t = solver.mkTerm(Kind::BAG_UNION_DISJOINT, {X, Y});

Union max

(bag.union_max X Y)

Term Y = solver.mkConst(s, "Y");

Term t = solver.mkTerm(Kind::BAG_UNION_MAX, {X, Y});

Intersection min

(bag.inter_min X Y)

Term t = solver.mkTerm(Kind::BAG_INTER_MIN, {X, Y});

Difference subtract

(bag.difference_subtract X Y)

Term t = solver.mkTerm(Kind::BAG_DIFFERENCE_SUBTRACT, {X, Y});

Duplicate elimination

(bag.duplicate_removal X)

Term t = solver.mkTerm(Kind::BAG_DUPLICATE_REMOVAL, {X});

Membership

(bag.member x X)

Term x = solver.mkConst(solver.getStringSort(), "x");

Term t = solver.mkTerm(Kind::BAG_MEMBER, {x, X});

Subbag

(bag.subbag X Y)

Term t = solver.mkTerm(Kind::BAG_SUBBAG, {X, Y});

Emptybag

(as bag.empty (Bag Int)

Term t = solver.mkEmptyBag(s);

Make bag

(bag "a" 3)

Term t = solver.mkTerm(Kind::BAG_MAKE,

{solver.mkString("a"), solver.mkInteger(1)});

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:

examples/api/cpp/bags.cpp

  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 
 20 using namespace std;
 21 using namespace cvc5;
 22 
 23 int 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(BAG_INTER_MIN, {A, C});
 38   Term intersectionBC = slv.mkTerm(BAG_INTER_MIN, {B, C});
 39 
 40   // union disjoint does not distribute over intersection
 41   {
 42     Term unionDisjointAB = slv.mkTerm(BAG_UNION_DISJOINT, {A, B});
 43     Term lhs = slv.mkTerm(BAG_INTER_MIN, {unionDisjointAB, C});
 44     Term rhs = slv.mkTerm(BAG_UNION_DISJOINT, {intersectionAC, intersectionBC});
 45     Term guess = slv.mkTerm(EQUAL, {lhs, rhs});
 46     cout << "cvc5 reports: " << guess.notTerm() << " is "
 47          << slv.checkSatAssuming(guess.notTerm()) << "." << endl;
 48 
 49     cout << A << ": " << slv.getValue(A) << endl;
 50     cout << B << ": " << slv.getValue(B) << endl;
 51     cout << C << ": " << slv.getValue(C) << endl;
 52     cout << lhs << ": " << slv.getValue(lhs) << endl;
 53     cout << rhs << ": " << slv.getValue(rhs) << endl;
 54   }
 55 
 56   // union max distributes over intersection
 57   {
 58     Term unionMaxAB = slv.mkTerm(BAG_UNION_MAX, {A, B});
 59     Term lhs = slv.mkTerm(BAG_INTER_MIN, {unionMaxAB, C});
 60     Term rhs = slv.mkTerm(BAG_UNION_MAX, {intersectionAC, intersectionBC});
 61     Term theorem = slv.mkTerm(EQUAL, {lhs, rhs});
 62     cout << "cvc5 reports: " << theorem.notTerm() << " is "
 63          << slv.checkSatAssuming(theorem.notTerm()) << "." << endl;
 64   }
 65 
 66   // Verify emptbag is a subbag of any bag
 67   {
 68     Term emptybag = slv.mkEmptyBag(bag);
 69     Term theorem = slv.mkTerm(BAG_SUBBAG, {emptybag, A});
 70 
 71     cout << "cvc5 reports: " << theorem.notTerm() << " is "
 72          << slv.checkSatAssuming(theorem.notTerm()) << "." << endl;
 73   }
 74 
 75   // find an element with multiplicity 4 in the disjoint union of
 76   // ; {|"a", "a", "b", "b", "b"|} and {|"b", "c", "c"|}
 77 
 78   {
 79     Term one = slv.mkInteger(1);
 80     Term two = slv.mkInteger(2);
 81     Term three = slv.mkInteger(3);
 82     Term four = slv.mkInteger(4);
 83     Term a = slv.mkString("a");
 84     Term b = slv.mkString("b");
 85     Term c = slv.mkString("c");
 86 
 87     Term bag_a_2 = slv.mkTerm(BAG_MAKE, {a, two});
 88     Term bag_b_3 = slv.mkTerm(BAG_MAKE, {b, three});
 89     Term bag_b_1 = slv.mkTerm(BAG_MAKE, {b, one});
 90     Term bag_c_2 = slv.mkTerm(BAG_MAKE, {c, two});
 91     Term bag_a_2_b_3 = slv.mkTerm(BAG_UNION_DISJOINT, {bag_a_2, bag_b_3});
 92     Term bag_b_1_c_2 = slv.mkTerm(BAG_UNION_DISJOINT, {bag_b_1, bag_c_2});
 93     Term union_disjoint =
 94         slv.mkTerm(BAG_UNION_DISJOINT, {bag_a_2_b_3, bag_b_1_c_2});
 95 
 96     Term count_x = slv.mkTerm(BAG_COUNT, {x, union_disjoint});
 97     Term e = slv.mkTerm(EQUAL, {four, count_x});
 98     Result result = slv.checkSatAssuming(e);
 99 
100     cout << "cvc5 reports: " << e << " is " << result << "." << endl;
101     if (result.isSat())
102     {
103       cout << x << ": " << slv.getValue(x) << endl;
104     }
105   }
106 }