SMTLIB (.smtlib) File Format
SMTLIB file format
SMT-LIB Logics Supported in Maple
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.
Unquantified formulas built over Boolean-valued symbols.
Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables.
Quantifier-free integer arithmetic.
Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables.
Quantifier-free real arithmetic.
Closed linear formulas over linear integer arithmetic.
Closed linear formulas in linear real arithmetic.
Translate a Boolean expression to SMT-LIB format in the QF_UF logic.
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(assert (=> (xor a b) c))
Translate a polynomial equation to SMT-LIB format in the logic of (possibly nonlinear) integer arithmetic.
(declare-fun x () Int)
(assert (= (+ (* x x x) x 1) 0))
[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.
Download Help Document