Assert - Maple Help
For the best experience, we recommend viewing online help using Google Chrome or Microsoft Edge.

SMTLIB[Session]

 Assert
 add assertion to current level of SMTLIB session stack

 Calling Sequence session:-Assert( expr )

Parameters

 session - a SMTLIB[Session] object expr - set, function, or boolean; expression to be asserted

Description

 • The session:-Assert(m) command asserts the truth of expression expr within the SMTLIB session session.

Details

 • Assertions made at a given stack level will be deleted when the stack is popped with SMTLIB[Session][Pop].

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}}\\ {26036920}\\ {\mathrm{Variables: 0}}\\ {\mathrm{Stack Depth: 0}}\end{array}\right]$ (1)
 > $\mathrm{session}:-\mathrm{Assert}\left(4
 ${::}{ℤ}$ (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)

Compatibility

 • The SMTLIB[Session][Assert] command was introduced in Maple 2022.
 • For more information on Maple 2022 changes, see Updates in Maple 2022.