Skip to content

Commit

Permalink
Merge remote-tracking branch 'upstream/master'
Browse files Browse the repository at this point in the history
  • Loading branch information
@Ouyancheng
Ouyancheng committed Mar 29, 2022
2 parents a8219c8 + 3d21e43 commit 09ecd70
Show file tree
Hide file tree
Showing 75 changed files with 1,361 additions and 632 deletions.
3 changes: 2 additions & 1 deletion .github/workflows/ci.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,10 +49,11 @@ jobs:

- name: ubuntu:production-dbg
os: ubuntu-18.04
config: production --auto-download --assertions --tracing --unit-testing --java-bindings --editline
config: production --auto-download --assertions --tracing --unit-testing --all-bindings --editline
cache-key: dbg
exclude_regress: 3-4
run_regression_args: --tester base --tester model --tester synth --tester abduct --tester proof --tester dump
python-bindings: true

- name: ubuntu:production-dbg-clang
os: ubuntu-latest
Expand Down
86 changes: 86 additions & 0 deletions docs/theories/bags.rst
View file
Original file line number Diff line number Diff line change
@@ -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

4 changes: 2 additions & 2 deletions examples/api/python/floating_point.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@
##

import cvc5
from cvc5 import Kind
from cvc5 import Kind, RoundingMode

if __name__ == "__main__":
slv = cvc5.Solver()
Expand All @@ -29,7 +29,7 @@
fp32 = slv.mkFloatingPointSort(8, 24)

# the standard rounding mode
rm = slv.mkRoundingMode(cvc5.RoundNearestTiesToEven)
rm = slv.mkRoundingMode(RoundingMode.RoundNearestTiesToEven)

# create a few single-precision variables
x = slv.mkConst(fp32, 'x')
Expand Down
47 changes: 47 additions & 0 deletions examples/api/smtlib/bags.smt2
View file
Original file line number Diff line number Diff line change
@@ -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))
Loading

0 comments on commit 09ecd70

Please sign in to comment.