Add bags.rst (#8432)

diff --git a/docs/theories/bags.rst b/docs/theories/bags.rst
new file mode 100644 (file)
index 0000000..a458b44
--- /dev/null
+++ b/docs/theories/bags.rst
@@ -0,0 +1,86 @@
+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::api::Solver solver` object.
+
++----------------------+----------------------------------------------+-------------------------------------------------------------------------+
+|                      | SMTLIB language                              | C++ API                                                                 |
++----------------------+----------------------------------------------+-------------------------------------------------------------------------+
+| Logic String         | ``(set-logic ALL)``                          | ``solver.setLogic("ALL");``                                             |
++----------------------+----------------------------------------------+-------------------------------------------------------------------------+
+| Sort                 | ``(Bag <Sort>)``                             | ``solver.mkBagSort(cvc5::api::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) :math:`m` can be defined as a function from the domain of its elements
+to the set of natural numbers (i.e., :math:`m : D \rightarrow \mathbb{N}`),
+where :math:`m(e)` represents the multiplicity of element :math:`e` in the bag :math:`m`.
+
+The semantics of supported bag operators is given in the table below.
+
++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+
+| Bag operator                                        | cvc5 operator           | Semantics                                                                          |
++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+
+| union disjoint :math:`m_1 \uplus m_2`               | bag.union_disjoint      | :math:`\forall e. \; (m_1 \uplus m_2)(e) = m_1(e) + m_2 (e)`                       |
++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+
+| union max :math:`m_1 \cup m_2`                      | bag.union_max           | :math:`\forall e. \; (m_1 \cup m_2)(e) = max(m_1(e), m_2 (e))`                     |
++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+
+| intersection :math:`m_1 \cap m_2`                   | bag.inter_min           | :math:`\forall e. \; (m_1 \cap m_2)(e) = min(m_1(e), m_2 (e))`                     |
++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+
+| difference subtract :math:`m_1 \setminus m_2`       | bag.difference_subtract | :math:`\forall e. \; (m_1 \setminus m_2)(e) = max(m_1(e) - m_2 (e), 0)`            |
++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+
+| difference remove :math:`m_1 \setminus\setminus m_2`| bag.difference_remove   | :math:`\forall e. \; (m_1 \setminus\setminus m_2)(e) = ite(m_2(e) = 0, m_1(e), 0)` |
++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+
+| duplicate elimination  :math:`\delta(m)`            | bag.duplicate_removal   | :math:`\forall e. \; (\delta(m))(e) = ite(1 \leq m(e), 1, 0)`                      |
++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+
+| subbag :math:`m_1 \subseteq m_2`                    | bag.subbag              | :math:`\forall e. \; m_1(e) \leq m_2(e)`                                           |
++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+
+| equality :math:`m_1 = m_2`                          | =                       | :math:`\forall e. \; m_1(e) = m_2(e)`                                              |
++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+
+| membership :math:`e \in m`                          | bag.member              | :math:`m(e) \geq 1`                                                                |
++-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+
+
+Below is a more extensive example on how to use finite bags:
+
+.. api-examples::
+    <examples>/api/smtlib/bags.smt2
+

diff --git a/examples/api/smtlib/bags.smt2 b/examples/api/smtlib/bags.smt2
new file mode 100644 (file)
index 0000000..785a8d3
--- /dev/null
+++ b/examples/api/smtlib/bags.smt2
@@ -0,0 +1,47 @@
+(set-logic ALL)
+
+(set-option :produce-models true)
+(set-option :incremental true)
+
+(declare-const A (Bag String))
+(declare-const B (Bag String))
+(declare-const C (Bag String))
+(declare-const x String)
+
+; union disjoint does not distribute over intersection
+; sat
+(check-sat-assuming
+ ((distinct
+   (bag.inter_min (bag.union_disjoint A B) C)
+   (bag.union_disjoint (bag.inter_min A C) (bag.inter_min B C)))))
+
+
+(get-value (A))
+(get-value (B))
+(get-value (C))
+(get-value ((bag.inter_min (bag.union_disjoint A B) C)))
+(get-value ((bag.union_disjoint (bag.inter_min A C) (bag.inter_min B C))))
+
+; union max distributes over intersection
+; unsat
+(check-sat-assuming
+ ((distinct
+   (bag.inter_min (bag.union_max A B) C)
+   (bag.union_max (bag.inter_min A C) (bag.inter_min B C)))))
+
+; Verify emptbag is a subbag of any bag
+; unsat
+(check-sat-assuming
+ ((not (bag.subbag (as bag.empty (Bag String)) A))))
+
+; find an element with multiplicity 4 in the disjoint union of
+; {|"a", "a", "b", "b", "b"|} and {|"b", "c", "c"|}
+(check-sat-assuming
+ ((= 4
+     (bag.count x
+                (bag.union_disjoint
+                 (bag.union_disjoint (bag "a" 2) (bag "b" 3))
+                 (bag.union_disjoint (bag "b" 1) (bag "c" 2)))))))
+
+; x is "b"
+(get-value (x))