This page will detail the work presented in Approximations for Model Construction. The goal is to solve quantifier-free first-order constraints over theory of FPA. The procedure presented in the paper is an iterative approximation refinement procedure. The approximations used for FPA cannot be classified as either over- or under-approximations. The approximation changes the floating-point sort of the individual occurrences of operations and constants and changes them accordingly. Initially, all sorts are as small as possible and will (unless the model is obtained sooner) increase until they reach the sorts of the original problem. The procedure is built upon the bit-vector encoding of FPA and it's subsequent bit-blasting to a propositional formula.

About (the Theory of) Floating-Point Arithmetic

The Floating-Point Arithmetic is defined by the Standard IEEE 754-2008 (orig. 1985). The Theory of Floating-Point Arithmetic refers to the SMT-LIB theory which can be found here.

Implementation

The described approach is implemented as a tactic within the Z3 SMT solver and the source code can be found here.

Benchmarks

Benchamarks used in the paper have been used to evaluate the ACDCL approach to solving FPA found in MathSAT. The benchmarks originate from verification problems of C programs performing numerical computations, where ranges and error bounds of variables and expressions are verified; other benchmarks are randomly generated systems of inequalities over bounded floating-point variables.

Experimental evaluation

We performed comparison with the base method (implemented in Z3) and the ACDCL approach (MathSAT).