Tools for parsing and generating files in SMT-LIB format
Accessing SMTLIB Package Commands
List of SMTLIB Package Commands
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.
Generate an SMT-LIB script which tests for satisfiability of the input expression
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)))
Find a satisfying assignment for the previous example.
Satisfy( (a and b and c) or (not a or b or not c) );
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;
(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 if a satisfying assignment for the previous example.
Satisfiable( x^3+y^3=z^3, logic="QF_NIA" ) assuming posint;
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.
Download Help Document
What kind of issue would you like to report? (Optional)