SMTLIB - Maple Programming Help

Online Help

All Products    Maple    MapleSim


Home : Support : Online Help : Programming : Logic : SMTLIB Package : SMTLIB

SMTLIB

Tools for parsing and generating files in SMT-LIB format

 

Calling Sequence

Description

Accessing SMTLIB Package Commands

List of SMTLIB Package Commands

Examples

References

Compatibility

Calling Sequence

SMTLIB[command](arguments)

command(arguments)

Description

• 

The SMTLIB package provides tools for encoding Maple expressions into SMT-LIB format.

• 

The SMT-LIB format is an interface language for interacting with programs which solve Satisfiability Modulo Theories (SMT) problems.

Accessing SMTLIB Package Commands

• 

Each command in the SMTLIB package can be accessed by using either the long form or the short form of the command symbol in the command calling sequence.

• 

Because the underlying implementation of the SMTLIB package is a module, it is possible to use the form SMTLIB:-command to access a command from the package. For more information, see Module Members.

List of SMTLIB Package Commands

• 

The following is a list of commands available in the SMTLIB package.

ParseFile

ParseString

Satisfiable

Satisfy

Simplify

ToString

 

 

• 

To display the help page for a particular SMTLIB command, see Getting Help with a Command in a Package.

Examples

Generate an SMT-LIB script which tests for satisfiability of the input expression

with(SMTLIB):

ToString( (a and b and c) or (not a or b or not c) );

(declare-fun a () Bool) (declare-fun b () Bool) (declare-fun c () Bool) (assert (or (and a b c) (not a) b (not c))) (check-sat) (exit)

(1)

Find a satisfying assignment for the previous example.

Satisfy( (a and b and c) or (not a or b or not c) );

a=false,b=false,c=true

(2)

Generate an SMT-LIB script which returns a satisfying assignment for an equation using the logic of quantifier-free nonlinear integer arithmetic.

ToString( x^3+y^3=z^3, logic="QF_NIA" ) assuming posint;

(set-logic QF_NIA) (declare-fun V1 () Int) (declare-fun V2 () Int) (declare-fun V3 () Int) (assert (and (= (+ (* V1 V1 V1) (* V2 V2 V2)) (* V3 V3 V3)) (<= 1 V1) (<= 1 V2) (<= 1 V3))) (check-sat) (exit)

(3)

Check if a satisfying assignment for the previous example.

Satisfiable( x^3+y^3=z^3, logic="QF_NIA" ) assuming posint;

FAIL

(4)

References

  

Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The SMT-LIB Standard: Version 2.5

Compatibility

• 

The SMTLIB package was introduced in Maple 2017.

• 

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

See Also

Formats,SMTLIB

Logic[Satisfy]