SMT-LIB (Satisfiability Modulo Theories LIBrary) is a interface language intended for use by programs designed to solve SMT (Satisfiability Modulo Theories) problems.

It is reminiscent of LISP in design and appearance.

The SMTLIB package provides tools for generating SMTLIB input from Maple expressions.

The general-purpose command Export supports this format.

SMT-LIB scripts require the underlying logic to be explicitly specified by name from a list of logics defined in the SMT-LIB standard.

For this reason, those Maple commands which generate SMT-LIB allow the logic to be specified (as a string). The following SMT-LIB logics are supported by these commands.

For more details on these logics, see the SMT-LIB Standard.

$\mathrm{SMTLIB}:-\mathrm{ToString}\left(a\mathbf{xor}b\Rightarrow c\,\mathrm{logic}=''QF\_UF''\right)$

$''(set-logic\; QF\_UF)\; (declare-fun\; a\; ()\; Bool)\; (declare-fun\; b\; ()\; Bool)\; (declare-fun\; c\; ()\; Bool)\; (assert\; (=>\; (xor\; a\; b)\; c))\; (check-sat)\; (exit)''$

$\mathrm{SMTLIB}:-\mathrm{ToString}\left(x^3+x+1=0\,\mathrm{logic}=''QF\_NIA''\right)$

$''(set-logic\; QF\_NIA)\; (declare-fun\; x\; ()\; Int)\; (assert\; (=\; (+\; (*\; x\; x\; x)\; x\; 1)\; 0))\; (check-sat)\; (exit)''$

[SMT-LIB Standard] Clark Barrett and Pascal Fontaine and Cesare Tinelli, The SMT-LIB Standard: Version 2.5, Department of Computer Science, The University of Iowa, 2015.