construct session object for SMT problem
Operations with Sessions
set, function, or boolean; expression to be checked for satisfiability
(optional) options as specified below
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.
Create a a SMTLIB session object for solving over quantifier-free integer linear arithmetic.
sess ≔ Session⁡logic=QF_LIA
sess≔SMTLIB Session32682312Variables: 0Stack Depth: 0
Assert this Diophantine problem.
Push the stack and add a side assumption. The problem becomes unsatisfiable.
Pop the stack and verify the problem is once again satisfiable.
The SMTLIB[Session] command was introduced in Maple 2022.
For more information on Maple 2022 changes, see Updates in Maple 2022.
Download Help Document