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

Online Help

All Products    Maple    MapleSim


SMTLIB[Session]

  

Satisfiable

  

check if SMT problem from session is satisfiable

  

Satisfy

  

find satisfying instance for SMT problem from session

 

Calling Sequence

Parameters

Description

Details

Examples

Compatibility

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.

withSMTLIB:

sessionSession

sessionSMTLIB Session18995816Variables: 0Stack Depth: 0

(1)

session:-Assert1<xandx2<9::integer

::Typesetting:-_Holdinteger

(2)

session:-Satisfiable

true

(3)

session:-Assert2x

session:-Satisfiable

true

(4)

Compatibility

• 

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

• 

For more information on Maple 2022 changes, see Updates in Maple 2022.

See Also

SMTLIB

SMTLIB[Satisfy]

SMTLIB[Session]