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.

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.

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.