Depth - Maple Help

SMTLIB[Session]

 Depth
 query depth of SMTLIB session stack
 Pop
 pop one or more levels from SMTLIB session stack
 Push
 push zero or more levels onto SMTLIB session stack
 Reset
 reset SMTLIB session stack

 Calling Sequence session:-Depth() session:-Pop( m ) session:-Push() session:-Reset()

Parameters

 session - a SMTLIB[Session] object m - (optional) positive integer

Description

 • The session:-Depth() command returns the current depth of the stack associated with the SMTLIB session session. The depth of the stack of a fresh session is 0.
 • The session:-Pop(m) command pops m levels off of the stack associated with the SMTLIB session session. The default value of m is 1.
 • The session:-Push() command pushes a new level onto the stack associated with the SMTLIB session session.
 • The session:-Reset() command clears all assertions in the SMTLIB session session and resets the stack depth to zero.

Details

 • Popping the stack will delete all assertions made at the current stack level.

Examples

Test for the satisfiability of this simple Boolean problem.

 > $\mathrm{with}\left(\mathrm{SMTLIB}\right):$
 > $\mathrm{session}≔\mathrm{Session}\left(\right)$
 ${\mathrm{session}}{≔}\left[\begin{array}{c}{\mathrm{SMTLIB Session}}\\ {13904568}\\ {\mathrm{Variables: 0}}\\ {\mathrm{Stack Depth: 0}}\end{array}\right]$ (1)
 > $\mathrm{session}:-\mathrm{Assert}\left(7<2x\right)::\mathrm{integer}$
 ${::}{ℤ}$ (2)
 > $\mathrm{session}:-\mathrm{Satisfiable}\left(\right)$
 ${\mathrm{true}}$ (3)
 > $\mathrm{session}:-\mathrm{Push}\left(\right):$
 > $\mathrm{session}:-\mathrm{Assert}\left(x<0\right)::\mathrm{integer}$
 ${::}{ℤ}$ (4)
 > $\mathrm{session}:-\mathrm{Satisfiable}\left(\right)$
 ${\mathrm{false}}$ (5)
 > $\mathrm{session}:-\mathrm{Pop}\left(\right):$
 > $\mathrm{session}:-\mathrm{Satisfiable}\left(\right)$
 ${\mathrm{true}}$ (6)

Compatibility

 • The SMTLIB[Session][Depth], SMTLIB[Session][Pop], SMTLIB[Session][Push] and SMTLIB[Session][Reset] commands were introduced in Maple 2022.