The session:-Satisfiable() command checks whether the SMT problem posed to the session session can be satisfied.

The session:-Satisfy() command finds a solution for the SMT problem posed to the session session.

For details on SMT solving see SMTLIB[Satisfy].

For details on SMT sessions see SMTLIB[Session].

Note that SMTLIB[Session][Push] and SMTLIB[Session][Pop] operations affect the state of the problem posed to the session.

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

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

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

$\mathrm{session}:-\mathrm{Assert}\left(1<x\mathbf{and}{x}^2<9\right)::\mathrm{integer}$

$::\mathbb{Z}$

$\mathrm{session}:-\mathrm{Satisfiable}\left(\right)$

$\mathrm{true}$

$\mathrm{session}:-\mathrm{Assert}\left(2\le x\right)$

$\mathrm{session}:-\mathrm{Satisfiable}\left(\right)$

$\mathrm{true}$

The SMTLIB[Session][Satisfiable] and SMTLIB[Session][Satisfy] commands were introduced in Maple 2022.

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