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
 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}