From: mudathirmahgoub Date: Tue, 29 Mar 2022 17:32:37 +0000 (-0500) Subject: Add bags.rst (#8432) X-Git-Tag: cvc5-1.0.0~140 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2cbeb0d7b09816c2364d61616b88bdabfd90029e;p=cvc5.git Add bags.rst (#8432) --- diff --git a/docs/theories/bags.rst b/docs/theories/bags.rst new file mode 100644 index 000000000..a458b44b2 --- /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 )`` | ``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:: + /api/smtlib/bags.smt2 + diff --git a/examples/api/smtlib/bags.smt2 b/examples/api/smtlib/bags.smt2 new file mode 100644 index 000000000..785a8d379 --- /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))