Support reasoning over most the SMT-LIB FPA theory symbols by hra687261 · Pull Request #1364 · OCamlPro/alt-ergo

hra687261 · 2026-06-24T11:55:36Z

This PR adds a prelude which axiomatizes the semantics of most of the SMT-LIB FPA theory symbols, and maps the symbols of the theory parsed by dolmen to these axiomatizations, providing support for symbolic reasoning over most of them (except fp.rem, fp.to_fp, fp.of_sbv, fp.of_ubv, fp.to_ubv and fp.to_sbv the support for which will be added in the future in a separate PR).
The PR also propagates for each of the FPA literals for which support was added in #1358 predicates and assertions which allow linking these literals to the axiomatization. It also adds propagation of equalities with literals from asserted predicates, as well as a shostak theory to solve equalities between fp literals among themselves or fp literals and fp variables.

…when the `smt_lib_fpa` option is set to true

…ns from them

…ns with symbolic precision and rounding mode arguments

…ways be literals in the theory, remove support for symbolic arguments for ae.round + float*

Halbaroth · 2026-07-08T09:50:54Z

  | NaN -> Fmt.pf ppf "NaN"
-  | Finite { neg; biased_exp; significand } ->
-    Fmt.pf ppf "fp[%b;%d;%s]" neg biased_exp (Z.to_string significand)
+  | Finite q -> Fmt.pf ppf "fp[%s]" (Q.to_string q)


We display the size of the biased and significand in the smtlib printer but loss it in the debug printer.

Yes, because the smt-lib printer is expected (I suppose) to produce something that is (at least close) to something parseable in the smt-lib format, while this one is for debugging only.
On the other hand, I am not sure if for debugging it is better to print a Q.t or the mantissa/significand bit-vectors, intuitively, since we represent finite Floats as Q.t, I'd say its this one but I am not sure, in practice I've seen that it quickly becomes unreadable anyway.

Ideally for debug we would print as a float, i.e. a real with a dot (decimal would be nice but hexadecimal is easy to do I believe)!

We could simply convert to float then print with "%.17g", but we would lose precision on float > 64, so maybe the hex format is best.
The current version should be good.

Halbaroth · 2026-07-08T12:19:40Z

+          watched_args = add_by_arg r_mode term t.watched_args
+        }
+
+  let subst ~ex:_ rr nrr t =


You don't need to track the explanation as these domains cannot generate conflicts?

Indeed, this one simply tracks arguments and substitutes them when they becomes literals, then propagates equalities, but it might actually still be necessary to pass the explanation down to the deduced equalities, I will do that. (Not exactly sure, the explanation is probably attached to the semantic values already no?)
Now, that I think of it, since Sy.Op Float now supports symbolic arguments for the rounding mode, its not clear that this domain is still necessary.

Halbaroth · 2026-07-08T12:24:00Z

@@ -0,0 +1,1845 @@
+(set-logic ALL)


Should we be concerned about the license of this file? It is essentially a one-one translation of the Why3 theory.

Not sure, though the transformation is pretty significant, I wouldn't call it a "one-one translation". It's also not clear how the license applies, since the original axiomatization was technically generated by Why3 and not part of its source code.

Alt-Ergo is distributed under a unfree license but Why3 is a free software under the terms of LGPL 2.1 https://gitlab.inria.fr/why3/why3/-/blob/master/LICENSE?ref_type=heads

This file is a kind of derivative work of the original file in Why3.

This file is a kind of derivative work of the original file in Why3.

That is unclear, since:

the original axiomatization was technically generated by Why3 and not part of its source code.

(Though it is generated from a whyml module which is part of the Why3 source code ...)

Anyway, what do you suggest?

bclement-ocp

Thanks :) Did a first pass with some comments, but did not look at the prelude and some calculations in detail yet.

bclement-ocp · 2026-07-09T06:40:46Z

