Session - Maple Help

SMTLIB

 Session
 construct session object for SMT problem

 Calling Sequence Session(expr,options)

Parameters

 expr - set, function, or boolean; expression to be checked for satisfiability options - (optional) options as specified below

Options

 • 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.

Description

 • 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.

Operations with Sessions

 • The following functions can be performed with a SMTLIB Session.

Examples

Create a a SMTLIB session object for solving over quantifier-free integer linear arithmetic.

 > $\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]$ (1)

Assert this Diophantine problem.

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

Push the stack and add a side assumption. The problem becomes unsatisfiable.

 > $\mathrm{sess}:-\mathrm{Push}\left(\right)$
 ${1}$ (3)
 > $\mathrm{sess}:-\mathrm{Assert}\left(0
 > $\mathrm{sess}:-\mathrm{Satisfiable}\left(\right)$
 ${\mathrm{false}}$ (4)

Pop the stack and verify the problem is once again satisfiable.

 > $\mathrm{sess}:-\mathrm{Pop}\left(\right)$
 ${0}$ (5)
 > $\mathrm{sess}:-\mathrm{Satisfy}\left(\right)$
 $\left\{{x}{=}{4}{,}{y}{=}{-1}\right\}$ (6)

Compatibility

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