projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 59d4deb)
docs: Fix mkTerm calls in theory documentation. (#8567)
authorMathias Preiner <mathias.preiner@gmail.com>
Tue, 5 Apr 2022 02:14:37 +0000 (19:14 -0700)
committerGitHub <noreply@github.com>
Tue, 5 Apr 2022 02:14:37 +0000 (02:14 +0000)
docs/theories/bags.rst patch | blob | history
docs/theories/separation-logic.rst patch | blob | history
docs/theories/sequences.rst patch | blob | history
docs/theories/sets-and-relations.rst patch | blob | history

diff --git a/docs/theories/bags.rst b/docs/theories/bags.rst
index 6666015aeb0470d3dc7d7919a9aac6db8368595d..5978851627af8219a33ae9b43f620fa0ef0d2f6b 100644 (file)
--- a/docs/theories/bags.rst
+++ b/docs/theories/bags.rst
@@ -23,28 +23,28 @@ a `cvc5::Solver solver` object.
 +----------------------+----------------------------------------------+-------------------------------------------------------------------------+
 | Union disjoint       | ``(bag.union_disjoint X Y)``                 | ``Term Y = solver.mkConst(s, "Y");``                                    |
 |                      |                                              |                                                                         |
-|                      |                                              | ``Term t = solver.mkTerm(Kind::BAG_UNION_DISJOINT, X, 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);``                  |
+|                      |                                              | ``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);``                  |
+| 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);``        |
+| 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);``             |
+| 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);``                     |
+|                      |                                              | ``Term t = solver.mkTerm(Kind::BAG_MEMBER, {x, X});``                   |
 +----------------------+----------------------------------------------+-------------------------------------------------------------------------+
-| Subbag               | ``(bag.subbag X Y)``                         | ``Term t = solver.mkTerm(Kind::BAG_SUBBAG, X, Y);``                     |
+| 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));``              |
+|                      |                                              |            ``{solver.mkString("a"), solver.mkInteger(1)});``            |
 +----------------------+----------------------------------------------+-------------------------------------------------------------------------+
 
 
diff --git a/docs/theories/separation-logic.rst b/docs/theories/separation-logic.rst
index 55811ed25f51f2edb781ab0ebd8020936827e4e9..2ae43a7c23518e3d0af23278d2194cf46245fc2a 100644 (file)
--- a/docs/theories/separation-logic.rst
+++ b/docs/theories/separation-logic.rst
@@ -80,11 +80,11 @@ a :cpp:class:`cvc5::Solver` object.
 |                      |                                              |                                                                    |
 |                      |                                              | where ``x`` and ``y`` are of sort ``<Sort_1>`` and ``<Sort_2>``    |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
-| Points-To            | ``(pto x y)``                                | ``solver.mkTerm(Kind::SEP_PTO, x, y);``                            |
+| Points-To            | ``(pto x y)``                                | ``solver.mkTerm(Kind::SEP_PTO, {x, y});``                          |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
 | Separation Star      | ``(sep c1 .. cn)``                           | ``solver.mkTerm(Kind::SEP_STAR, {c1, ..., cn});``                  |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
-| Magic Wand           | ``(wand c1 c1)``                             | ``solver.mkTerm(Kind::SEP_WAND, c1, c2);``                         |
+| Magic Wand           | ``(wand c1 c1)``                             | ``solver.mkTerm(Kind::SEP_WAND, {c1, c2});``                       |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
 | Nil Element          | ``(as sep.nil <Sort>)``                      | ``solver.mkSepNil(cvc5::Sort sort);``                              |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
diff --git a/docs/theories/sequences.rst b/docs/theories/sequences.rst
index cb6806fa1d7f14f7aa9b3752618713c945317a77..bc6148befd0469330a56a5e5fa0a552004ae2fdb 100644 (file)
--- a/docs/theories/sequences.rst
+++ b/docs/theories/sequences.rst
@@ -116,35 +116,35 @@ a ``cvc5::api::Solver solver`` object.
 |                      |                                              |                                                                    |
 |                      |                                              | ``Term t = solver.mkEmptySequence(intSort);``                      |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
