diff --git a/src_colibri2/theories/FP/dom_interval.ml b/src_colibri2/theories/FP/dom_interval.ml
new file mode 100644
index 0000000000000000000000000000000000000000..d0bb75203482e4a05d193cec4813295c31e2447d
--- /dev/null
+++ b/src_colibri2/theories/FP/dom_interval.ml
@@ -0,0 +1,285 @@
+(*************************************************************************)
+(* 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 = DomKind.create_key (module struct type t = D.t let name = "FP_ARITH" end)
+
+let () = DomKind.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 Egraph.print_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 Egraph.print_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 _ -> Egraph.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 = {
+ Egraph.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 Egraph.print_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.t -> 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.t -> 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 DomKind.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 ValueKind.Registered 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 wait =
+ Demon.Fast.register_simply "GotDomInterval"
+
+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 -> wait.for_dom d dom n wakeup) [a;b];
+ wait.for_value d Boolean.BoolValue.key r wakeup
+ 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 -> wait.for_dom d dom n 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 -> wait.for_dom d dom n 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 -> wait.for_dom d dom n 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 =
+ Demon.Fast.register_init_daemon_value
+ ~name:"Float32ToDomInterval"
+ (module Float32)
+ (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
+ ) env;
+ Ground.register_converter env converter
diff --git a/src_colibri2/theories/FP/dune b/src_colibri2/theories/FP/dune
index 60fb4f3eb59c4cbacb84ef17af276482f78d6e54..9c01e3f198496c7de542574af903c7e6a30486d7 100644
--- a/src_colibri2/theories/FP/dune
+++ b/src_colibri2/theories/FP/dune
@@ -10,6 +10,7 @@
colibri2.theories.helpers
colibri2.core.structures
colibri2.theories.bool
+ colibri2.theories.LRA.stages
colibri2.theories.quantifiers
colibri2.core)
(preprocess
diff --git a/src_colibri2/theories/FP/float32.ml b/src_colibri2/theories/FP/float32.ml
index 45591c00f79ea85b1fa61b30e9008f96589e7cb5..d612b15076b68c6e25b15108b266fda90ef6f872 100644
--- a/src_colibri2/theories/FP/float32.ml
+++ b/src_colibri2/theories/FP/float32.ml
@@ -26,6 +26,11 @@ module N32 = struct let name = "Float32" end
module Float32 = ValueKind.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)
*)
diff --git a/src_colibri2/theories/FP/float32.mli b/src_colibri2/theories/FP/float32.mli
index 51b03a489ade1b941073cae6020a125e70e17e85..c3900e1f43c164bbbf2b2b5499b79a55ebeb2c48 100644
--- a/src_colibri2/theories/FP/float32.mli
+++ b/src_colibri2/theories/FP/float32.mli
@@ -20,4 +20,8 @@
include ValueKind.Registered with type s = Farith.B32.t
+val cst': Farith.B32.t -> t
+
+val cst: Farith.B32.t -> Node.t
+
val init : Egraph.t -> unit
\ No newline at end of file