logic = string

The value of option logic is a string which must correspond to one of the following logic names defined by the SMT-LIB standard: "QF_UF", "QF_LIA", "QF_NIA", "QF_LRA", "QF_NRA", "LIA", and "LRA".

For an explanation of these logics, see Formats,SMTLIB.

timelimit = positive or infinity

Specify a time limit for the call to the SMT solver. A nonzero value represents a time budget in seconds for SMTLIB[Session][Satisfiable] or SMTLIB[Session][Satisfy] calls. The default is infinity, meaning no limit is imposed.

The Session(expr) command creates a session object for working interactively with an SMT solver. In particular, the session has a stack which can be pushed to add additional assumptions onto the current problem, and popped to remove these assumptions to restore the previous problem state.

The following functions can be performed with a SMTLIB Session.

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

$\mathrm{sess}≔\mathrm{Session}\left(\mathrm{logic}=''QF\_LIA''\right)$

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

$\mathrm{sess}:-\mathrm{Assert}\left(\left\{x+y=3\,2x+3y=5\right\}\right)$

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

$\mathrm{true}$

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

$1$

$\mathrm{sess}:-\mathrm{Assert}\left(0<y\right)$

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

$\mathrm{false}$

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

$0$

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

$\left\{x=4\&comma;y=\mathrm{-1}\right\}$

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

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