-| Unit sequence        | ``(seq.unit 1)``                             | ``Term t = solver.mkTerm(Kind::SEQ_UNIT, solver.mkInteger(1));``   |
+| Unit sequence        | ``(seq.unit 1)``                             | ``Term t = solver.mkTerm(Kind::SEQ_UNIT, {solver.mkInteger(1)});`` |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
-| Sequence length      | ``(seq.len X)``                              | ``Term t = solver.mkTerm(Kind::SEQ_LENGTH, X);``                   |
+| Sequence length      | ``(seq.len X)``                              | ``Term t = solver.mkTerm(Kind::SEQ_LENGTH, {X});``                 |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
-| Element access       | ``(seq.nth X i)``                            | ``Term t = solver.mkTerm(Kind::SEQ_NTH, X, i);``                   |
+| Element access       | ``(seq.nth X i)``                            | ``Term t = solver.mkTerm(Kind::SEQ_NTH, {X, i});``                 |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
-| Element update       | ``(seq.update X i Y)``                       | ``Term t = solver.mkTerm(Kind::SEQ_UPDATE, X, i, Y);``             |
+| Element update       | ``(seq.update X i Y)``                       | ``Term t = solver.mkTerm(Kind::SEQ_UPDATE, {X, i, Y});``           |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
-| Extraction           | ``(seq.extract X i j)``                      | ``Term t = solver.mkTerm(Kind::SEQ_EXTRACT, X, i, j);``            |
+| Extraction           | ``(seq.extract X i j)``                      | ``Term t = solver.mkTerm(Kind::SEQ_EXTRACT, {X, i, j});``          |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
-| Concatenation        | ``(seq.++ X Y)``                             | ``Term t = solver.mkTerm(Kind::SEQ_CONCAT, X, Y);``                |
+| Concatenation        | ``(seq.++ X Y)``                             | ``Term t = solver.mkTerm(Kind::SEQ_CONCAT, {X, Y});``              |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
-| Sub-sequence with    | ``(seq.at X i)``                             | ``Term t = solver.mkTerm(Kind::SEQ_AT, X, i);``                    |
+| Sub-sequence with    | ``(seq.at X i)``                             | ``Term t = solver.mkTerm(Kind::SEQ_AT, {X, i});``                  |
 | single element       |                                              |                                                                    |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
-| Sequence containment | ``(seq.contains X Y)``                       | ``Term t = solver.mkTerm(Kind::SEQ_CONTAINS, X, Y);``              |
+| Sequence containment | ``(seq.contains X Y)``                       | ``Term t = solver.mkTerm(Kind::SEQ_CONTAINS, {X, Y});``            |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
-| Sequence indexof     | ``(seq.indexof X Y i)``                      | ``Term t = solver.mkTerm(Kind::SEQ_INDEXOF, X, Y, i);``            |
+| Sequence indexof     | ``(seq.indexof X Y i)``                      | ``Term t = solver.mkTerm(Kind::SEQ_INDEXOF, {X, Y, i});``          |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
-| Sub-sequence replace | ``(seq.replace X Y Z)``                      | ``Term t = solver.mkTerm(Kind::SEQ_REPLACE, X, Y, Z);``            |
+| Sub-sequence replace | ``(seq.replace X Y Z)``                      | ``Term t = solver.mkTerm(Kind::SEQ_REPLACE, {X, Y, Z});``          |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
-| Sub-sequence         | ``(seq.replace_all X Y Z)``                  | ``Term t = solver.mkTerm(Kind::SEQ_REPLACE_ALL, X, Y, Z);``        |
+| Sub-sequence         | ``(seq.replace_all X Y Z)``                  | ``Term t = solver.mkTerm(Kind::SEQ_REPLACE_ALL, {X, Y, Z});``      |
 | replace all          |                                              |                                                                    |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
-| Sequence reverse     | ``(seq.rev X)``                              | ``Term t = solver.mkTerm(Kind::SEQ_REV, X);``                      |
+| Sequence reverse     | ``(seq.rev X)``                              | ``Term t = solver.mkTerm(Kind::SEQ_REV, {X});``                    |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
-| Sequence prefix of   | ``(seq.prefixof X Y)``                       | ``Term t = solver.mkTerm(Kind::SEQ_PREFIX, X, Y);``                |
+| Sequence prefix of   | ``(seq.prefixof X Y)``                       | ``Term t = solver.mkTerm(Kind::SEQ_PREFIX, {X, Y});``              |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
-| Sequence suffix of   | ``(seq.suffixof X Y)``                       | ``Term t = solver.mkTerm(Kind::SEQ_SUFFIX, X, Y);``                |
+| Sequence suffix of   | ``(seq.suffixof X Y)``                       | ``Term t = solver.mkTerm(Kind::SEQ_SUFFIX, {X, Y});``              |
 +----------------------+----------------------------------------------+--------------------------------------------------------------------+
 
 Examples
