ToString - Maple Help

SMTLIB[Session]

 ToString
 get assertions active in session as an SMT-LIB string

 Calling Sequence session:-ToString()

Parameters

 session - a SMTLIB[Session] object

Description

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

Examples

Generate an SMT-LIB summary of the assertions made in this session.

 > $\mathrm{with}\left(\mathrm{SMTLIB}\right):$
 > $\mathrm{sess}≔\mathrm{Session}\left(\right)$
 ${\mathrm{sess}}{≔}\left[\begin{array}{c}{\mathrm{SMTLIB Session}}\\ {14699112}\\ {\mathrm{Variables: 0}}\\ {\mathrm{Stack Depth: 0}}\end{array}\right]$ (1)
 > $\mathrm{sess}:-\mathrm{Assert}\left(a\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}\mathbf{xor}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}b\mathbf{⇒}c\right)$
 > $\mathrm{sess}:-\mathrm{Assert}\left(b\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}\mathbf{and}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}\mathbf{not}\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}d\right)$
 > $\mathrm{sess}:-\mathrm{ToString}\left(\right)$
 ${"\left(declare-fun c \left(\right) Bool\right) \left(declare-fun b \left(\right) Bool\right) \left(declare-fun a \left(\right) Bool\right) \left(declare-fun d \left(\right) Bool\right) \left(assert \left(=> \left(xor a b\right) c\right)\right) \left(assert \left(and b \left(not d\right)\right)\right)"}$ (2)

Compatibility

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