From 1b4da763dfcb62a59290a6186a9d3b423c4fe203 Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Fri, 28 May 2021 11:10:28 +0200
Subject: [PATCH] Add computations for fp.le|lt|ge|gt|eq
---
src_colibri2/tests/solve/smt_fp/sat/dune.inc | 2 ++
.../solve/smt_fp/sat/simple_eq_float32.smt2 | 5 ++++
src_colibri2/theories/FP/float32.ml | 23 +++++++++++++++++++
src_colibri2/theories/FP/fp_value.mli | 2 +-
4 files changed, 31 insertions(+), 1 deletion(-)
create mode 100644 src_colibri2/tests/solve/smt_fp/sat/simple_eq_float32.smt2
diff --git a/src_colibri2/tests/solve/smt_fp/sat/dune.inc b/src_colibri2/tests/solve/smt_fp/sat/dune.inc
index 317cd2282..7c0354f44 100644
--- a/src_colibri2/tests/solve/smt_fp/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_fp/sat/dune.inc
@@ -7,5 +7,7 @@
(rule (alias runtest) (action (diff oracle recognize_rounding_mode.smt2.res)))
(rule (action (with-stdout-to simple_add_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:simple_add_float32.smt2}))))
(rule (alias runtest) (action (diff oracle simple_add_float32.smt2.res)))
+(rule (action (with-stdout-to simple_eq_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:simple_eq_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle simple_eq_float32.smt2.res)))
(rule (action (with-stdout-to simple_mul_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:simple_mul_float32.smt2}))))
(rule (alias runtest) (action (diff oracle simple_mul_float32.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_fp/sat/simple_eq_float32.smt2 b/src_colibri2/tests/solve/smt_fp/sat/simple_eq_float32.smt2
new file mode 100644
index 000000000..11abb9fe5
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/simple_eq_float32.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-fun x () (_ FloatingPoint 8 24))
+(declare-fun y () (_ FloatingPoint 8 24))
+(assert (fp.eq (fp.add RNE x y) x))
+(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/theories/FP/float32.ml b/src_colibri2/theories/FP/float32.ml
index 7a641d43e..7e8bf1319 100644
--- a/src_colibri2/theories/FP/float32.ml
+++ b/src_colibri2/theories/FP/float32.ml
@@ -47,6 +47,7 @@ let compute_ground d t =
let (!>>) t = Rounding_mode.value (Rounding_mode.coerce_nodevalue (interp d t )) in
let (!>) t = Float32.value (Float32.coerce_nodevalue (interp d t)) in
let (!<) v = `Some (Float32.nodevalue (Float32.index v)) in
+ let (!<<) v = `Some (Boolean.BoolValue.nodevalue (Boolean.BoolValue.index v)) in
match Ground.sem t with
| { app = {builtin = Expr.Fp_add (8, 24); _}; args; _} ->
let m, a, b = IArray.extract3_exn args in
@@ -64,6 +65,21 @@ let compute_ground d t =
let m, a, b = IArray.extract3_exn args in
if Farith.B32.(eq !>b (zero true) || eq !>b (zero false)) then `Uninterp
else !< (Farith.B32.div !>>m !>a !>b)
+ | { app = {builtin = Expr.Fp_eq (8, 24); _}; args; _} ->
+ let a, b = IArray.extract2_exn args in
+ !<< (Farith.B32.eq !>a !>b)
+ | { app = {builtin = Expr.Fp_leq (8, 24); _}; args; _} ->
+ let a, b = IArray.extract2_exn args in
+ !<< (Farith.B32.le !>a !>b)
+ | { app = {builtin = Expr.Fp_lt (8, 24); _}; args; _} ->
+ let a, b = IArray.extract2_exn args in
+ !<< (Farith.B32.lt !>a !>b)
+ | { app = {builtin = Expr.Fp_geq (8, 24); _}; args; _} ->
+ let a, b = IArray.extract2_exn args in
+ !<< (Farith.B32.ge !>a !>b)
+ | { app = {builtin = Expr.Fp_gt (8, 24); _}; args; _} ->
+ let a, b = IArray.extract2_exn args in
+ !<< (Farith.B32.gt !>a !>b)
| _ -> `None
let init_check d = Interp.Register.check d (fun d t ->
@@ -155,6 +171,13 @@ let converter d (f:Ground.t) =
List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b]
in
match Ground.sem f with
+ | {app={builtin=Expr.Fp_abs (8, 24); _}; args; _} ->
+ let a = IArray.extract1_exn args in
+ reg a; attach d f;
+ let wait =
+ set r (let+ va = get a in Farith.B32.abs va)
+ in
+ List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a; r]
| {app={builtin=Expr.Fp_add (8, 24); _}; args; _} ->
let m, a, b = IArray.extract3_exn args in
reg m; reg a; reg b; attach d f;
diff --git a/src_colibri2/theories/FP/fp_value.mli b/src_colibri2/theories/FP/fp_value.mli
index 947ebe724..62ee723d8 100644
--- a/src_colibri2/theories/FP/fp_value.mli
+++ b/src_colibri2/theories/FP/fp_value.mli
@@ -26,7 +26,7 @@ val posint_sequence : Z.t Base.Sequence.t
(** Names (string) wrapped in a module *)
module type FloatName = sig val name : string end
-(**
+(**
Helper to extend a module of type [Farith.S] into a module of
type [ValueKind.Value]
*)
--
GitLab