diff --git a/docs/theories/sets-and-relations.rst b/docs/theories/sets-and-relations.rst
index 88c38aa27b0c922fdf13cbefb863f30dcd5773ec..f6e27732917a8e72ca249499d4ea6caafc45cb29 100644 (file)
--- a/docs/theories/sets-and-relations.rst
+++ b/docs/theories/sets-and-relations.rst
@@ -12,53 +12,53 @@ functions and predicates.  More details can be found in :cite:`BansalBRT17`.
 For the C++ API examples in the table below, we assume that we have created
 a `cvc5::Solver solver` object.
 
-+----------------------+----------------------------------------------+-------------------------------------------------------------------------+
-|                      | SMTLIB language                              | C++ API                                                                 |
-+----------------------+----------------------------------------------+-------------------------------------------------------------------------+
-| Logic String         | append `FS` for finite sets                  | append `FS` for finite sets                                             |
-|                      |                                              |                                                                         |
-|                      | ``(set-logic QF_UFLIAFS)``                   | ``solver.setLogic("QF_UFLIAFS");``                                      |
-+----------------------+----------------------------------------------+-------------------------------------------------------------------------+
-| Sort                 | ``(Set <Sort>)``                             | ``solver.mkSetSort(cvc5::Sort elementSort);``                           |
-+----------------------+----------------------------------------------+-------------------------------------------------------------------------+
-| Constants            | ``(declare-const X (Set Int)``               | ``Sort s = solver.mkSetSort(solver.getIntegerSort());``                 |
-|                      |                                              |                                                                         |
-|                      |                                              | ``Term X = solver.mkConst(s, "X");``                                    |
-+----------------------+----------------------------------------------+-------------------------------------------------------------------------+
-| Union                | ``(set.union X Y)``                          | ``Term Y = solver.mkConst(s, "Y");``                                    |
-|                      |                                              |                                                                         |
-|                      |                                              | ``Term t = solver.mkTerm(Kind::SET_UNION, X, Y);``                      |
-+----------------------+----------------------------------------------+-------------------------------------------------------------------------+
-| Intersection         | ``(set.inter X Y)``                          | ``Term t = solver.mkTerm(Kind::SET_INTER, X, Y);``                      |
-+----------------------+----------------------------------------------+-------------------------------------------------------------------------+
-| Minus                | ``(set.minus X Y)``                          | ``Term t = solver.mkTerm(Kind::SET_MINUS, X, Y);``                      |
-+----------------------+----------------------------------------------+-------------------------------------------------------------------------+
-| Membership           | ``(set.member x X)``                         | ``Term x = solver.mkConst(solver.getIntegerSort(), "x");``              |
-|                      |                                              |                                                                         |
-|                      |                                              | ``Term t = solver.mkTerm(Kind::SET_MEMBER, x, X);``                     |
-+----------------------+----------------------------------------------+-------------------------------------------------------------------------+
-| Subset               | ``(set.subset X Y)``                         | ``Term t = solver.mkTerm(Kind::SET_SUBSET, X, Y);``                     |
-+----------------------+----------------------------------------------+-------------------------------------------------------------------------+
-| Emptyset             | ``(as set.empty (Set Int)``                  | ``Term t = solver.mkEmptySet(s);``                                      |
-+----------------------+----------------------------------------------+-------------------------------------------------------------------------+
-| Singleton Set        | ``(set.singleton 1)``                        | ``Term t = solver.mkTerm(Kind::SET_SINGLETON, solver.mkInteger(1));``   |
-+----------------------+----------------------------------------------+-------------------------------------------------------------------------+
-| Cardinality          | ``(set.card X)``                             | ``Term t = solver.mkTerm(Kind::SET_CARD, X);``                          |
-+----------------------+----------------------------------------------+-------------------------------------------------------------------------+
-| Insert / Finite Sets | ``(set.insert 1 2 3 (set.singleton 4))``     | ``Term one = solver.mkInteger(1);``                                     |
-|                      |                                              |                                                                         |
-|                      |                                              | ``Term two = solver.mkInteger(2);``                                     |
-|                      |                                              |                                                                         |
-|                      |                                              | ``Term three = solver.mkInteger(3);``                                   |
-|                      |                                              |                                                                         |
-|                      |                                              | ``Term sgl = solver.mkTerm(Kind::SET_SINGLETON, solver.mkInteger(4));`` |
-|                      |                                              |                                                                         |
-|                      |                                              | ``Term t = solver.mkTerm(Kind::SET_INSERT, {one, two, three, sgl});``   |
-+----------------------+----------------------------------------------+-------------------------------------------------------------------------+
-| Complement           | ``(set.complement X)``                       | ``Term t = solver.mkTerm(Kind::SET_COMPLEMENT, X);``                    |
-+----------------------+----------------------------------------------+-------------------------------------------------------------------------+
-| Universe Set         | ``(as set.universe (Set Int))``              | ``Term t = solver.mkUniverseSet(s);``                                   |
-+----------------------+----------------------------------------------+-------------------------------------------------------------------------+
++----------------------+----------------------------------------------+---------------------------------------------------------------------------+
+|                      | SMTLIB language                              | C++ API                                                                   |
++----------------------+----------------------------------------------+---------------------------------------------------------------------------+
+| Logic String         | append `FS` for finite sets                  | append `FS` for finite sets                                               |
+|                      |                                              |                                                                           |
+|                      | ``(set-logic QF_UFLIAFS)``                   | ``solver.setLogic("QF_UFLIAFS");``                                        |
++----------------------+----------------------------------------------+---------------------------------------------------------------------------+
+| Sort                 | ``(Set <Sort>)``                             | ``solver.mkSetSort(cvc5::Sort elementSort);``                             |
++----------------------+----------------------------------------------+---------------------------------------------------------------------------+
+| Constants            | ``(declare-const X (Set Int)``               | ``Sort s = solver.mkSetSort(solver.getIntegerSort());``                   |
+|                      |                                              |                                                                           |
+|                      |                                              | ``Term X = solver.mkConst(s, "X");``                                      |
++----------------------+----------------------------------------------+---------------------------------------------------------------------------+
+| Union                | ``(set.union X Y)``                          | ``Term Y = solver.mkConst(s, "Y");``                                      |
+|                      |                                              |                                                                           |
+|                      |                                              | ``Term t = solver.mkTerm(Kind::SET_UNION, {X, Y});``                      |
++----------------------+----------------------------------------------+---------------------------------------------------------------------------+
+| Intersection         | ``(set.inter X Y)``                          | ``Term t = solver.mkTerm(Kind::SET_INTER, {X, Y});``                      |
++----------------------+----------------------------------------------+---------------------------------------------------------------------------+
+| Minus                | ``(set.minus X Y)``                          | ``Term t = solver.mkTerm(Kind::SET_MINUS, {X, Y});``                      |
++----------------------+----------------------------------------------+---------------------------------------------------------------------------+
+| Membership           | ``(set.member x X)``                         | ``Term x = solver.mkConst(solver.getIntegerSort(), "x");``                |
+|                      |                                              |                                                                           |
+|                      |                                              | ``Term t = solver.mkTerm(Kind::SET_MEMBER, {x, X});``                     |
++----------------------+----------------------------------------------+---------------------------------------------------------------------------+
+| Subset               | ``(set.subset X Y)``                         | ``Term t = solver.mkTerm(Kind::SET_SUBSET, {X, Y});``                     |
++----------------------+----------------------------------------------+---------------------------------------------------------------------------+
+| Emptyset             | ``(as set.empty (Set Int)``                  | ``Term t = solver.mkEmptySet(s);``                                        |
++----------------------+----------------------------------------------+---------------------------------------------------------------------------+
+| Singleton Set        | ``(set.singleton 1)``                        | ``Term t = solver.mkTerm(Kind::SET_SINGLETON, {solver.mkInteger(1)});``   |
++----------------------+----------------------------------------------+---------------------------------------------------------------------------+
+| Cardinality          | ``(set.card X)``                             | ``Term t = solver.mkTerm(Kind::SET_CARD, {X});``                          |
++----------------------+----------------------------------------------+---------------------------------------------------------------------------+
+| Insert / Finite Sets | ``(set.insert 1 2 3 (set.singleton 4))``     | ``Term one = solver.mkInteger(1);``                                       |
+|                      |                                              |                                                                           |
+|                      |                                              | ``Term two = solver.mkInteger(2);``                                       |
+|                      |                                              |                                                                           |
+|                      |                                              | ``Term three = solver.mkInteger(3);``                                     |
+|                      |                                              |                                                                           |
+|                      |                                              | ``Term sgl = solver.mkTerm(Kind::SET_SINGLETON, {solver.mkInteger(4)});`` |
+|                      |                                              |                                                                           |
+|                      |                                              | ``Term t = solver.mkTerm(Kind::SET_INSERT, {one, two, three, sgl});``     |
++----------------------+----------------------------------------------+---------------------------------------------------------------------------+
+| Complement           | ``(set.complement X)``                       | ``Term t = solver.mkTerm(Kind::SET_COMPLEMENT, {X});``                    |
++----------------------+----------------------------------------------+---------------------------------------------------------------------------+
+| Universe Set         | ``(as set.universe (Set Int))``              | ``Term t = solver.mkUniverseSet(s);``                                     |
++----------------------+----------------------------------------------+---------------------------------------------------------------------------+
 
 
 Semantics