Assert - Maple Help

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}}\\ {13801480}\\ {\mathrm{Variables: 0}}\\ {\mathrm{Stack Depth: 0}}\end{array}\right]$ (1)
 > $\left(\mathrm{session}:-\mathrm{Assert}\left(4
 ${::}{\mathrm{Typesetting}}{:-}{\mathrm{_Hold}}{}\left(\left[{\mathrm{integer}}\right]\right)$ (2)
 > $\mathrm{session}:-\mathrm{Satisfiable}\left(\right)$
 ${\mathrm{true}}$ (3)
 > $\mathrm{session}:-\mathrm{Push}\left(\right):$
 > $\left(\mathrm{session}:-\mathrm{Assert}\left(x<0\right)\right)::\mathrm{integer}$
 ${::}{\mathrm{Typesetting}}{:-}{\mathrm{_Hold}}{}\left(\left[{\mathrm{integer}}\right]\right)$ (4)
 > $\mathrm{session}:-\mathrm{Satisfiable}\left(\right)$
 ${\mathrm{false}}$ (5)

Compatibility

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