Add general disequality hook

    Just partially connected to existing theory

.vscode/tasks.json

@@ -7,7 +7,7 @@
 				"$ocamlc"
 			],
 			"group": {
-				"kind": "test",
+				"kind": "build",
 				"isDefault": true
 			},
 			"label": "dune: build @runtest"

colibri2.opam

@@ -8,6 +8,7 @@ authors: [
   "Bruno Marre"
   "Guillaume Bury"
   "Stéphane Graham-Lengrand"
+  "Hichem Ait El Hara"
 ]
 license: "LGPL-2.1-only"
 homepage: "https://colibri.frama-c.com"

colibri2/popop_lib/bag.ml

@@ -31,6 +31,7 @@ type 'a t =
   | App of 'a t * 'a
   | List of 'a list
   | Concat of 'a t * 'a t
+  [@@ deriving eq]
 
 let empty = Empty
 let elt x = Elt x
@@ -222,4 +223,4 @@ let rec collect t xs =
 
 let elements t = collect t []
 
-let pp sep pelt fmt t = Pp.iter1 iter sep pelt fmt t
+let pp pelt fmt t = Pp.iter1 iter Pp.comma pelt fmt t

colibri2/popop_lib/bag.mli

@@ -24,7 +24,8 @@
     @since Carbon-20101201
 *)
 
-type 'a t
+type 'a t  [@@ deriving eq]
+
 
 val empty : 'a t
 val elt : 'a -> 'a t
@@ -58,6 +59,5 @@ val elements : 'a t -> 'a list
 val choose: 'a t -> 'a
 
 val pp:
-  (unit Pp.pp) ->
   ('a Pp.pp) ->
   'a t Pp.pp

colibri2/theories/LRA/dom_polynome.ml

@@ -136,4 +136,11 @@ let init env =
       let cl = RealValue.node value in
       let p1 = Polynome.of_list v [] in
       assume_equality d cl p1);
-  Ground.register_converter env converter
+  Ground.register_converter env converter;
+  Disequality.register_disequal env (fun d n1 n2 ->
+      match (get_repr d n1, get_repr d n2) with
+      | Some p1, Some p2 -> (
+          match Polynome.is_cst (Polynome.sub p1 p2) with
+          | Some c when A.is_not_zero c -> true
+          | _ -> false)
+      | _ -> false)

colibri2/theories/LRA/pivot.ml

@@ -446,7 +446,7 @@ end = struct
       end)
 
   let used_in_poly : Node.t Bag.t Node.HC.t =
-    Node.HC.create (Bag.pp Pp.semi Node.pp) "used_in_poly"
+    Node.HC.create (Bag.pp Node.pp) "used_in_poly"
 
   let set_poly d cl old_ new_ =
     Egraph.set_dom d dom cl new_;

colibri2/theories/array/array.ml

@@ -247,14 +247,14 @@ let init env =
   if Options.get env restrict_ext then
     if Options.get env use_diff_graph then (
       (* (a = b) ≡ false |> (a[k] ≠ b[k]) (when a and b are neighbours) *)
-      Equality.register_hook_new_disequality env (apply_res_ext_1_2 env);
+      Equality.register_hook_new_disequality env apply_res_ext_1_2;
       (* a, b, {a,b} ⊆ foreign |> (a = b) ⋁ (a[k] ≠ b[k])
          (when a and b are neighbours) *)
       Foreign_dom.register_hook_new_foreign_array env (apply_res_ext_2_2 env))
     else (
       (* (a = b) ≡ false |> (a[k] ≠ b[k]) *)
       (* TODO: Are a and b always of the same type? *)
-      Equality.register_hook_new_disequality env (apply_res_ext_1_1 env);
+      Equality.register_hook_new_disequality env apply_res_ext_1_1;
       (* a, b, {a,b} ⊆ foreign |> (a = b) ⋁ (a[k] ≠ b[k]) *)
       Foreign_dom.register_hook_new_foreign_array env (apply_res_ext_2_1 env));
   let l = [ (adown_pattern, adown_run) ] in

