diff --git a/docs/theories/sets-and-relations.rst b/docs/theories/sets-and-relations.rst index bce2ef5329b..cbe14739b1d 100644 --- a/docs/theories/sets-and-relations.rst +++ b/docs/theories/sets-and-relations.rst @@ -19,7 +19,7 @@ a `cvc5::Solver solver` object. +----------------------+----------------------------------------------+---------------------------------------------------------------------------+ | Sort | ``(Set )`` | ``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");`` | +----------------------+----------------------------------------------+---------------------------------------------------------------------------+ @@ -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)});`` | +----------------------+----------------------------------------------+---------------------------------------------------------------------------+