From: mudathirmahgoub <mudathirmahgoub@gmail.com>
Date: Thu, 31 Mar 2022 15:17:22 +0000 (-0500)
Subject: Add examples/bags.cpp (#8463)
X-Git-Tag: cvc5-1.0.0~95
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6c421a82211f8e9c1e8d4d0725bedce567fe5aa6;p=cvc5.git

Add examples/bags.cpp (#8463)
---

diff --git a/docs/examples/bags.rst b/docs/examples/bags.rst
new file mode 100644
index 000000000..ae3b267e2
--- /dev/null
+++ b/docs/examples/bags.rst
@@ -0,0 +1,9 @@
+Theory of Bags
+=================
+
+
+.. api-examples::
+    <examples>/api/cpp/bags.cpp
+    <examples>/api/java/Bags.java
+    <examples>/api/python/bags.py
+    <examples>/api/smtlib/bags.smt2
diff --git a/docs/examples/examples.rst b/docs/examples/examples.rst
index b9303f1d9..9812027ed 100644
--- a/docs/examples/examples.rst
+++ b/docs/examples/examples.rst
@@ -11,6 +11,7 @@ input mechanisms.
 
     helloworld
     exceptions
+    bags
     bitvectors
     bitvectors_and_arrays
     extract
diff --git a/docs/theories/bags.rst b/docs/theories/bags.rst
index d3e32fb28..d29d3905e 100644
--- a/docs/theories/bags.rst
+++ b/docs/theories/bags.rst
@@ -82,5 +82,8 @@ The semantics of supported bag operators is given in the table below.
 Below is a more extensive example on how to use finite bags:
 
 .. api-examples::
+    <examples>/api/cpp/bags.cpp
+    <examples>/api/cpp/Bags.java
+    <examples>/api/cpp/bags.py
     <examples>/api/smtlib/bags.smt2
 
diff --git a/examples/api/cpp/CMakeLists.txt b/examples/api/cpp/CMakeLists.txt
index 6d462da5d..02496fe8f 100644
--- a/examples/api/cpp/CMakeLists.txt
+++ b/examples/api/cpp/CMakeLists.txt
@@ -14,6 +14,7 @@
 ##
 
 set(CVC5_EXAMPLES_API
+  bags
   bitvectors
   bitvectors_and_arrays
   combination
diff --git a/examples/api/cpp/bags.cpp b/examples/api/cpp/bags.cpp
new file mode 100644
index 000000000..6df2bc46e
--- /dev/null
+++ b/examples/api/cpp/bags.cpp
@@ -0,0 +1,105 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * A simple demonstration of reasoning about bags.
+ */
+
+#include <cvc5/cvc5.h>
+
+#include <iostream>
+
+using namespace std;
+using namespace cvc5;
+
+int main()
+{
+  Solver slv;
+  slv.setLogic("ALL");
+  // Produce models
+  slv.setOption("produce-models", "true");
+  slv.setOption("incremental", "true");
+
+  Sort bag = slv.mkBagSort(slv.getStringSort());
+  Term A = slv.mkConst(bag, "A");
+  Term B = slv.mkConst(bag, "B");
+  Term C = slv.mkConst(bag, "C");
+  Term x = slv.mkConst(slv.getStringSort(), "x");
+
+  Term intersectionAC = slv.mkTerm(BAG_INTER_MIN, {A, C});
+  Term intersectionBC = slv.mkTerm(BAG_INTER_MIN, {B, C});
+
+  // union disjoint does not distribute over intersection
+  {
+    Term unionDisjointAB = slv.mkTerm(BAG_UNION_DISJOINT, {A, B});
+    Term lhs = slv.mkTerm(BAG_INTER_MIN, {unionDisjointAB, C});
+    Term rhs = slv.mkTerm(BAG_UNION_DISJOINT, {intersectionAC, intersectionBC});
+    Term guess = slv.mkTerm(EQUAL, {lhs, rhs});
+    cout << "cvc5 reports: " << guess.notTerm() << " is "
+         << slv.checkSatAssuming(guess.notTerm()) << "." << endl;
+
+    cout << A << ": " << slv.getValue(A) << endl;
+    cout << B << ": " << slv.getValue(B) << endl;
+    cout << C << ": " << slv.getValue(C) << endl;
+    cout << lhs << ": " << slv.getValue(lhs) << endl;
+    cout << rhs << ": " << slv.getValue(rhs) << endl;
+  }
+
+  // union max distributes over intersection
+  {
+    Term unionMaxAB = slv.mkTerm(BAG_UNION_MAX, {A, B});
+    Term lhs = slv.mkTerm(BAG_INTER_MIN, {unionMaxAB, C});
+    Term rhs = slv.mkTerm(BAG_UNION_MAX, {intersectionAC, intersectionBC});
+    Term theorem = slv.mkTerm(EQUAL, {lhs, rhs});
+    cout << "cvc5 reports: " << theorem.notTerm() << " is "
+         << slv.checkSatAssuming(theorem.notTerm()) << "." << endl;
+  }
+
+  // Verify emptbag is a subbag of any bag
+  {
+    Term emptybag = slv.mkEmptyBag(bag);
+    Term theorem = slv.mkTerm(BAG_SUBBAG, {emptybag, A});
+
+    cout << "cvc5 reports: " << theorem.notTerm() << " is "
+         << slv.checkSatAssuming(theorem.notTerm()) << "." << endl;
+  }
+
+  // find an element with multiplicity 4 in the disjoint union of
+  // ; {|"a", "a", "b", "b", "b"|} and {|"b", "c", "c"|}
+
+  {
+    Term one = slv.mkInteger(1);
+    Term two = slv.mkInteger(2);
+    Term three = slv.mkInteger(3);
+    Term four = slv.mkInteger(4);
+    Term a = slv.mkString("a");
+    Term b = slv.mkString("b");
+    Term c = slv.mkString("c");
+
+    Term bag_a_2 = slv.mkTerm(BAG_MAKE, {a, two});
+    Term bag_b_3 = slv.mkTerm(BAG_MAKE, {b, three});
+    Term bag_b_1 = slv.mkTerm(BAG_MAKE, {b, one});
+    Term bag_c_2 = slv.mkTerm(BAG_MAKE, {c, two});
+    Term bag_a_2_b_3 = slv.mkTerm(BAG_UNION_DISJOINT, {bag_a_2, bag_b_3});
+    Term bag_b_1_c_2 = slv.mkTerm(BAG_UNION_DISJOINT, {bag_b_1, bag_c_2});
+    Term union_disjoint =
+        slv.mkTerm(BAG_UNION_DISJOINT, {bag_a_2_b_3, bag_b_1_c_2});
+
+    Term count_x = slv.mkTerm(BAG_COUNT, {x, union_disjoint});
+    Term e = slv.mkTerm(EQUAL, {four, count_x});
+    Result result = slv.checkSatAssuming(e);
+
+    cout << "cvc5 reports: " << e << " is " << result << "." << endl;
+    if (result.isSat())
+    {
+      cout << x << ": " << slv.getValue(x) << endl;
+    }
+  }
+}
diff --git a/examples/api/java/Bags.java b/examples/api/java/Bags.java
new file mode 100644
index 000000000..f1c74ca97
--- /dev/null
+++ b/examples/api/java/Bags.java
@@ -0,0 +1,112 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * A simple demonstration of reasoning about bags with cvc5.
+ */
+
+import static io.github.cvc5.Kind.*;
+
+import io.github.cvc5.*;
+
+public class Bags
+{
+  public static void main(String args[]) throws CVC5ApiException
+
+  {
+    try (Solver slv = new Solver())
+    {
+      slv.setLogic("ALL");
+
+      // Produce models
+      slv.setOption("produce-models", "true");
+      slv.setOption("incremental", "true");
+
+      Sort bag = slv.mkBagSort(slv.getStringSort());
+      Term A = slv.mkConst(bag, "A");
+      Term B = slv.mkConst(bag, "B");
+      Term C = slv.mkConst(bag, "C");
+      Term x = slv.mkConst(slv.getStringSort(), "x");
+
+      Term intersectionAC = slv.mkTerm(BAG_INTER_MIN, new Term[] {A, C});
+      Term intersectionBC = slv.mkTerm(BAG_INTER_MIN, new Term[] {B, C});
+
+      // union disjoint does not distribute over intersection
+      {
+        Term unionDisjointAB = slv.mkTerm(BAG_UNION_DISJOINT, new Term[] {A, B});
+        Term lhs = slv.mkTerm(BAG_INTER_MIN, new Term[] {unionDisjointAB, C});
+        Term rhs = slv.mkTerm(BAG_UNION_DISJOINT, new Term[] {intersectionAC, intersectionBC});
+        Term guess = slv.mkTerm(EQUAL, new Term[] {lhs, rhs});
+
+        System.out.println("cvc5 reports: " + guess.notTerm() + " is "
+            + slv.checkSatAssuming(guess.notTerm()) + ".");
+
+        System.out.println(A + ": " + slv.getValue(A));
+        System.out.println(B + ": " + slv.getValue(B));
+        System.out.println(C + ": " + slv.getValue(C));
+        System.out.println(lhs + ": " + slv.getValue(lhs));
+        System.out.println(rhs + ": " + slv.getValue(rhs));
+      }
+
+      // union max distributes over intersection
+      {
+        Term unionMaxAB = slv.mkTerm(BAG_UNION_MAX, new Term[] {A, B});
+        Term lhs = slv.mkTerm(BAG_INTER_MIN, new Term[] {unionMaxAB, C});
+        Term rhs = slv.mkTerm(BAG_UNION_MAX, new Term[] {intersectionAC, intersectionBC});
+        Term theorem = slv.mkTerm(EQUAL, new Term[] {lhs, rhs});
+        System.out.println("cvc5 reports: " + theorem.notTerm() + " is "
+            + slv.checkSatAssuming(theorem.notTerm()) + ".");
+      }
+
+      // Verify emptbag is a subbag of any bag
+      {
+        Term emptybag = slv.mkEmptyBag(bag);
+        Term theorem = slv.mkTerm(BAG_SUBBAG, new Term[] {emptybag, A});
+
+        System.out.println("cvc5 reports: " + theorem.notTerm() + " is "
+            + slv.checkSatAssuming(theorem.notTerm()) + ".");
+      }
+
+      // find an element with multiplicity 4 in the disjoint union of
+      // ; {|"a", "a", "b", "b", "b"|} and {|"b", "c", "c"|}
+      {
+        Term one = slv.mkInteger(1);
+        Term two = slv.mkInteger(2);
+        Term three = slv.mkInteger(3);
+        Term four = slv.mkInteger(4);
+        Term a = slv.mkString("a");
+        Term b = slv.mkString("b");
+        Term c = slv.mkString("c");
+
+        Term bag_a_2 = slv.mkTerm(BAG_MAKE, new Term[] {a, two});
+        Term bag_b_3 = slv.mkTerm(BAG_MAKE, new Term[] {b, three});
+        Term bag_b_1 = slv.mkTerm(BAG_MAKE, new Term[] {b, one});
+        Term bag_c_2 = slv.mkTerm(BAG_MAKE, new Term[] {c, two});
+
+        Term bag_a_2_b_3 = slv.mkTerm(BAG_UNION_DISJOINT, new Term[] {bag_a_2, bag_b_3});
+
+        Term bag_b_1_c_2 = slv.mkTerm(BAG_UNION_DISJOINT, new Term[] {bag_b_1, bag_c_2});
+
+        Term union_disjoint = slv.mkTerm(BAG_UNION_DISJOINT, new Term[] {bag_a_2_b_3, bag_b_1_c_2});
+
+        Term count_x = slv.mkTerm(BAG_COUNT, new Term[] {x, union_disjoint});
+        Term e = slv.mkTerm(EQUAL, new Term[] {four, count_x});
+        Result result = slv.checkSatAssuming(e);
+
+        System.out.println("cvc5 reports: " + e + " is " + result + ".");
+        if (result.isSat())
+        {
+          System.out.println(x + ": " + slv.getValue(x));
+        }
+      }
+    }
+  }
+}
\ No newline at end of file
diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java
index 2abbc35fe..72aaadc4b 100644
--- a/examples/api/java/BitVectors.java
+++ b/examples/api/java/BitVectors.java
@@ -88,8 +88,7 @@ public class BitVectors
 
       System.out.println(" Check sat assuming: " + new_x_eq_new_x_.notTerm());
       System.out.println(" Expect UNSAT. ");
-      System.out.println(
-          " cvc5: " + slv.checkSatAssuming(new_x_eq_new_x_.notTerm()));
+      System.out.println(" cvc5: " + slv.checkSatAssuming(new_x_eq_new_x_.notTerm()));
       System.out.println(" Popping context. ");
       slv.pop();
 
@@ -105,8 +104,7 @@ public class BitVectors
 
       System.out.println(" Check sat assuming: " + new_x_eq_new_x_.notTerm());
       System.out.println(" Expect UNSAT. ");
-      System.out.println(
-          " cvc5: " + slv.checkSatAssuming(new_x_eq_new_x_.notTerm()));
+      System.out.println(" cvc5: " + slv.checkSatAssuming(new_x_eq_new_x_.notTerm()));
 
       Term x_neq_x = slv.mkTerm(Kind.EQUAL, x, x).notTerm();
       Term[] v = new Term[] {new_x_eq_new_x_, x_neq_x};
diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt
index bd4eb179a..159d0e928 100644
--- a/examples/api/java/CMakeLists.txt
+++ b/examples/api/java/CMakeLists.txt
@@ -14,6 +14,7 @@
 ##
 
 set(EXAMPLES_API_JAVA
+   Bags
    BitVectors
    BitVectorsAndArrays
    Combination
diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java
index 60a9e803b..0754fd707 100644
--- a/examples/api/java/Combination.java
+++ b/examples/api/java/Combination.java
@@ -86,8 +86,7 @@ public class Combination
       System.out.println("Given the following assertions:\n" + assertions + "\n");
 
       System.out.println("Prove x /= y is entailed. \n"
-          + "cvc5: " + slv.checkSatAssuming(slv.mkTerm(Kind.EQUAL, x, y))
-          + ".\n");
+          + "cvc5: " + slv.checkSatAssuming(slv.mkTerm(Kind.EQUAL, x, y)) + ".\n");
 
       System.out.println("Call checkSat to show that the assertions are satisfiable. \n"
           + "cvc5: " + slv.checkSat() + ".\n");
diff --git a/examples/api/java/HelloWorld.java b/examples/api/java/HelloWorld.java
index 7cef12966..1b4499950 100644
--- a/examples/api/java/HelloWorld.java
+++ b/examples/api/java/HelloWorld.java
@@ -23,8 +23,7 @@ public class HelloWorld
     {
       Term helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!");
 
-      System.out.println(
-          helloworld + " is " + slv.checkSatAssuming(helloworld));
+      System.out.println(helloworld + " is " + slv.checkSatAssuming(helloworld));
     }
   }
 }
diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java
index 7ba565ff3..fe9d6b4b7 100644
--- a/examples/api/java/LinearArith.java
+++ b/examples/api/java/LinearArith.java
@@ -57,8 +57,8 @@ public class LinearArith
       Term diff_leq_two_thirds = slv.mkTerm(Kind.LEQ, diff, two_thirds);
       System.out.println("Prove that " + diff_leq_two_thirds + " with cvc5.");
       System.out.println("cvc5 should report UNSAT.");
-      System.out.println("Result from cvc5 is: "
-          + slv.checkSatAssuming(diff_leq_two_thirds.notTerm()));
+      System.out.println(
+          "Result from cvc5 is: " + slv.checkSatAssuming(diff_leq_two_thirds.notTerm()));
       slv.pop();
 
       System.out.println();
diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java
index a4b568ccd..f7fbf4bf3 100644
--- a/examples/api/java/Relations.java
+++ b/examples/api/java/Relations.java
@@ -113,7 +113,7 @@ public class Relations
 
       // (assert (forall ((x Person)) (not (set.member (tuple x x) ancestor))))
       Term x = solver.mkVar(personSort, "x");
-      Term xxTuple = solver.mkTuple(new Sort[]{personSort, personSort}, new Term[] {x, x});
+      Term xxTuple = solver.mkTuple(new Sort[] {personSort, personSort}, new Term[] {x, x});
       Term member = solver.mkTerm(SET_MEMBER, xxTuple, ancestor);
       Term notMember = solver.mkTerm(NOT, member);
 
diff --git a/examples/api/java/Sets.java b/examples/api/java/Sets.java
index 6002c0e69..1a2cff031 100644
--- a/examples/api/java/Sets.java
+++ b/examples/api/java/Sets.java
@@ -50,8 +50,8 @@ public class Sets
 
         Term theorem = slv.mkTerm(EQUAL, lhs, rhs);
 
-        System.out.println("cvc5 reports: " + theorem + " is "
-            + slv.checkSatAssuming(theorem.notTerm()) + ".");
+        System.out.println(
+            "cvc5 reports: " + theorem + " is " + slv.checkSatAssuming(theorem.notTerm()) + ".");
       }
 
       // Verify set.empty is a subset of any set