colibri2/theories/bool/disequality.ml

+(*************************************************************************)
+(*  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_core
+
+let disequal_hook = Datastructure.Push.create Fmt.nop "disequal_hook"
+
+let register_disequal d f = Datastructure.Push.push disequal_hook d f
+
+let update_hook = Datastructure.Push.create Fmt.nop "update_hook"
+
+let register_update d f = Datastructure.Push.push update_hook d f
+
+let is_disequal d n1 n2 =
+  try
+    Datastructure.Push.iter ~f:(fun f -> if f d n1 n2 then raise Exit)
+       disequal_hook d;
+    false
+  with Exit -> true
+
+let update_disequality d n1 check =
+  Datastructure.Push.iter ~f:(fun f -> f d n1 check )
+    update_hook d;

colibri2/theories/bool/disequality.mli

+(*************************************************************************)
+(*  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).           *)
+(*************************************************************************)
+
+val is_disequal: Egraph.wt -> Node.t -> Node.t -> bool
+(** [is_disequal d n1 n2] indicates if n1 and n2 are known to be distinct *)
+
+val register_disequal: Egraph.wt -> 
+ (Egraph.wt -> Node.t -> Node.t -> bool)
+  -> unit
+(** [register_disequal f d] Register function [f] to test disequality *)
+
+val update_disequality:
+ Egraph.wt -> Node.t ->  (Egraph.wt -> Node.t -> bool) ->
+  unit
+(** [update_disequality upd d n] warn that the disequality with [n] could have
+  changed
+  *) 
+
+val register_update:
+Egraph.wt -> (Egraph.wt -> Node.t -> (Egraph.wt -> Node.t -> bool) -> unit) -> unit
+
+(** [new_daemon d f] registers a function [f] where [f n1 g] is called when the
+      disequalities of n1 could have changed, [g] allows to check for such
+      new or not disequalities.
+*)

colibri2/theories/bool/dune

@@ -2,7 +2,6 @@
  (name colibri2_theories_bool)
  (public_name colibri2.theories.bool)
  (synopsis "theories for colibri2")
- (modules Boolean Equality)
  (libraries
   containers
   ocamlgraph

colibri2/theories/bool/equality.ml

@@ -224,7 +224,12 @@ let add_new_tag d the s =
   let _dis, stag = new_tag the in
   Debug.dprintf2 debug "[Dis: %a]" Dis.pp (stag ());
   Node.S.iter (fun cl -> set_dom d cl (stag ())) s;
-  Datastructure.Push.iter add_new_tag_hooks d ~f:(fun f -> f s)
+  Node.S.iter
+     (fun n1 ->
+       Disequality.update_disequality d n1
+        (fun d n2 -> not (Egraph.is_equal d n1 n2) && Node.S.mem n2 s))
+  s;
+  Datastructure.Push.iter add_new_tag_hooks d ~f:(fun f -> f d s)
 
 exception Found of Node.t * Node.t
 
@@ -560,6 +565,7 @@ let th_register env =
   Ground.register_converter env converter;
   bool_init_diff_to_value env;
   Check.init_check env;
+  Disequality.register_disequal env is_disequal;
   ()
 
 let () = Init.add_default_theory th_register

colibri2/theories/bool/equality.mli

@@ -26,7 +26,9 @@ val is_disequal : _ Egraph.t -> Node.t -> Node.t -> bool
 val iter_on_value_different :
   they_are_different:(Node.t -> Value.t -> unit) -> Egraph.wt -> Node.t -> unit
 
-val register_hook_new_disequality : _ Egraph.t -> (Node.S.t -> unit) -> unit
+val register_hook_new_disequality : _ Egraph.t -> (Egraph.wt -> Node.S.t -> unit) -> unit
 (** register a hook that is called each time a set of nodes is known to be disequal *)
 
 val th_register : Egraph.wt -> unit
+
+