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

SMTLIB

Tools for parsing and generating files in SMT-LIB format

 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.
 The long form, SMTLIB:-command, is always available. The short form can be used after loading the package.

List of SMTLIB Package Commands

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

 • 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) );
 ${"\left(declare-fun a \left(\right) Bool\right) \left(declare-fun b \left(\right) Bool\right) \left(declare-fun c \left(\right) Bool\right) \left(assert \left(or \left(and a b c\right) \left(not a\right) b \left(not c\right)\right)\right) \left(check-sat\right) \left(exit\right)"}$ (1)

Find a satisfying assignment for the previous example.

 > Satisfy( (a and b and c) or (not a or b or not c) );
 $\left\{{a}{=}{\mathrm{false}}{,}{b}{=}{\mathrm{false}}{,}{c}{=}{\mathrm{true}}\right\}$ (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;
 ${"\left(set-logic QF_NIA\right) \left(declare-fun x \left(\right) Int\right) \left(declare-fun y \left(\right) Int\right) \left(declare-fun z \left(\right) Int\right) \left(assert \left(and \left(= \left(+ \left(* x x x\right) \left(* y y y\right)\right) \left(* z z z\right)\right) \left(<= 1 x\right) \left(<= 1 y\right) \left(<= 1 z\right)\right)\right) \left(check-sat\right) \left(exit\right)"}$ (3)

Check if a satisfying assignment for the previous example.

 > Satisfiable( x^3+y^3=z^3, logic="QF_NIA" ) assuming posint;
 ${\mathrm{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.