+             @@ Dolmen_type.Base.app0
+                  (module Dl.Typer.T)
+                  env s DE.Ty.roundingMode)
+      |> add_constrs )


We should remove the rounding mode type from fpa_rounding.ml if we don't use it anymore (and if we do, replace it with DE.Ty.roundingMode).

Done. But unfortunately, rounding modes in Dolmen are put in the same ADT as other FP symbols, so it makes matching on rounding modes awkward (we always have to skip the cases of the non-rounding mode symbols).
I will open a PR on Dolmen to put rounding modes in their own enum type (with the hope that it will be accepted and be part of the next Dolmen release).

bclement-ocp · 2026-07-09T06:43:15Z

+    | Id { ns = Term; name = Simple "ae.float" } ->
+      Dl.Typer.T.builtin_term
+      @@ Dolmen_type.Base.term_app_cst (module Dl.Typer.T) env ae_float_cst


Ah, it is unfortunate that we need to expose both ae.round (with _ constant args) and ae.float :(

Indeed, IIRC indexed operators expect literals as indices not symbolic values, so we have to. But maybe in the future we can deprecate ae.round for ae.float, or rename ae.float to ae.round and make the precisions arguments normal arguments instead of indices (because its a better name, the operator in alt-ergo should probably renamed to something like FloatRound instead of just Float)

bclement-ocp · 2026-07-09T06:44:06Z

+  | `App (`Builtin (B.Float B.Float.RoundingMode), []) ->
+    Fpa_rounding.fpa_rounding_mode


I think this should go above, along with the other App cases (likely just after B.Unit).

bclement-ocp · 2026-07-09T06:45:14Z

+    when Compat.List.is_empty tyl && String.equal name E.FP.Names.t ->
+    (* To get the generic abstract float type from the axiomatization which is
+       stored as type varialbe `ae.fp.t`. *)
+    tv


I'm not sure I understand this. Why don't we define ae.fp.t directly here (like we do e.g. for rounding mode) and make it available to the axiomatization?

bclement-ocp · 2026-07-09T06:49:54Z

+        | B.Float RoundNearestTiesToEven -> mk_rounding NearestTiesToEven
+        | B.Float RoundNearestTiesToAway -> mk_rounding NearestTiesToAway
+        | B.Float RoundTowardPositive -> mk_rounding Up
+        | B.Float RoundTowardNegative -> mk_rounding Down
+        | B.Float RoundTowardZero -> mk_rounding ToZero


Please keep these within the global match on B.Float below (moving guards on when get_smt_lib_fpa to the constants).

bclement-ocp · 2026-07-09T07:07:26Z

  val ieee_format_to_fp : t -> int -> int -> t
+
+  (* arithmetic with rounding mode *)
+  val add : e:int -> s:int -> mode:t -> t -> t -> t


The e and s labelled arguments should maybe be explained somewhere? Is there a reason they are called e and s rather than eb and sb following the SMT-LIB?

This just follows what the Dolmen constructors used, e and s probably as short for eb and sb.
I changed them.

bclement-ocp · 2026-07-09T07:11:35Z

  | NaN -> Fmt.pf ppf "NaN"
-  | Finite { neg; biased_exp; significand } ->
-    Fmt.pf ppf "fp[%b;%d;%s]" neg biased_exp (Z.to_string significand)
+  | Finite q -> Fmt.pf ppf "fp[%s]" (Q.to_string q)


Ideally for debug we would print as a float, i.e. a real with a dot (decimal would be nice but hexadecimal is easy to do I believe)!

bclement-ocp · 2026-07-09T07:13:10Z

+  (* hidden_bit = 2^(sb-1), m >= hidden_bit -> normal *)
+  let hidden_bit = Z.shift_left Z.one (sb - 1) in
+  let biased_exp, significand =
+    if Z.compare m hidden_bit >= 0


I think we can simply check Z.testbit m (sb - 1)?

…fpa's hash function

