diff --git a/src_colibri2/core/colibri2_core.mli b/src_colibri2/core/colibri2_core.mli
index fa2dae87b9a9ca718374c53430487c80f2175c64..fb305ef40564018b60398ac415c18c011a75c4e1 100644
--- a/src_colibri2/core/colibri2_core.mli
+++ b/src_colibri2/core/colibri2_core.mli
@@ -442,7 +442,11 @@ and Value : sig
val of_nodevalue : Value.t -> t option
+ val of_value : s -> Value.t
+
val coerce_nodevalue : Value.t -> t
+
+ val coerce_value : Value.t -> s
end
module Register (T : Colibri2_popop_lib.Popop_stdlib.NamedDatatype) :
diff --git a/src_colibri2/core/structures/nodes.ml b/src_colibri2/core/structures/nodes.ml
index e64e0eab1076bc98f4d92fff51e38a9c73999d66..8325f5fb1b5d56c023a1a6bf1afaeb5ffed57223 100644
--- a/src_colibri2/core/structures/nodes.ml
+++ b/src_colibri2/core/structures/nodes.ml
@@ -178,7 +178,11 @@ module type RegisteredValue = sig
val of_nodevalue : Node.nodevalue -> t option
+ val of_value : s -> Node.nodevalue
+
val coerce_nodevalue : Node.nodevalue -> t
+
+ val coerce_value : Node.nodevalue -> s
end
module ValueRegistry = ValueKind.Make_Registry (struct
@@ -419,10 +423,14 @@ struct
| Node.Value (_, value', _) as v when ValueKind.equal value' key -> Some v
| _ -> None
+ let of_value v = nodevalue (index v)
+
let coerce_nodevalue : Value.t -> t = function
| Node.Value (_, value', _) as v ->
assert (ValueKind.equal value' key);
v
+
+ let coerce_value x = value (coerce_nodevalue x)
end
include All
diff --git a/src_colibri2/core/structures/nodes.mli b/src_colibri2/core/structures/nodes.mli
index 0740eff1a694076fd87a7c4f4e353f78034d57a9..1896052704f56f573edf96b602c6ea099f97da22 100644
--- a/src_colibri2/core/structures/nodes.mli
+++ b/src_colibri2/core/structures/nodes.mli
@@ -166,11 +166,14 @@ module type RegisteredValue = sig
val value : t -> s
(** Return the value from a nodevalue *)
- val nodevalue : t -> Value.t
+ val nodevalue: t -> Value.t
+ val of_nodevalue: Value.t -> t option
- val of_nodevalue : Value.t -> t option
+ val of_value: s -> Value.t
val coerce_nodevalue : Value.t -> t
+
+ val coerce_value: Value.t -> s
end
module RegisterValue (D : NamedDatatype) : RegisteredValue with type s = D.t
@@ -187,15 +190,15 @@ module Only_for_solver : sig
type sem_of_node = ThTerm : (_, 'b) ThTermKind.t * 'b -> sem_of_node
val thterm : Node.t -> ThTerm.t option
- (** give the sem associated with a node, make sense only for not merged
+ (** give the sem associated with a node, make sense only for not merged
class. So only the module solver can use it *)
val sem_of_node : ThTerm.t -> sem_of_node
- (** give the sem associated with a node, make sense only for not merged
+ (** give the sem associated with a node, make sense only for not merged
class. So only the module solver can use it *)
val nodevalue : Node.t -> Value.t option
- (** give the value associated with a node, make sense only for not merged
+ (** give the value associated with a node, make sense only for not merged
class. So only the module solver can use it *)
val node_of_thterm : ThTerm.t -> Node.t
diff --git a/src_colibri2/tests/solve/smt_fp/sat/dune b/src_colibri2/tests/solve/smt_fp/sat/dune
new file mode 100644
index 0000000000000000000000000000000000000000..137bdf589269179a3ae42355c4024e65ca273535
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/dune
@@ -0,0 +1,13 @@
+(include dune.inc)
+
+(rule
+ (alias runtest)
+ (deps
+ (glob_files *.cnf)
+ (glob_files *.smt2)
+ (glob_files *.psmt2))
+ (action
+ (with-stdout-to
+ dune.inc
+ (run %{exe:../../../generate_tests/generate_dune_tests.exe} . sat)))
+ (mode promote))
diff --git a/src_colibri2/tests/solve/smt_fp/sat/dune.inc b/src_colibri2/tests/solve/smt_fp/sat/dune.inc
new file mode 100644
index 0000000000000000000000000000000000000000..449d1077432c0cafa060be3b7b7bb1d6ca12c39a
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/dune.inc
@@ -0,0 +1,35 @@
+(rule (action (with-stdout-to oracle (echo "sat\n"))))
+(rule (action (with-stdout-to exists_eq_not_fp_eq.smt2.res (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 %{dep:exists_eq_not_fp_eq.smt2}))))
+(rule (alias runtest) (action (diff oracle exists_eq_not_fp_eq.smt2.res)))
+(rule (action (with-stdout-to inf_pos_neg_neq_float32.smt2.res (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 %{dep:inf_pos_neg_neq_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle inf_pos_neg_neq_float32.smt2.res)))
+(rule (action (with-stdout-to infm_eq_float32.smt2.res (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 %{dep:infm_eq_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle infm_eq_float32.smt2.res)))
+(rule (action (with-stdout-to infp_eq_float32.smt2.res (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 %{dep:infp_eq_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle infp_eq_float32.smt2.res)))
+(rule (action (with-stdout-to nan_neq_float32.smt2.res (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 %{dep:nan_neq_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle nan_neq_float32.smt2.res)))
+(rule (action (with-stdout-to recognize_float32.smt2.res (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 %{dep:recognize_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle recognize_float32.smt2.res)))
+(rule (action (with-stdout-to recognize_float64.smt2.res (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 %{dep:recognize_float64.smt2}))))
+(rule (alias runtest) (action (diff oracle recognize_float64.smt2.res)))
+(rule (action (with-stdout-to recognize_rounding_mode.smt2.res (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 %{dep:recognize_rounding_mode.smt2}))))
+(rule (alias runtest) (action (diff oracle recognize_rounding_mode.smt2.res)))
+(rule (action (with-stdout-to rm_instanciation.smt2.res (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 %{dep:rm_instanciation.smt2}))))
+(rule (alias runtest) (action (diff oracle rm_instanciation.smt2.res)))
+(rule (action (with-stdout-to rm_universal.smt2.res (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 %{dep:rm_universal.smt2}))))
+(rule (alias runtest) (action (diff oracle rm_universal.smt2.res)))
+(rule (action (with-stdout-to simple_add_float32.smt2.res (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 %{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} --size=10M --time=30s --max-steps 3500 %{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} --size=10M --time=30s --max-steps 3500 %{dep:simple_mul_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle simple_mul_float32.smt2.res)))
+(rule (action (with-stdout-to to_fp_eq_float32.smt2.res (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 %{dep:to_fp_eq_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle to_fp_eq_float32.smt2.res)))
+(rule (action (with-stdout-to zero_pos_neg_neq_float32.smt2.res (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 %{dep:zero_pos_neg_neq_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle zero_pos_neg_neq_float32.smt2.res)))
+(rule (action (with-stdout-to zerom_eq_float32.smt2.res (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 %{dep:zerom_eq_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle zerom_eq_float32.smt2.res)))
+(rule (action (with-stdout-to zerop_eq_float32.smt2.res (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 %{dep:zerop_eq_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle zerop_eq_float32.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_fp/sat/exists_eq_not_fp_eq.smt2 b/src_colibri2/tests/solve/smt_fp/sat/exists_eq_not_fp_eq.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..ab5587405feb8f2fe8a1e604ac03cd3cb53c1e6d
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/exists_eq_not_fp_eq.smt2
@@ -0,0 +1,4 @@
+(set-logic ALL)
+(assert (exists ((x (_ FloatingPoint 8 24)) (y (_ FloatingPoint 8 24)))
+ (and (= x y) (not (fp.eq x y)))))
+(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/sat/inf_pos_neg_neq_float32.smt2 b/src_colibri2/tests/solve/smt_fp/sat/inf_pos_neg_neq_float32.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..50d5f9ed42e6df44b1666710683c179c81e6ebd8
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/inf_pos_neg_neq_float32.smt2
@@ -0,0 +1,3 @@
+(set-logic ALL)
+(assert (not (fp.eq (_ +oo 8 24) (_ -oo 8 24))))
+(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/sat/infm_eq_float32.smt2 b/src_colibri2/tests/solve/smt_fp/sat/infm_eq_float32.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..d32861d4906d1fa6bc3d4e5070737bc0ae48cf26
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/infm_eq_float32.smt2
@@ -0,0 +1,3 @@
+(set-logic ALL)
+(assert (fp.eq (_ -oo 8 24) (_ -oo 8 24)))
+(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/sat/infp_eq_float32.smt2 b/src_colibri2/tests/solve/smt_fp/sat/infp_eq_float32.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..91101620ae68c22e4b68a4de338d6b81ba808631
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/infp_eq_float32.smt2
@@ -0,0 +1,3 @@
+(set-logic ALL)
+(assert (fp.eq (_ +oo 8 24) (_ +oo 8 24)))
+(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/sat/nan_neq_float32.smt2 b/src_colibri2/tests/solve/smt_fp/sat/nan_neq_float32.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..566d8821e60fd5b4c1d080fbcb0865a7e1ab8efd
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/nan_neq_float32.smt2
@@ -0,0 +1,3 @@
+(set-logic ALL)
+(assert (not (fp.eq (_ NaN 8 24) (_ NaN 8 24))))
+(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/sat/recognize_rounding_mode.smt2 b/src_colibri2/tests/solve/smt_fp/sat/recognize_rounding_mode.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..d2343304cbaaf0fe1bfc63eb7d2161d9b852827d
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/recognize_rounding_mode.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+(declare-fun rm1 () RoundingMode)
+(declare-fun rm2 () RoundingMode)
+(assert (= rm1 rm2))
+(check-sat)
+
diff --git a/src_colibri2/tests/solve/smt_fp/sat/rm_instanciation.smt2 b/src_colibri2/tests/solve/smt_fp/sat/rm_instanciation.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..f881999439bff2f9f5f5ca1f62afe46b6336c187
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/rm_instanciation.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+(declare-fun x () (_ FloatingPoint 8 24))
+(declare-fun y () (_ FloatingPoint 8 24))
+(declare-fun m () RoundingMode)
+(assert (not (= RNE m)))
+(assert (= (fp.add m x y) x))
+(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/sat/rm_universal.smt2 b/src_colibri2/tests/solve/smt_fp/sat/rm_universal.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..78a5beceda606d4b277bf2f590023a237712ce33
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/rm_universal.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-fun x () (_ FloatingPoint 8 24))
+(declare-fun y () (_ FloatingPoint 8 24))
+(assert (forall ((m RoundingMode)) (= (fp.add m x y) x)))
+(check-sat)
\ No newline at end of file
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
new file mode 100644
index 0000000000000000000000000000000000000000..6f0a55c4ef55157052764d0a2b7c12ed868ede9b
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/simple_add_float32.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-fun x () (_ FloatingPoint 8 24))
+(declare-fun y () (_ FloatingPoint 8 24))
+(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_eq_float32.smt2 b/src_colibri2/tests/solve/smt_fp/sat/simple_eq_float32.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..11abb9fe5b5a84f4ad0720a9e282a4cc74c5efd7
--- /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/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 0000000000000000000000000000000000000000..e0e38f6736112c5a4924579cd4cfa9b4897845de
--- /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/tests/solve/smt_fp/sat/to_fp_eq_float32.smt2 b/src_colibri2/tests/solve/smt_fp/sat/to_fp_eq_float32.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..e4402a93de6bedf59b71e5615bf66280f120d069
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/to_fp_eq_float32.smt2
@@ -0,0 +1,3 @@
+(set-logic ALL)
+(assert (fp.eq ((_ to_fp 8 24) RNE 1.0) ((_ to_fp 8 24) RNE 1.0)))
+(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/sat/zero_pos_neg_neq_float32.smt2 b/src_colibri2/tests/solve/smt_fp/sat/zero_pos_neg_neq_float32.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..510378baa30e26f198e94868794c6c43421a70aa
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/zero_pos_neg_neq_float32.smt2
@@ -0,0 +1,3 @@
+(set-logic ALL)
+(assert (fp.eq (_ +zero 8 24) (_ -zero 8 24)))
+(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/sat/zerom_eq_float32.smt2 b/src_colibri2/tests/solve/smt_fp/sat/zerom_eq_float32.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..1efb9d8cebcc7952df6fd12095e5e21c092b3cc9
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/zerom_eq_float32.smt2
@@ -0,0 +1,3 @@
+(set-logic ALL)
+(assert (fp.eq (_ -zero 8 24) (_ -zero 8 24)))
+(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/sat/zerop_eq_float32.smt2 b/src_colibri2/tests/solve/smt_fp/sat/zerop_eq_float32.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..b02b40f4719e076ffa01f85d2bb87e1a5e446904
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/zerop_eq_float32.smt2
@@ -0,0 +1,3 @@
+(set-logic ALL)
+(assert (fp.eq (_ +zero 8 24) (_ +zero 8 24)))
+(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/dune b/src_colibri2/tests/solve/smt_fp/unsat/dune
new file mode 100644
index 0000000000000000000000000000000000000000..6d9fe5883f08bc15b92dc715d3c58c193023dbb5
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/unsat/dune
@@ -0,0 +1,13 @@
+(include dune.inc)
+
+(rule
+ (alias runtest)
+ (deps
+ (glob_files *.cnf)
+ (glob_files *.smt2)
+ (glob_files *.psmt2))
+ (action
+ (with-stdout-to
+ dune.inc
+ (run %{exe:../../../generate_tests/generate_dune_tests.exe} . unsat)))
+ (mode promote))
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/dune.inc b/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
new file mode 100644
index 0000000000000000000000000000000000000000..d1c1e6097e0ef6a63763190775c76a334aa33c91
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
@@ -0,0 +1,7 @@
+(rule (action (with-stdout-to oracle (echo "unsat\n"))))
+(rule (action (with-stdout-to eq_fp_eq.smt2.res (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 %{dep:eq_fp_eq.smt2}))))
+(rule (alias runtest) (action (diff oracle eq_fp_eq.smt2.res)))
+(rule (action (with-stdout-to inf_pos_neg_neq.smt2.res (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 %{dep:inf_pos_neg_neq.smt2}))))
+(rule (alias runtest) (action (diff oracle inf_pos_neg_neq.smt2.res)))
+(rule (action (with-stdout-to nan_neq_float32.smt2.res (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 %{dep:nan_neq_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle nan_neq_float32.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/eq_fp_eq.smt2 b/src_colibri2/tests/solve/smt_fp/unsat/eq_fp_eq.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..92d9d453164614c9f3c1fcaab6d8e32dfa5660b7
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/unsat/eq_fp_eq.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+; (assert (forall ((x (_ FloatingPoint 8 24)) (y (_ FloatingPoint 8 24)))
+; (=> (fp.eq x y) (= x y))))
+; should be unsat because (= NaN NaN) is true but not (fp.eq Nan NaN)
+(assert (fp.eq (_ NaN 8 24) (_ NaN 8 24)))
+(check-sat)
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/f32_f64_incompatible.smt2 b/src_colibri2/tests/solve/smt_fp/unsat/f32_f64_incompatible.smt2
deleted file mode 100644
index fdc81481ad8535a4a8787e20ec17c8619f95328a..0000000000000000000000000000000000000000
--- a/src_colibri2/tests/solve/smt_fp/unsat/f32_f64_incompatible.smt2
+++ /dev/null
@@ -1,5 +0,0 @@
-(set-logic ALL)
-(declare-fun x () (_ FloatingPoint 11 53))
-(declare-fun y () (_ FloatingPoint 8 24))
-(assert (= x y))
-(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/inf_pos_neg_neq.smt2 b/src_colibri2/tests/solve/smt_fp/unsat/inf_pos_neg_neq.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..3e7669912bd18cd3f61847c639ba4a4174f88c9d
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/unsat/inf_pos_neg_neq.smt2
@@ -0,0 +1,3 @@
+(set-logic ALL)
+(assert (fp.eq (_ +oo 8 24) (_ -oo 8 24)))
+(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/nan_neq_float32.smt2 b/src_colibri2/tests/solve/smt_fp/unsat/nan_neq_float32.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..ceca02a3db99276bf132d8860e1c39d06cf8dafe
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/unsat/nan_neq_float32.smt2
@@ -0,0 +1,3 @@
+(set-logic ALL)
+(assert (fp.eq (_ NaN 8 24) (_ NaN 8 24)))
+(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/tests_fp.ml b/src_colibri2/tests/tests_fp.ml
index a9d8a4a57a00b8c28c056067576ffd1dbf2e0540..1c5c0a907056409c60f8e6e2aea3c4a1a747e8b3 100644
--- a/src_colibri2/tests/tests_fp.ml
+++ b/src_colibri2/tests/tests_fp.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
open OUnit2
open Colibri2_core
open Tests_lib
diff --git a/src_colibri2/theories/FP/dom_interval.ml b/src_colibri2/theories/FP/dom_interval.ml
new file mode 100644
index 0000000000000000000000000000000000000000..907ed8e5150432fdbaa75281473a81a3ae4767e2
--- /dev/null
+++ b/src_colibri2/theories/FP/dom_interval.ml
@@ -0,0 +1,279 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
+open Colibri2_popop_lib
+open Colibri2_core
+open Colibri2_stdlib.Std
+
+let debug = Debug.register_info_flag
+ ~desc:"for intervals for the floating points theory"
+ "FP.interval"
+
+module D = Colibri2_theories_LRA_stages.Interval_domain
+
+let dom = Dom.Kind.create (module struct type t = D.t let name = "FP_ARITH" end)
+
+let () = Dom.register(module struct
+ include D
+ let key = dom
+ let merged i1 i2 =
+ match i1, i2 with
+ | None, None -> true
+ | Some i1, Some i2 -> D.equal i1 i2
+ | _ -> false
+
+ let merge d (i1,cl1) (i2,cl2) _ =
+ assert (not (Egraph.is_equal d cl1 cl2));
+ match i1, cl1, i2, cl2 with
+ | Some i1,_, Some i2,_ ->
+ begin match D.inter i1 i2 with
+ | None ->
+ Debug.dprintf8 Debug.contradiction
+ "[FP/Dom] The intersection of %a and %a is empty when merging %a and %a"
+ D.pp i1 D.pp i2
+ Node.pp cl1
+ Node.pp cl2;
+ Egraph.contradiction d
+ | Some i ->
+ if not (D.equal i i1) then
+ Egraph.set_dom d dom cl1 i;
+ if not (D.equal i i2) then
+ Egraph.set_dom d dom cl2 i
+ end
+ | Some i1, _, _, cl2 | _, cl2, Some i1, _ ->
+ Egraph.set_dom d dom cl2 i1
+ | None,_,None,_ -> raise Impossible
+ end)
+
+let is_zero_or_positive d n =
+ match Egraph.get_dom d dom n with
+ | None -> false
+ | Some p -> match D.is_comparable D.zero p with
+ | D.Le | D.Lt -> true
+ | D.Ge | D.Gt | D.Uncomparable -> false
+
+let is_not_zero d n =
+ match Egraph.get_dom d dom n with
+ | None -> false
+ | Some p -> D.absent Q.zero p
+
+let is_strictly_positive d n =
+ match Egraph.get_dom d dom n with
+ | None -> false
+ | Some p -> match D.is_comparable D.zero p with
+ | D.Lt -> true
+ | D.Le | D.Ge | D.Gt | D.Uncomparable -> false
+
+let is_strictly_negative d n =
+ match Egraph.get_dom d dom n with
+ | None -> false
+ | Some p -> match D.is_comparable D.zero p with
+ | D.Gt -> true
+ | D.Le | D.Ge | D.Lt | D.Uncomparable -> false
+
+let is_integer d n =
+ match Egraph.get_dom d dom n with
+ | None -> false
+ | Some p -> D.is_integer p
+
+let set_dom d node v =
+ match D.is_singleton v with
+ | Some q ->
+ let cst = Float32.cst' (Farith.B32.(of_q NE q)) in
+ Egraph.set_value d node (Float32.nodevalue cst)
+ | None ->
+ (** the pexp must be in the dom *)
+ Egraph.set_dom d dom node v
+
+
+module ChoLRA = struct
+ let make_decision node v env =
+ Debug.dprintf4 Debug.decision
+ "[FP] decide %a on %a" D.pp v Node.pp node;
+ set_dom env node v
+
+ let choose_decision node env =
+ let v = Opt.get_def D.reals (Egraph.get_dom env dom node) in
+ match D.split_heuristic v with
+ | Singleton _ -> Choice.DecNo
+ | Splitted (v1,v2) ->
+ DecTodo (List.map (make_decision node) (Shuffle.shufflel [v1;v2]))
+ | NotSplitted ->
+ DecTodo [make_decision node (D.singleton (D.choose v))]
+
+ let choice n = {
+ Choice.prio = 1;
+ choice = choose_decision n;
+ }
+
+end
+
+let choice = ChoLRA.choice
+
+let upd_dom d n' v' =
+ match Egraph.get_dom d dom n' with
+ | None -> Egraph.set_dom d dom n' v'
+ | Some old ->
+ match D.inter old v' with
+ | None ->
+ Debug.dprintf6 Debug.contradiction
+ "[FP/Dom] The intersection of %a with %a is empty when updating %a"
+ D.pp old D.pp v'
+ Node.pp n';
+ Egraph.contradiction d
+ | Some d' ->
+ if not (D.equal old d')
+ then Egraph.set_dom d dom n' d'
+
+module Monad : sig
+ type 'a monad = Egraph.wt -> Node.t -> 'a
+ val get: Node.t -> D.t option monad
+ val set: Node.t -> D.t option monad -> unit monad
+ val getb: Node.t -> bool option monad
+ val setb: Node.t -> bool option option monad -> unit monad
+ val (let+): 'b option monad -> ('b -> 'c) -> 'c option monad
+ val (and+): 'b option monad -> 'c option monad -> ('b * 'c) option monad
+ val (&&): unit monad -> unit monad -> unit monad
+end = struct
+ type 'a monad = Egraph.wt -> Node.t -> 'a
+ let [@ocaml.always inline] get_dom dom n' = fun d _ ->
+ Egraph.get_dom d dom n'
+ let [@ocaml.always inline] set_dom (type b) (dom:b Dom.Kind.t) n' v' d n =
+ if Node.equal n n' then () else
+ Option.iter
+ (fun (v':b) -> Egraph.set_dom d dom n' v')
+ (v' d n)
+ let [@ocaml.always inline] set n' v' d n =
+ if Node.equal n n' then () else
+ Option.iter
+ (fun v' -> upd_dom d n' v' )
+ (v' d n)
+ let [@ocaml.always inline] get a = get_dom dom a
+ let [@ocaml.always inline] get_value key n' = fun d _ ->
+ let open CCOpt in
+ let* v = Egraph.get_value d n' in
+ Value.value key v
+ let [@ocaml.always inline] set_value (type b)
+ (value:(module Value.S with type s = b))
+ n' (v':b option option monad) : unit monad =
+ fun d n ->
+ if Node.equal n n' then () else
+ let module V = (val value) in
+ Option.iter
+ (Option.iter (fun v' -> Egraph.set_value d n' (V.nodevalue (V.index v'))))
+ (v' d n)
+ let getb a = get_value Boolean.dom a
+ let setb a = set_value (module Boolean.BoolValue) a
+ let [@ocaml.always inline] (let+) a (f:'b -> 'a) = fun d n -> Option.map f (a d n)
+ let [@ocaml.always inline] (and+) a b = fun d n -> match a d n, b d n with
+ | Some a, Some b -> Some (a,b) | _ -> None
+ let [@ocaml.always inline] (&&) a b = fun d n -> a d n; b d n
+
+end
+
+let neg_cmp = function
+ | `Lt -> `Ge
+ | `Le -> `Gt
+ | `Ge -> `Lt
+ | `Gt -> `Le
+
+let com_cmp = function
+ | `Lt -> `Gt
+ | `Le -> `Ge
+ | `Ge -> `Le
+ | `Gt -> `Lt
+
+let backward = function
+ | `Lt -> D.lt'
+ | `Gt -> D.gt'
+ | `Le -> D.le'
+ | `Ge -> D.ge'
+
+(** {2 Initialization} *)
+let converter d (f:Ground.t) =
+ let r = Ground.node f in
+ let reg n = Egraph.register d n in
+ let open Monad in
+ let cmp test cmp a b =
+ reg a; reg b;
+ let wakeup =
+ setb r (let+ va = get a and+ vb = get b in
+ test (D.is_comparable va vb)) &&
+ set b (let+ va = get a and+ vr = getb r in
+ backward (if vr then (com_cmp cmp) else (com_cmp (neg_cmp cmp))) va) &&
+ set a (let+ vb = get b and+ vr = getb r in
+ backward (if vr then cmp else (neg_cmp cmp)) vb)
+ in
+ List.iter (fun n -> Daemon.attach_dom d n dom wakeup) [a;b];
+ Daemon.attach_value d r Boolean.BoolValue.key (fun d n _ -> wakeup d n)
+ in
+ match Ground.sem f with
+ | { app = {builtin = Expr.Base; _ }; tyargs = _; args = _; ty }
+ when Ground.Ty.equal ty Ground.Ty.real ->
+ (* Egraph.register_decision d (ChoLRA.choice r) *) (* not useful for now *)
+ ()
+ | { app = {builtin = Expr.Base; _ }; tyargs = _; args = _; ty }
+ when Ground.Ty.equal ty Ground.Ty.int ->
+ upd_dom d r D.integers
+ | { app = {builtin = Expr.Add}; tyargs = []; args; _ } ->
+ let (a,b) = IArray.extract2_exn args in
+ reg a; reg b;
+ let wakeup =
+ set r (let+ va = get a and+ vb = get b in D.add va vb)
+ in
+ List.iter (fun n -> Daemon.attach_dom d n dom wakeup) [a; b; r]
+ | { app = {builtin = Expr.Sub}; tyargs = []; args; _ } ->
+ let (a,b) = IArray.extract2_exn args in
+ reg a; reg b;
+ let wakeup =
+ set r (let+ va = get a and+ vb = get b in D.minus va vb)
+ in
+ List.iter (fun n -> Daemon.attach_dom d n dom wakeup) [a; b; r]
+ | { app = {builtin = Expr.Minus}; tyargs = []; args; _ } ->
+ let a = IArray.extract1_exn args in
+ reg a;
+ let wakeup =
+ set r (let+ va = get a in D.mult_cst Q.minus_one va) &&
+ set a (let+ vr = get r in D.mult_cst Q.minus_one vr)
+ in
+ List.iter (fun n -> Daemon.attach_dom d n dom wakeup) [a;r]
+ | { app = {builtin = Expr.Lt}; tyargs = []; args; _ } ->
+ let a,b = IArray.extract2_exn args in
+ cmp (function | Uncomparable | Le -> None | Lt -> Some true | Ge | Gt -> Some false) `Lt a b
+ | { app = {builtin = Expr.Leq}; tyargs = []; args; _ } ->
+ let a,b = IArray.extract2_exn args in
+ cmp (function | Uncomparable | Ge -> None | Lt | Le -> Some true | Gt -> Some false) `Le a b
+ | { app = {builtin = Expr.Geq}; tyargs = []; args; _ } ->
+ let a,b = IArray.extract2_exn args in
+ cmp (function | Uncomparable | Le -> None | Lt -> Some false | Ge | Gt -> Some true) `Ge a b
+ | { app = {builtin = Expr.Gt}; tyargs = []; args; _ } ->
+ let a,b = IArray.extract2_exn args in
+ cmp (function | Uncomparable | Ge -> None | Lt | Le -> Some false | Gt -> Some true) `Gt a b
+ | _ -> ()
+
+let init env =
+ Daemon.attach_reg_value env
+ Float32.key
+ (fun d value ->
+ let v = Float32.value value in
+ let s = D.singleton (Farith.B32.to_q v) in
+ Egraph.set_dom d dom (Float32.node value) s
+ );
+ Ground.register_converter env converter
diff --git a/src_colibri2/theories/FP/dune b/src_colibri2/theories/FP/dune
index dc4d996e90e022c83d5f069872eaa67bf6dd1f5a..cbb3f787cb459924a1feec6571f6578d90eac56b 100644
--- a/src_colibri2/theories/FP/dune
+++ b/src_colibri2/theories/FP/dune
@@ -7,11 +7,19 @@
farith
colibri2.stdlib
colibri2.popop_lib
+ colibri2.theories.bool
+ colibri2.theories.LRA
+ colibri2.theories.LRA.stages
+ colibri2.theories.quantifiers
colibri2.core)
(preprocess
(pps ppx_deriving.std ppx_hash))
(flags
:standard
+ -w
+ +a-4-42-44-48-50-58-32-60-40-9@8
+ -color
+ always
-open
Containers
-open
@@ -19,6 +27,10 @@
-open
Std
-open
+ Colibri2_theories_bool
+ -open
+ Colibri2_theories_quantifiers
+ -open
Colibri2_core)
(ocamlopt_flags
:standard
diff --git a/src_colibri2/theories/FP/float32.ml b/src_colibri2/theories/FP/float32.ml
index 74b3dfd9305e32dbfe2ce73b8b6d1623d7dcd426..e4d919c80e45a1f267d9e63392cdbad7cfaaf9cf 100644
--- a/src_colibri2/theories/FP/float32.ml
+++ b/src_colibri2/theories/FP/float32.ml
@@ -19,29 +19,203 @@
(*************************************************************************)
open Fp_value
+open Colibri2_theories_LRA
+open Colibri2_popop_lib
+
module N32 = struct let name = "Float32" end
module Float32 = Value.Register(MakeFloat(Farith.B32)(N32))
include Float32
+let cst' c = index c
+
+let cst c = node (cst' c)
+
(** Initialise type interpretation
TODO : fix bounds (there is a finite set of 32 bits floats)
*)
let init_ty d =
+ let specials =
+ let open Base.Sequence.Generator in
+ let (let*) = (>>=) in
+ run (
+ let* _ = yield (Farith.B32.default_nan) in
+ let* _ = yield (Farith.B32.zero true) in
+ let* _ = yield (Farith.B32.zero false) in
+ let* _ = yield (Farith.B32.infm) in
+ yield (Farith.B32.infp))
+ in
+ let open Base.Sequence in
+ let finites = posint_sequence >>| Farith.B32.of_bits in
+ let fp_seq = append specials finites in
+ let fp_values = fp_seq >>| Float32.of_value in
Interp.Register.ty d (fun d ty ->
match ty with
| {app={builtin = Builtin.Float(8, 24);_};_} ->
- let seq =
- let open Interp.SeqLim in
- let+ e = of_seq d posint_sequence in
- (Farith.B32.of_bits e |> index |> nodevalue)
- in
- Some seq
+ let open Interp.SeqLim in
+ Some (of_seq d fp_values)
| _ -> None)
-(* TO DO : Initialise check *)
-(* let init_check d = Interp.Register.check d (...) *)
+let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
+
+let compute_ground d t =
+ let (!>>>) t = RealValue.coerce_value (interp d t) in
+ let (!>>) t = Rounding_mode.coerce_value (interp d t) in
+ let (!>) t = Float32.coerce_value (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.Real_to_fp (8, 24); _}; args; _} ->
+ let m, r = IArray.extract2_exn args in
+ !< (Farith.B32.of_q !>>m !>>>r)
+ | { app = {builtin = Expr.Plus_infinity (8, 24); _}; args; _} ->
+ assert (IArray.is_empty args);
+ !< (Farith.B32.infp)
+ | { app = {builtin = Expr.Minus_infinity (8, 24); _}; args; _} ->
+ assert (IArray.is_empty args);
+ !< (Farith.B32.infm)
+ | { app = {builtin = Expr.NaN (8, 24); _}; args; _} ->
+ assert (IArray.is_empty args);
+ !< (Farith.B32.(nan true Z.one))
+ | { app = {builtin = Expr.Plus_zero (8, 24); _}; args; _} ->
+ assert (IArray.is_empty args);
+ !< (Farith.B32.zerop)
+ | { app = {builtin = Expr.Minus_zero (8, 24); _}; args; _} ->
+ assert (IArray.is_empty args);
+ !< (Farith.B32.zero true)
+ | { app = {builtin = Expr.Fp_add (8, 24); _}; args; _} ->
+ 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)
+ | { 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 ->
+ let check r =
+ Value.equal r (interp d (Ground.node t))
+ in
+ match compute_ground d t with
+ | `None -> None
+ | `Some v -> Some (check v)
+ | `Uninterp ->
+ Some (Uninterp.On_uninterpreted_domain.check d t)
+ )
+
+let attach_interp d g =
+ let f d g =
+ match compute_ground d g with
+ | `None -> raise Impossible
+ | `Some v -> Egraph.set_value d (Ground.node g) v
+ | `Uninterp -> Uninterp.On_uninterpreted_domain.propagate d g
+ in
+ Interp.WatchArgs.create d f g
+
+let converter d (f:Ground.t) =
+ let r = Ground.node f in
+ let reg n = Egraph.register d n in
+ let merge n = Egraph.register d n; Egraph.merge d r n in
+ let open Monad in
+ let get a = Monad.getv Float32.key a in
+ let getq a = Monad.getv RealValue.key a in
+ let set a = Monad.setv Float32.key a in
+ let _getb a = Monad.getv Boolean.BoolValue.key a in
+ let setb a = Monad.setv Boolean.BoolValue.key a in
+ let (!>>) t = Rounding_mode.value (Rounding_mode.coerce_nodevalue (interp d t )) in
+ (* let (!>>>) t = RealValue.value (RealValue.coerce_nodevalue (interp d t )) in *)
+ let is_zero v = Farith.B32.(eq v (zero true) || eq v (zero false)) in
+ let cmp cmp a b =
+ reg a; reg b;
+ attach d (setb r (let+ va = get a and+ vb = get b in cmp va vb));
+ in
+ match Ground.sem f with
+ | {app={builtin=Expr.Real_to_fp (8, 24); _}; args; _} ->
+ let m, a = IArray.extract2_exn args in
+ reg m; reg a;
+ attach d (set r (let+ va = getq a in Farith.B32.of_q !>>m va));
+ | {app={builtin=Expr.NaN (8, 24); _}; args; _} ->
+ assert (IArray.is_empty args);
+ merge (cst (Farith.B32.nan true Z.one))
+ | {app={builtin=Expr.Plus_infinity (8, 24); _}; args; _} ->
+ assert (IArray.is_empty args);
+ merge (cst (Farith.B32.infp))
+ | {app={builtin=Expr.Minus_infinity (8, 24); _}; args; _} ->
+ assert (IArray.is_empty args);
+ merge (cst (Farith.B32.infm))
+ | {app={builtin=Expr.Plus_zero (8, 24); _}; args; _} ->
+ assert (IArray.is_empty args);
+ merge (cst (Farith.B32.zerop))
+ | {app={builtin=Expr.Minus_zero (8, 24); _}; args; _} ->
+ assert (IArray.is_empty args);
+ merge (cst (Farith.B32.zero true))
+ | {app={builtin=Expr.Fp_abs (8, 24); _}; args; _} ->
+ let a = IArray.extract1_exn args in
+ reg a; attach_interp d f;
+ attach d (set r (let+ va = get a in Farith.B32.abs va));
+ | {app={builtin=Expr.Fp_add (8, 24); _}; args; _} ->
+ let m, a, b = IArray.extract3_exn args in
+ reg m; reg a; reg b; attach_interp d f;
+ attach d (set r (let+ va = get a and+ vb = get b in Farith.B32.add !>>m va vb));
+ | {app={builtin=Expr.Fp_sub (8, 24); _}; args; _} ->
+ let m, a, b = IArray.extract3_exn args in
+ reg m; reg a; reg b; attach_interp d f;
+ attach d (set r (let+ va = get a and+ vb = get b in Farith.B32.sub !>>m va vb));
+ | {app={builtin=Expr.Fp_mul (8, 24); _}; args; _} ->
+ let m, a, b = IArray.extract3_exn args in
+ reg m; reg a; reg b; attach_interp d f;
+ attach d (
+ set r (let* va = get a and+ vb = get b in
+ if is_zero vb then None else Some (Farith.B32.mul !>>m va vb))
+ );
+ | {app={builtin=Expr.Fp_div (8, 24); _}; args; _} ->
+ let m, a, b = IArray.extract3_exn args in
+ reg m; reg a; reg b; attach_interp d f;
+ attach d (
+ set r (let* va = get a and+ vb = get b in
+ if is_zero vb then None else Some (Farith.B32.div !>>m va vb))
+ );
+ | {app={builtin=Expr.Fp_leq (8, 24); _}; args; _} ->
+ let a, b = IArray.extract2_exn args in
+ cmp Farith.B32.le a b; attach_interp d f;
+ | {app={builtin=Expr.Fp_gt (8, 24); _}; args; _} ->
+ let a, b = IArray.extract2_exn args in
+ cmp Farith.B32.gt a b; attach_interp d f;
+ | {app={builtin=Expr.Fp_geq (8, 24); _}; args; _} ->
+ let a, b = IArray.extract2_exn args in
+ cmp Farith.B32.ge a b; attach_interp d f;
+ | {app={builtin=Expr.Fp_eq (8, 24); _}; args; _} ->
+ let a, b = IArray.extract2_exn args in
+ cmp Farith.B32.eq a b; attach_interp d f;
+ | _ -> ()
+
let init env =
- init_ty env
+ Ground.register_converter env converter;
+ init_ty env;
+ init_check env
diff --git a/src_colibri2/theories/FP/float32.mli b/src_colibri2/theories/FP/float32.mli
index 3d9a3ffe1e876cf88dc01c56c96d5d4df1ace0ad..9f3efaae6112d8fd67db119080a51a67bd97f858 100644
--- a/src_colibri2/theories/FP/float32.mli
+++ b/src_colibri2/theories/FP/float32.mli
@@ -20,4 +20,8 @@
include Value.S with type s = Farith.B32.t
+val cst': Farith.B32.t -> t
+
+val cst: Farith.B32.t -> Node.t
+
val init : Egraph.wt -> unit
diff --git a/src_colibri2/theories/FP/fp.ml b/src_colibri2/theories/FP/fp.ml
index aa65f49318f733b293b83639f4b603ec2989d588..edd102b7cf47e01221870a9610de44a6e8a5ea3c 100644
--- a/src_colibri2/theories/FP/fp.ml
+++ b/src_colibri2/theories/FP/fp.ml
@@ -19,7 +19,10 @@
(*************************************************************************)
let th_register env =
- Float32.init env
+ Rounding_mode.init env;
+ Dom_interval.init env;
+ Float32.init env;
+ Float64.init env
(* Add the theory to defaults *)
let () =
diff --git a/src_colibri2/theories/FP/fp_value.mli b/src_colibri2/theories/FP/fp_value.mli
index 876601c9fb35d08360686845036b3e8a9ae4ef69..6c759aa446a375910404bdaba4f48383a5ed0b12 100644
--- a/src_colibri2/theories/FP/fp_value.mli
+++ b/src_colibri2/theories/FP/fp_value.mli
@@ -30,4 +30,4 @@ module type FloatName = sig val name : string end
Helper to extend a module of type [Farith.S] into a module of
type [Value.Kind.Value]
*)
-module MakeFloat (F : Farith.S) (N : FloatName) : Colibri2_popop_lib.Popop_stdlib.NamedDatatype with type t = F.t
+module MakeFloat (F : Farith.S) (_ : FloatName) : Colibri2_popop_lib.Popop_stdlib.NamedDatatype with type t = F.t
diff --git a/src_colibri2/theories/FP/rounding_mode.ml b/src_colibri2/theories/FP/rounding_mode.ml
new file mode 100644
index 0000000000000000000000000000000000000000..1d896b9f41d2afa67f10c01b8e08850f4db3ccdf
--- /dev/null
+++ b/src_colibri2/theories/FP/rounding_mode.ml
@@ -0,0 +1,126 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
+open Colibri2_popop_lib
+open Popop_stdlib
+
+module FarithModes = struct
+ let string_of_mode = function
+ | Farith.NE -> "RoundNearestTiesToEven"
+ | Farith.NA -> "RoundNearestTiesToAway"
+ | Farith.UP -> "RoundTowardPositive"
+ | Farith.DN -> "RoundTowardNegative"
+ | Farith.ZR -> "RoundTowardZero"
+
+ type t = Farith.mode
+
+ let hash = Hashtbl.hash
+
+ let compare = Stdlib.compare
+
+ let equal = Stdlib.(=)
+
+ let hash_fold_t s t = Base.Hash.fold_int s (hash t)
+
+ let sexp_of_t t = Base.Sexp.Atom (string_of_mode t)
+
+ let pp fmt t = Format.pp_print_string fmt (string_of_mode t)
+end
+
+module Modes = Value.Register(struct
+ include FarithModes
+ module M = Map.Make(FarithModes)
+ module S = Extset.MakeOfMap(M)
+ module H = XHashtbl.Make(FarithModes)
+ let name = "RoundingMode"
+ end)
+
+include Modes
+
+let rounding_mode_sequence =
+ let open Base.Sequence.Generator in
+ (
+ yield Farith.NE >>= fun () ->
+ yield Farith.NA >>= fun () ->
+ yield Farith.UP >>= fun () ->
+ yield Farith.DN >>= fun () ->
+ yield Farith.ZR
+ ) |> run
+
+let init_ty d =
+ Interp.Register.ty d (fun d ty ->
+ match ty with
+ | {app={builtin = Expr.RoundingMode;_};_} ->
+ let seq =
+ let open Interp.SeqLim in
+ let+ e = of_seq d rounding_mode_sequence in
+ (e |> index |> nodevalue)
+ in
+ Some seq
+ | _ -> None
+ )
+
+let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
+
+let compute_cst t =
+ let (!<) v = `Some (Modes.nodevalue (Modes.index v)) in
+ match Ground.sem t with
+ | { app = {builtin = Expr.RoundNearestTiesToEven; _}; _} ->
+ !< Farith.NE
+ | { app = {builtin = Expr.RoundNearestTiesToAway; _}; _} ->
+ !< Farith.NA
+ | { app = {builtin = Expr.RoundTowardNegative; _}; _} ->
+ !< Farith.DN
+ | { app = {builtin = Expr.RoundTowardPositive; _}; _} ->
+ !< Farith.UP
+ | { app = {builtin = Expr.RoundTowardZero; _}; _} ->
+ !< Farith.ZR
+ | _ -> `None
+
+let converter d f =
+ let r = Ground.node f in
+ let cst c = node (index c) in
+ let merge n = Egraph.register d n; Egraph.merge d r n in
+ match Ground.sem f with
+ | { app = {builtin = Expr.RoundNearestTiesToEven; _}; _} ->
+ merge (cst Farith.NE)
+ | { app = {builtin = Expr.RoundNearestTiesToAway; _}; _} ->
+ merge (cst Farith.NA)
+ | { app = {builtin = Expr.RoundTowardNegative; _}; _} ->
+ merge (cst Farith.DN)
+ | { app = {builtin = Expr.RoundTowardPositive; _}; _} ->
+ merge (cst Farith.UP)
+ | { app = {builtin = Expr.RoundTowardZero; _}; _} ->
+ merge (cst Farith.ZR)
+ | _ -> ()
+
+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_cst t with
+ | `None -> None
+ | `Some v -> Some (check v)
+ )
+
+let init env =
+ Ground.register_converter env converter;
+ init_ty env;
+ init_check env
diff --git a/src_colibri2/theories/FP/rounding_mode.mli b/src_colibri2/theories/FP/rounding_mode.mli
new file mode 100644
index 0000000000000000000000000000000000000000..07d44840f8cd6f6e13c76968fe8c592c546f77e1
--- /dev/null
+++ b/src_colibri2/theories/FP/rounding_mode.mli
@@ -0,0 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
+include Value.S with type s = Farith.mode
+
+val init : Egraph.wt -> unit