Skip to content

Commit

Permalink
Minor fixes for sets doc (cvc5#10060)
Browse files Browse the repository at this point in the history
  • Loading branch information
ajreynol authored Oct 2, 2023
1 parent 7ff15aa commit 74e943d
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions docs/theories/sets-and-relations.rst
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ a `cvc5::Solver solver` object.
+----------------------+----------------------------------------------+---------------------------------------------------------------------------+
| Sort | ``(Set <Sort>)`` | ``solver.mkSetSort(cvc5::Sort elementSort);`` |
+----------------------+----------------------------------------------+---------------------------------------------------------------------------+
| Constants | ``(declare-const X (Set Int)`` | ``Sort s = solver.mkSetSort(solver.getIntegerSort());`` |
| Constants | ``(declare-const X (Set Int))`` | ``Sort s = solver.mkSetSort(solver.getIntegerSort());`` |
| | | |
| | | ``Term X = solver.mkConst(s, "X");`` |
+----------------------+----------------------------------------------+---------------------------------------------------------------------------+
Expand All @@ -37,7 +37,7 @@ a `cvc5::Solver solver` object.
+----------------------+----------------------------------------------+---------------------------------------------------------------------------+
| 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);`` |
| 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)});`` |
+----------------------+----------------------------------------------+---------------------------------------------------------------------------+
Expand Down

0 comments on commit 74e943d

Please sign in to comment.