The sess:-String() command translates the active assertions in the SMTLIB session sess to the SMT-LIB input format, expressed as a Maple string.

$\mathrm{with}\left(\mathrm{SMTLIB}\right)\:$

$\mathrm{sess}≔\mathrm{Session}\left(\right)$

$\mathrm{sess}≔\left[\begin{array}{c}\mathrm{SMTLIB\; Session}\\ 15559352\\ \mathrm{Variables:\; 0}\\ \mathrm{Stack\; Depth:\; 0}\end{array}\right]$

$\mathrm{sess}:-\mathrm{Assert}\left(a\mathbf{xor}b\Rightarrow c\right)$

$\mathrm{sess}:-\mathrm{Assert}\left(b\mathbf{and}\mathbf{not}d\right)$

$\mathrm{sess}:-\mathrm{ToString}\left(\right)$

$''(declare-fun\; c\; ()\; Bool)\; (declare-fun\; b\; ()\; Bool)\; (declare-fun\; a\; ()\; Bool)\; (declare-fun\; d\; ()\; Bool)\; (assert\; (=>\; (xor\; a\; b)\; c))\; (assert\; (and\; b\; (not\; d)))''$

The SMTLIB[Session][ToString] command was introduced in Maple 2022.

For more information on Maple 2022 changes, see Updates in Maple 2022.