@@ -61,8 +61,8 @@ public class Sets
 
         Term theorem = slv.mkTerm(SET_SUBSET, emptyset, A);
 
-        System.out.println("cvc5 reports: " + theorem + " is "
-            + slv.checkSatAssuming(theorem.notTerm()) + ".");
+        System.out.println(
+            "cvc5 reports: " + theorem + " is " + slv.checkSatAssuming(theorem.notTerm()) + ".");
       }
 
       // Find me an element in {1, 2} intersection {2, 3}, if there is one.
diff --git a/examples/api/java/Utils.java b/examples/api/java/Utils.java
index 9a2054d86..3ea56c55f 100644
--- a/examples/api/java/Utils.java
+++ b/examples/api/java/Utils.java
@@ -13,13 +13,12 @@
  * Utility methods.
  */
 
-import java.util.ArrayList;
-import java.util.List;
-
 import io.github.cvc5.CVC5ApiException;
 import io.github.cvc5.Kind;
 import io.github.cvc5.Sort;
 import io.github.cvc5.Term;
+import java.util.ArrayList;
+import java.util.List;
 
 public class Utils
 {
@@ -46,8 +45,7 @@ public class Utils
       {
         ss.append(' ');
       }
-      ss.append('(').append(params[i]).append(' ').append(params[i].getSort())
-          .append(')');
+      ss.append('(').append(params[i]).append(' ').append(params[i].getSort()).append(')');
     }
     ss.append(") ").append(sort).append(' ').append(body).append(')');
     return ss.toString();