…uctors

hra687261 force-pushed the fpa_axioms branch from 7806103 to 931019d Compare June 24, 2026 12:02

hra687261 marked this pull request as draft June 24, 2026 14:06

hra687261 force-pushed the fpa_axioms branch from 2f1cadf to 7f3f31d Compare June 30, 2026 11:52

hra687261 added 2 commits June 30, 2026 16:21

Add axiomatization of the SMT-LIB FPA theory

00b5eca

Map Dolmen terms to the symbols of the SMT-LIB FPA theory axiomatization

fcd9014

hra687261 force-pushed the fpa_axioms branch 2 times, most recently from f64ec20 to 0b6592b Compare June 30, 2026 14:24

hra687261 marked this pull request as ready for review June 30, 2026 14:27

hra687261 added 6 commits June 30, 2026 16:50

Propagate axiomatized predicates for FPA literals

fd96706

Propagate deduced equalities from asserted predicates in FPA relation

b23f211

Add FPA shostak theory to solve equalities with literals

56b38f9

Ensure that the FPA shostak theory solver and relation are only used …

746852e

…when the `smt_lib_fpa` option is set to true

Test symbolic reasoning on smt-lib fpa theory

a9f8625

upd CHANGES.md

76b1ca7

hra687261 force-pushed the fpa_axioms branch from 0b6592b to 76b1ca7 Compare June 30, 2026 14:52

hra687261 added 4 commits July 7, 2026 13:22

Use a domain to store and represent FPA predicates, and make deductio…

3981814

…ns from them

Add debug messages to FPA relation and shostak theory

ddfb824

Cleanup axiomatization by using builtin int.pow2

f8da815

Use builtin ae.float symbol, and add domain to support its applicatio…

65b553e

…ns with symbolic precision and rounding mode arguments

hra687261 force-pushed the fpa_axioms branch from 6207116 to 65b553e Compare July 7, 2026 12:37

hra687261 added 2 commits July 7, 2026 23:36

Add patterns to all axioms

a96023a

Only track ae.float's mode argument, not eb and sb since they will al…

d1b5a07

…ways be literals in the theory, remove support for symbolic arguments for ae.round + float*

Halbaroth reviewed Jul 8, 2026

View reviewed changes

hra687261 added 6 commits July 8, 2026 16:28

Add FPA timer

96d825f

Cleanup and avoid duplicate calls to E.Ints.of_int in fpa_rel

6a9f68e

Track new_terms in fpa_rel

f5f8854

Simplify deduce_fpval_eq

6c5cf9e

Pass ex as an argument to apply

625d054

Add comment explaining how SMT-LIB FPA axiomatization was produced.

ed93826

hra687261 added 2 commits July 8, 2026 20:00

Take explanations into account in AEFloat_arg_watch

d842bbc

use sqrt_real

b1b7597

bclement-ocp reviewed Jul 9, 2026

View reviewed changes

hra687261 added 10 commits July 10, 2026 15:37

Upd doc comments, improve debug printing of finite FPA literals, and …

f197078

…fpa's hash function

Better matching order in translate.ml

dbfd377

Replace Fpa_rounding.rounding_mode with Dolmen's rounding mode constr…

88fefa3

…uctors

Add symbolic reasoning tests

2fc901b

Add Fp_value.equal

9ae85fa

Better error msg in fpa.ml

5d3b9de

Put type parameters in literals in the shostak FPA theory

2ecc45a

Inline const_view

e1474a5

Treat unsupported FPA functions as uninterpreted symbols

fba01a1

Use eb and sb instead of e and s in Expr.FP

98de1b6

		\| `App (`Builtin (B.Float B.Float.RoundingMode), []) ->
		Fpa_rounding.fpa_rounding_mode

Uh oh!

Conversation

hra687261 commented Jun 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

bclement-ocp left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

hra687261 commented Jun 24, 2026 •

edited

Loading