The SMTLIB package provides support for converting Maple expressions to input in the SMT-LIB language format.
SMT-LIB is an interface language frequently used by programs designed to solve SMT (Satisfiability Modulo Theories) problems.
The SMTLIB[ToString] command converts a Maple expression into SMT-LIB input which can then be fed as input into an SMT solver program. By default, the generated SMT-LIB script performs a simple satisfiability query.
Example 1: Generate an SMT-LIB script testing whether a logical formula has a satisfying assignment (that is, an assignment of values making the formula true).
| (1.1) |
| (1.3) |
If an explicit satisfying assignment is desired, we can optionally generate a script requesting the SMT solver to produce one (here, a set of values for , , for which the formula is true).
| (1.4) |
In addition to Boolean-valued variables, SMT-LIB variables may also be numeric. The generated SMT-LIB requests a nontrivial solution in positive integers to the equation . (When such a solution exists, the integer is known as a taxicab number, the smallest of which is 1729.)
| (1.5) |