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

  

ToString

  

get assertions active in session as an SMT-LIB string

 

Calling Sequence

Parameters

Description

Examples

Compatibility

Calling Sequence

session:-ToString()

Parameters

session

-

a SMTLIB[Session] object

Description

• 

The sess:-String() command translates the active assertions in the SMTLIB session sess to the SMT-LIB input format, expressed as a Maple string.

Examples

Generate an SMT-LIB summary of the assertions made in this session.

withSMTLIB:

sessSession

sessSMTLIB Session14699112Variables: 0Stack Depth: 0

(1)

sess:-Assertaxorbc

sess:-Assertbandnotd

sess:-ToString

(declare-fun c () Bool) (declare-fun b () Bool) (declare-fun a () Bool) (declare-fun d () Bool) (assert (=> (xor a b) c)) (assert (and b (not d)))

(2)

Compatibility

• 

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

• 

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

See Also

SMTLIB

SMTLIB[ToString]