From 84a95ff2b24c877bae2f5a17aae4e98d6c5dc25c Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Fri, 21 May 2021 12:44:30 +0200
Subject: [PATCH] Add interpretation for fp.div fp.sub fp.mul fp.abs
---
.../solve/smt_fp/sat/simple_add_float32.smt2 | 2 +-
.../solve/smt_fp/sat/simple_mul_float32.smt2 | 5 ++++
src_colibri2/theories/FP/float32.ml | 28 +++++++++++--------
src_colibri2/theories/FP/fp.ml | 6 ++++
src_colibri2/theories/FP/fp_value.ml | 1 -
src_colibri2/theories/FP/rounding_mode.ml | 4 +--
6 files changed, 30 insertions(+), 16 deletions(-)
create mode 100644 src_colibri2/tests/solve/smt_fp/sat/simple_mul_float32.smt2
diff --git a/src_colibri2/tests/solve/smt_fp/sat/simple_add_float32.smt2 b/src_colibri2/tests/solve/smt_fp/sat/simple_add_float32.smt2
index 6dc5136f7..6f0a55c4e 100644
--- a/src_colibri2/tests/solve/smt_fp/sat/simple_add_float32.smt2
+++ b/src_colibri2/tests/solve/smt_fp/sat/simple_add_float32.smt2
@@ -1,5 +1,5 @@
(set-logic ALL)
(declare-fun x () (_ FloatingPoint 8 24))
(declare-fun y () (_ FloatingPoint 8 24))
-(assert (= (fp.add RNE x y) (fp.add RNE x y)))
+(assert (= (fp.add RNE x y) x))
(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/sat/simple_mul_float32.smt2 b/src_colibri2/tests/solve/smt_fp/sat/simple_mul_float32.smt2
new file mode 100644
index 000000000..e0e38f673
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/simple_mul_float32.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-fun x () (_ FloatingPoint 8 24))
+(declare-fun y () (_ FloatingPoint 8 24))
+(assert (= (fp.mul 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 c05d22bae..063738b31 100644
--- a/src_colibri2/theories/FP/float32.ml
+++ b/src_colibri2/theories/FP/float32.ml
@@ -43,25 +43,26 @@ let init_ty d =
let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
let compute_ground d t =
-
- (* let mode = function
- | Expr.RoundNearestTiesToEven -> Farith.NE
- | Expr.RoundNearestTiesToAway -> Farith.NA
- | Expr.RoundTowardPositive -> Farith.UP
- | Expr.RoundTowardNegative -> Farith.DN
- | Expr.RoundTowardZero -> Farith.ZR
- | _ -> raise Impossible
- in *)
-
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
-
match Ground.sem t with
| { app = {builtin = Expr.Fp_add (8, 24); _}; args; _} ->
- (* TODO: get the mode *)
let m, a, b = IArray.extract3_exn args in
!< (Farith.B32.add !>>m !>a !>b)
+ | { app = {builtin = Expr.Fp_sub (8, 24); _}; args; _} ->
+ let m, a, b = IArray.extract3_exn args in
+ !< (Farith.B32.sub !>>m !>a !>b)
+ | { app = {builtin = Expr.Fp_mul (8, 24); _}; args; _} ->
+ let m, a, b = IArray.extract3_exn args in
+ !< (Farith.B32.mul !>>m !>a !>b)
+ | { app = {builtin = Expr.Fp_abs (8, 24); _}; args; _} ->
+ let a = IArray.extract1_exn args in
+ !< (Farith.B32.abs !>a)
+ | { app = {builtin = Expr.Fp_div (8, 24); _}; args; _} ->
+ 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)
| _ -> `None
let init_check d = Interp.Register.check d (fun d t ->
@@ -71,6 +72,9 @@ let init_check d = Interp.Register.check d (fun d t ->
match compute_ground d t with
| `None -> None
| `Some v -> Some (check v)
+ | `Uninterp ->
+ (* TODO : Give the control to the Uniterpreted Symbols theory *)
+ None
)
let init env =
diff --git a/src_colibri2/theories/FP/fp.ml b/src_colibri2/theories/FP/fp.ml
index ce8138c8f..bfe29e988 100644
--- a/src_colibri2/theories/FP/fp.ml
+++ b/src_colibri2/theories/FP/fp.ml
@@ -25,6 +25,12 @@ let converter d f =
match Ground.sem f with
| { app = {builtin = Expr.Fp_add (_, _); _}; args; _ } ->
IArray.iter ~f:reg args
+ | { app = {builtin = Expr.Fp_sub (_, _); _}; args; _ } ->
+ IArray.iter ~f:reg args
+ | { app = {builtin = Expr.Fp_div (_, _); _}; args; _ } ->
+ IArray.iter ~f:reg args
+ | { app = {builtin = Expr.Fp_mul (_, _); _}; args; _ } ->
+ IArray.iter ~f:reg args
| _ -> ()
let th_register env =
diff --git a/src_colibri2/theories/FP/fp_value.ml b/src_colibri2/theories/FP/fp_value.ml
index 471f575c1..067a95eb1 100644
--- a/src_colibri2/theories/FP/fp_value.ml
+++ b/src_colibri2/theories/FP/fp_value.ml
@@ -53,4 +53,3 @@ let posint_sequence_without_zero =
(** Generate the sequence of positive integers (without 0) *)
let posint_sequence =
Base.Sequence.shift_right posint_sequence_without_zero Z.zero
-
diff --git a/src_colibri2/theories/FP/rounding_mode.ml b/src_colibri2/theories/FP/rounding_mode.ml
index a45335f4e..ecb669935 100644
--- a/src_colibri2/theories/FP/rounding_mode.ml
+++ b/src_colibri2/theories/FP/rounding_mode.ml
@@ -82,7 +82,7 @@ let init_ty d =
let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
-let compute_ground _ t =
+let compute_cst t =
let (!<) v = `Some (Modes.nodevalue (Modes.index v)) in
match Ground.sem t with
| { app = {builtin = Expr.RoundNearestTiesToEven; _}; _} ->
@@ -101,7 +101,7 @@ let init_check d = Interp.Register.check d (fun d t ->
let check r =
Value.equal r (interp d (Ground.node t))
in
- match compute_ground d t with
+ match compute_cst t with
| `None -> None
| `Some v -> Some (check v)
)
--
GitLab