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.
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.
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 x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (and (= (+ (* x x x) (* y y y)) (* z z z)) (<= 1 x) (<= 1 y) (<= 1 z)))
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