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.

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.

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.

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)''$

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\}$

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

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

$\mathrm{FAIL}$

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

The SMTLIB package was introduced in Maple 2017.

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