Satisfiable - Maple Help

SMTLIB[Session]

 Satisfiable
 check if SMT problem from session is satisfiable
 Satisfy
 find satisfying instance for SMT problem from session

 Calling Sequence session:-Satisfiable() session:-Satisfy()

Parameters

 session - a SMTLIB[Session] object

Description

 • The session:-Satisfiable() command checks whether the SMT problem posed to the session session can be satisfied.
 • The session:-Satisfy() command finds a solution for the SMT problem posed to the session session.

Details

 • For details on SMT solving see SMTLIB[Satisfy].
 • For details on SMT sessions see SMTLIB[Session].
 • Note that SMTLIB[Session][Push] and SMTLIB[Session][Pop] operations affect the state of the problem posed to the session.

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}}\\ {28859064}\\ {\mathrm{Variables: 0}}\\ {\mathrm{Stack Depth: 0}}\end{array}\right]$ (1)
 > $\mathrm{session}:-\mathrm{Assert}\left(1
 ${::}{ℤ}$ (2)
 > $\mathrm{session}:-\mathrm{Satisfiable}\left(\right)$
 ${\mathrm{true}}$ (3)
 > $\mathrm{session}:-\mathrm{Assert}\left(2\le x\right)$
 > $\mathrm{session}:-\mathrm{Satisfiable}\left(\right)$
 ${\mathrm{true}}$ (4)

Compatibility

 • The SMTLIB[Session][Satisfiable] and SMTLIB[Session][Satisfy] commands were introduced in Maple 2022.