SMT-LIB language

Since version 2.5.0, Alt-Ergo supports the SMT-LIB language from the SMT community. This support is enabled by the Dolmen library.

Note

In version 2.5.x, the --frontend dolmen option is required to get full SMT-LIB support. Starting from version 2.6.0, this option became the default and is no longer necessary.

Alt-Ergo supports the following SMT-LIB theories:

  • The Core theory of booleans.

  • The ArraysEx theory of functional arrays with extensionality.

  • The FixedSizeBitVectors theory of bit-vectors (since version 2.5.0).

  • The Ints theory of integers[1].

  • The Reals theory of real numbers.

  • The Reals_Ints theory of real and integer numbers[2].

Bit-vectors

Alt-Ergo supports the FixedSizeBitVectors theory, as well as the additional symbols from the QF_BV and BV logics.

The non-standard symbols bv2nat and (_ int2bv n) (where n > 0 is a natural number representing the target bit-vector size) for conversion between integers and bit-vectors are supported.

Floating-Point Arithmetic

Alt-Ergo does not currently support the FloatingPoint SMT-LIB theory. Instead, Alt-Ergo implements the second and third layers described in the paper “A Three-tier Strategy for Reasoning about Floating-Point Numbers in SMT” by Conchon et al.

Alt-Ergo provides the rounding function described in the paper by making available all functions symbols with declarations of the form below, where prec and exp are numerals greater than 1 and RoundingMode is defined in the FloatingPoint SMT-LIB theory.

((_ ae.round prec exp) RoundingMode Real Real)

prec defines the number of bits in the significand, including the hidden bit, and is equivalent to the sb parameter of the (_ FloatingPoint eb sb) sort in the FloatingPoint SMT-LIB theory.

exp defines the absolute value of the exponent of the smallest representable positive number (this is not the same as the emin value defined in IEEE-754, which is the minimum exponent of the smallest normal positive number). An appropriate value for exp can be computed from the eb and sb parameters of the (_ FloatingPoint eb sb) sort as exp = 2^(eb - 1) + sb - 3.

The result of (_ ae.round prec exp) is always of the form (-1)^s * c * 2^q where s is a sign (0 or 1), c is an integer with at most prec - 1 binary digits (i.e. 0 <= c < 2^(prec - 1)) and q >= -exp is an integer.

The following function symbols are provided as short synonyms for common floating point representations:

  • ae.float16 is a synonym for (_ ae.round 11 24)

  • ae.float32 is a synonym for (_ ae.round 24 149)

  • ae.float64 is a synonym for (_ ae.round 53 1074)

  • ae.float128 is a synonym for (_ ae.round 113 16494)

Examples

Input:

(set-option :produce-models true)
(set-logic ALL)
(declare-const |0.3f32| Real)
(assert (= (ae.float32 RNE 0.3) |0.3f32|))
(declare-const |0.3f16| Real)
(assert (= (ae.float16 RNE 0.3) |0.3f16|))
(check-sat)
(get-model)

Output:

unknown
(
  (define-fun |0.3f32| () Real (/ 5033165 16777216))
  (define-fun |0.3f16| () Real (/ 1229 4096))
)