SMTLIB - Maple Help

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.
 • 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.

 • 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 V1 \left(\right) Int\right) \left(declare-fun V2 \left(\right) Int\right) \left(declare-fun V3 \left(\right) Int\right) \left(assert \left(and \left(= \left(+ \left(* V1 V1 V1\right) \left(* V2 V2 V2\right)\right) \left(* V3 V3 V3\right)\right) \left(<= 1 V1\right) \left(<= 1 V2\right) \left(<= 1 V3\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.