Support reasoning over most the SMT-LIB FPA theory symbols - #1364

Open

hra687261 wants to merge 32 commits into

OCamlPro:nextfrom

hra687261:fpa_axioms

Commits on Jun 30, 2026

Add axiomatization of the SMT-LIB FPA theory
hra687261
committed
00b5eca
Map Dolmen terms to the symbols of the SMT-LIB FPA theory axiomatization
hra687261
committed
fcd9014
Propagate axiomatized predicates for FPA literals
hra687261
committed
fd96706
Propagate deduced equalities from asserted predicates in FPA relation
hra687261
committed
b23f211
Add FPA shostak theory to solve equalities with literals
hra687261
committed
56b38f9
Ensure that the FPA shostak theory solver and relation are only used when the `smt_lib_fpa` option is set to true
hra687261
committed
746852e
Test symbolic reasoning on smt-lib fpa theory
hra687261
committed
a9f8625
upd CHANGES.md
hra687261
committed
76b1ca7

Commits on Jul 7, 2026

Commits on Jul 8, 2026

Only track ae.float's mode argument, not eb and sb since they will always be literals in the theory, remove support for symbolic arguments for ae.round + float*
hra687261
committed
d1b5a07
Add FPA timer
hra687261
committed
96d825f
Cleanup and avoid duplicate calls to `E.Ints.of_int` in `fpa_rel`
hra687261
committed
6a9f68e
Track new_terms in fpa_rel
hra687261
committed
f5f8854
Simplify `deduce_fpval_eq`
hra687261
committed
6c5cf9e
Pass `ex` as an argument to `apply`
hra687261
committed
625d054
Add comment explaining how SMT-LIB FPA axiomatization was produced.
hra687261
committed
ed93826
Take explanations into account in AEFloat_arg_watch
hra687261
committed
d842bbc
use sqrt_real
hra687261
committed
b1b7597

Commits on Jul 10, 2026

Upd doc comments, improve debug printing of finite FPA literals, and fpa's hash function
hra687261
committed
f197078
Better matching order in translate.ml
hra687261
committed
dbfd377
Replace Fpa_rounding.rounding_mode with Dolmen's rounding mode constructors
hra687261
committed
88fefa3
Add symbolic reasoning tests
hra687261
committed
2fc901b
Add Fp_value.equal
hra687261
committed
9ae85fa
Better error msg in fpa.ml
hra687261
committed
5d3b9de
Put type parameters in literals in the shostak FPA theory
hra687261
committed
2ecc45a
Inline const_view
hra687261
committed
e1474a5
Treat unsupported FPA functions as uninterpreted symbols
hra687261
committed
fba01a1
Use `eb` and `sb` instead of `e` and `s` in `Expr.FP`
hra687261
committed
98de1b6