@@ -59,8 +57,7 @@ public class Utils
    * @param terms the terms for which the synthesis solutions were retrieved
    * @param sols the synthesis solutions of the given terms
    */
-  public static void printSynthSolutions(Term[] terms, Term[] sols)
-      throws CVC5ApiException
+  public static void printSynthSolutions(Term[] terms, Term[] sols) throws CVC5ApiException
   {
     System.out.println('(');
     for (int i = 0; i < terms.length; ++i)
@@ -75,8 +72,7 @@ public class Utils
         }
         body = sols[i].getChild(1);
       }
-      System.out.println("  "
-          + defineFunToString(terms[i], params.toArray(new Term[0]), body));
+      System.out.println("  " + defineFunToString(terms[i], params.toArray(new Term[0]), body));
     }
     System.out.println(')');
   }
diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt
index d6233f0c5..f03db7c54 100644
--- a/examples/api/python/CMakeLists.txt
+++ b/examples/api/python/CMakeLists.txt
@@ -14,6 +14,7 @@
 ##
 
 set(EXAMPLES_API_PYTHON
+  bags
   bitvectors_and_arrays
   bitvectors
   combination
diff --git a/examples/api/python/bags.py b/examples/api/python/bags.py
new file mode 100644
index 000000000..9172a97f5
--- /dev/null
+++ b/examples/api/python/bags.py
@@ -0,0 +1,86 @@
+#!/usr/bin/env python
+###############################################################################
+# Top contributors (to current version):
+#   Mudathir Mohamed
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+# in the top-level source directory and their institutional affiliations.
+# All rights reserved.  See the file COPYING in the top-level source
+# directory for licensing information.
+# #############################################################################
+#
+# A simple demonstration of reasoning about bags.
+##
+
+import cvc5
+from cvc5 import Kind
+
+if __name__ == "__main__":
+    slv = cvc5.Solver()
+    slv.setLogic("ALL")
+
+    # Produce models
+    slv.setOption("produce-models", "true")
+    slv.setOption("incremental", "true")
+
+    bag = slv.mkBagSort(slv.getStringSort())
+    A = slv.mkConst(bag, "A")
+    B = slv.mkConst(bag, "B")
+    C = slv.mkConst(bag, "C")
+    x = slv.mkConst(slv.getStringSort(), "x")
+
+    intersectionAC = slv.mkTerm(Kind.BagInterMin, A, C)
+    intersectionBC = slv.mkTerm(Kind.BagInterMin, B, C)
+
+    # union disjoint does not distribute over intersection
+    unionDisjointAB = slv.mkTerm(Kind.BagUnionDisjoint, A, B)
+    lhs = slv.mkTerm(Kind.BagInterMin, unionDisjointAB, C)
+    rhs = slv.mkTerm(Kind.BagUnionDisjoint, intersectionAC, intersectionBC)
+    guess = slv.mkTerm(Kind.Equal, lhs, rhs)
+    print("cvc5 reports: {} is {}".format(guess.notTerm(), slv.checkSatAssuming(guess.notTerm())))
+
+    print("{}: {}".format(A, slv.getValue(A)))
+    print("{}: {}".format(B, slv.getValue(B)))
+    print("{}: {}".format(C, slv.getValue(C)))
+    print("{}: {}".format(lhs, slv.getValue(lhs)))
+    print("{}: {}".format(rhs, slv.getValue(rhs)))
+
+    # union max distributes over intersection
+    unionMaxAB = slv.mkTerm(Kind.BagUnionMax, A, B)
+    lhs = slv.mkTerm(Kind.BagInterMin, unionMaxAB, C)
+    rhs = slv.mkTerm(Kind.BagUnionMax, intersectionAC, intersectionBC)
+    theorem = slv.mkTerm(Kind.Equal, lhs, rhs)
+    print("cvc5 reports: {} is {}.".format(theorem.notTerm(), slv.checkSatAssuming(theorem.notTerm())))
+
+    # Verify emptbag is a subbag of any bag
+    emptybag = slv.mkEmptyBag(bag)
+    theorem = slv.mkTerm(Kind.BagSubbag, emptybag, A)
+    print("cvc5 reports: {} is {}.".format(theorem.notTerm(), slv.checkSatAssuming(theorem.notTerm())))
+
+    # find an element with multiplicity 4 in the disjoint union of
+    #  {|"a", "a", "b", "b", "b"|} and {|"b", "c", "c"|}
+    one = slv.mkInteger(1)
+    two = slv.mkInteger(2)
+    three = slv.mkInteger(3)
+    four = slv.mkInteger(4)
+    a = slv.mkString("a")
+    b = slv.mkString("b")
+    c = slv.mkString("c")
+
+    bag_a_2 = slv.mkTerm(Kind.BagMake, a, two)
+    bag_b_3 = slv.mkTerm(Kind.BagMake, b, three)
+    bag_b_1 = slv.mkTerm(Kind.BagMake, b, one)
+    bag_c_2 = slv.mkTerm(Kind.BagMake, c, two)
+    bag_a_2_b_3 = slv.mkTerm(Kind.BagUnionDisjoint, bag_a_2, bag_b_3)
+    bag_b_1_c_2 = slv.mkTerm(Kind.BagUnionDisjoint, bag_b_1, bag_c_2)
+    UnionDisjoint = slv.mkTerm(Kind.BagUnionDisjoint, bag_a_2_b_3, bag_b_1_c_2)
+
+    count_x = slv.mkTerm(Kind.BagCount, x, UnionDisjoint)
+    e = slv.mkTerm(Kind.Equal, four, count_x)
+    result = slv.checkSatAssuming(e)
+
+    print("cvc5 reports: {} is {}.".format(e, result))
+    if result.isSat():
+        print("{}: {} ".format(x, slv.getValue(x)))