SMTLIB - Maple Help

SMTLIB (.smtlib) File Format

SMTLIB file format

Description

 • 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 Logics Supported in Maple

 • 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.

 QF_UF Unquantified formulas built over Boolean-valued symbols. QF_LIA Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables. QF_NIA Quantifier-free integer arithmetic. QF_LRA Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables. QF_NRA Quantifier-free real arithmetic. LIA Closed linear formulas over linear integer arithmetic. LRA Closed linear formulas in linear real arithmetic.

Examples

Translate a Boolean expression to SMT-LIB format in the QF_UF logic.

 > $\mathrm{SMTLIB}:-\mathrm{ToString}\left(a\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{xor}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}b⇒c,\mathrm{logic}="QF_UF"\right)$
 ${"\left(set-logic QF_UF\right) \left(declare-fun a \left(\right) Bool\right) \left(declare-fun b \left(\right) Bool\right) \left(declare-fun c \left(\right) Bool\right) \left(assert \left(=> \left(xor a b\right) c\right)\right) \left(check-sat\right) \left(exit\right)"}$ (1)

Translate a polynomial equation to SMT-LIB format in the logic of (possibly nonlinear) integer arithmetic.

 > $\mathrm{SMTLIB}:-\mathrm{ToString}\left({x}^{3}+x+1=0,\mathrm{logic}="QF_NIA"\right)$
 ${"\left(set-logic QF_NIA\right) \left(declare-fun x \left(\right) Int\right) \left(assert \left(= \left(+ \left(* x x x\right) x 1\right) 0\right)\right) \left(check-sat\right) \left(exit\right)"}$ (2)

References

 [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.