SMTLIB (.smtlib) File Format - Maple Programming Help

Online Help

All Products    Maple    MapleSim


Home : Support : Online Help : Programming : Input and Output : File Formats : Formats/SMTLIB

SMTLIB (.smtlib) File Format

SMTLIB file format

 

Description

SMT-LIB Logics Supported in Maple

Examples

References

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.

SMTLIB:-ToStringaxorbc,logic=QF_UF

(set-logic QF_UF) (declare-fun a () Bool) (declare-fun b () Bool) (declare-fun c () Bool) (assert (=> (xor a b) c)) (check-sat) (exit)

(1)

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

SMTLIB:-ToStringx3+x+1=0,logic=QF_NIA

(set-logic QF_NIA) (declare-fun x () Int) (assert (= (+ (* x x x) x 1) 0)) (check-sat) (exit)

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

See Also

Formats

SMTLIB