From b94739478ec6d7cfe373345ce9b7ff7674726db6 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Mon, 4 Apr 2022 19:14:37 -0700 Subject: [PATCH] docs: Fix mkTerm calls in theory documentation. (#8567) --- docs/theories/bags.rst | 16 ++--- docs/theories/separation-logic.rst | 4 +- docs/theories/sequences.rst | 28 ++++----- docs/theories/sets-and-relations.rst | 94 ++++++++++++++-------------- 4 files changed, 71 insertions(+), 71 deletions(-) diff --git a/docs/theories/bags.rst b/docs/theories/bags.rst index 6666015ae..597885162 100644 --- 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 55811ed25..2ae43a7c2 100644 --- 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 ```` and ```` | +----------------------+----------------------------------------------+--------------------------------------------------------------------+ -| 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 )`` | ``solver.mkSepNil(cvc5::Sort sort);`` | +----------------------+----------------------------------------------+--------------------------------------------------------------------+ diff --git a/docs/theories/sequences.rst b/docs/theories/sequences.rst index cb6806fa1..bc6148bef 100644 --- 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 88c38aa27..f6e277329 100644 --- 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 )`` | ``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 )`` | ``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 -- 2.30.2