Assert - 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]

  

Assert

  

add assertion to current level of SMTLIB session stack

 

Calling Sequence

Parameters

Description

Details

Examples

Compatibility

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.

withSMTLIB:

sessionSession

sessionSMTLIB Session13801480Variables: 0Stack Depth: 0

(1)

session:-Assert4<x::integer

::Typesetting:-_Holdinteger

(2)

session:-Satisfiable

true

(3)

session:-Push&colon;

session:-Assertx<0::integer

::Typesetting:-_Holdinteger

(4)

session:-Satisfiable

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.

See Also

SMTLIB

SMTLIB[Session]