Theory of Bags

examples/api/cpp/bags.cpp 

  1/******************************************************************************
  2 * Top contributors (to current version):
  3 *   Mudathir Mohamed, Aina Niemetz
  4 *
  5 * This file is part of the cvc5 project.
  6 *
  7 * Copyright (c) 2009-2024 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  TermManager tm;
 26  Solver slv(tm);
 27  slv.setLogic("ALL");
 28  // Produce models
 29  slv.setOption("produce-models", "true");
 30  slv.setOption("incremental", "true");
 31
 32  Sort bag = tm.mkBagSort(tm.getStringSort());
 33  Term A = tm.mkConst(bag, "A");
 34  Term B = tm.mkConst(bag, "B");
 35  Term C = tm.mkConst(bag, "C");
 36  Term x = tm.mkConst(tm.getStringSort(), "x");
 37
 38  Term intersectionAC = tm.mkTerm(Kind::BAG_INTER_MIN, {A, C});
 39  Term intersectionBC = tm.mkTerm(Kind::BAG_INTER_MIN, {B, C});
 40
 41  // union disjoint does not distribute over intersection
 42  {
 43    Term unionDisjointAB = tm.mkTerm(Kind::BAG_UNION_DISJOINT, {A, B});
 44    Term lhs = tm.mkTerm(Kind::BAG_INTER_MIN, {unionDisjointAB, C});
 45    Term rhs =
 46        tm.mkTerm(Kind::BAG_UNION_DISJOINT, {intersectionAC, intersectionBC});
 47    Term guess = tm.mkTerm(Kind::EQUAL, {lhs, rhs});
 48    cout << "cvc5 reports: " << guess.notTerm() << " is "
 49         << slv.checkSatAssuming(guess.notTerm()) << "." << endl;
 50
 51    cout << A << ": " << slv.getValue(A) << endl;
 52    cout << B << ": " << slv.getValue(B) << endl;
 53    cout << C << ": " << slv.getValue(C) << endl;
 54    cout << lhs << ": " << slv.getValue(lhs) << endl;
 55    cout << rhs << ": " << slv.getValue(rhs) << endl;
 56  }
 57
 58  // union max distributes over intersection
 59  {
 60    Term unionMaxAB = tm.mkTerm(Kind::BAG_UNION_MAX, {A, B});
 61    Term lhs = tm.mkTerm(Kind::BAG_INTER_MIN, {unionMaxAB, C});
 62    Term rhs = tm.mkTerm(Kind::BAG_UNION_MAX, {intersectionAC, intersectionBC});
 63    Term theorem = tm.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 = tm.mkEmptyBag(bag);
 71    Term theorem = tm.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 = tm.mkInteger(1);
 82    Term two = tm.mkInteger(2);
 83    Term three = tm.mkInteger(3);
 84    Term four = tm.mkInteger(4);
 85    Term a = tm.mkString("a");
 86    Term b = tm.mkString("b");
 87    Term c = tm.mkString("c");
 88
 89    Term bag_a_2 = tm.mkTerm(Kind::BAG_MAKE, {a, two});
 90    Term bag_b_3 = tm.mkTerm(Kind::BAG_MAKE, {b, three});
 91    Term bag_b_1 = tm.mkTerm(Kind::BAG_MAKE, {b, one});
 92    Term bag_c_2 = tm.mkTerm(Kind::BAG_MAKE, {c, two});
 93    Term bag_a_2_b_3 = tm.mkTerm(Kind::BAG_UNION_DISJOINT, {bag_a_2, bag_b_3});
 94    Term bag_b_1_c_2 = tm.mkTerm(Kind::BAG_UNION_DISJOINT, {bag_b_1, bag_c_2});
 95    Term union_disjoint =
 96        tm.mkTerm(Kind::BAG_UNION_DISJOINT, {bag_a_2_b_3, bag_b_1_c_2});
 97
 98    Term count_x = tm.mkTerm(Kind::BAG_COUNT, {x, union_disjoint});
 99    Term e = tm.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}