Use an external table for polynome/product to node

In order to not keep some and simplify the debug gui

src_colibri2/theories/LRA/dom_polynome.ml

@@ -34,9 +34,35 @@ end
 
 module ThE = ThTerm.Register (T)
 
-let node_of_polynome p =
+module Table = struct
+  module H = Datastructure.Hashtbl (T)
+
+  let h = H.create Node.pp "HARITH_POLY"
+
+  let set ~old_ ~new_ n d =
+    (match old_ with
+    | None -> ()
+    | Some old_ -> if not (Polynome.equal old_ new_) then H.remove h d old_);
+    H.change
+      (function
+        | None -> Some n
+        | Some n' as s ->
+            Egraph.merge d n n';
+            s)
+      h d new_
+
+  let new_ d p =
+    match H.find_opt h d p with
+    | Some n -> n
+    | None ->
+        let n = ThE.node (ThE.index p) in
+        H.set h d p n;
+        n
+end
+
+let node_of_polynome d p =
   match Polynome.is_cst p with
-  | None -> ThE.node (ThE.index p)
+  | None -> Table.new_ d p
   | Some q -> RealValue.node (RealValue.index q)
 
 include Pivot.Total (struct
@@ -56,11 +82,11 @@ include Pivot.Total (struct
     let add acc cl c = Polynome.x_p_cy acc c (f cl) in
     Polynome.fold add (Polynome.cst p.cst) p
 
-  let set d cl p =
-    match is_one_node p with
+  let set d cl ~old_ ~new_ =
+    match is_one_node new_ with
     | None -> (
-        match Polynome.is_cst p with
-        | None -> Egraph.set_thterm d cl (ThE.thterm (ThE.index p))
+        match Polynome.is_cst new_ with
+        | None -> Table.set ~old_ ~new_ cl d
         | Some q ->
             Egraph.set_value d cl (RealValue.nodevalue (RealValue.index q)))
     | Some cl' -> Egraph.merge d cl cl'

src_colibri2/theories/LRA/dom_polynome.mli

@@ -30,6 +30,6 @@ val events_repr_change :
 
 val init : Egraph.wt -> unit
 
-val node_of_polynome : Polynome.t -> Node.t
+val node_of_polynome : _ Egraph.t -> Polynome.t -> Node.t
 
 val normalize : _ Egraph.t -> Polynome.t -> Polynome.t

src_colibri2/theories/LRA/dom_product.ml

@@ -40,16 +40,42 @@ end
 
 module ThE = ThTerm.Register (T)
 
-let node_of_product abs sign =
+module Table = struct
+  module H = Datastructure.Hashtbl (T)
+
+  let h = H.create Node.pp "HARITH_PRODUCT"
+
+  let set ~old_ ~new_ d n =
+    if not (T.equal old_ new_) then H.remove h d old_;
+    H.change
+      (function
+        | None -> Some n
+        | Some n' as s ->
+            Egraph.merge d n n';
+            s)
+      h d new_
+
+  let new_ d p =
+    match H.find_opt h d p with
+    | Some n -> n
+    | None ->
+        let n = ThE.node (ThE.index p) in
+        H.set h d p n;
+        n
+end
+
+let node_of_product d abs sign =
   let t = { T.abs; sign } in
-  ThE.node (ThE.index t)
+  Table.new_ d t
 
-let set d cl abs sign =
+let set d cl ~old_abs ~old_sign abs sign =
   if Sign_product.equal Sign_product.zero sign then
     Egraph.merge d cl RealValue.zero
   else
     let aux () =
-      Egraph.set_thterm d cl (ThE.thterm (ThE.index { abs; sign }))
+      Table.set d cl
+        ~old_:{ T.abs = old_abs; sign = old_sign }
+        ~new_:{ T.abs; sign }
     in
     match Product.is_one_node abs with
     | None -> aux ()
@@ -85,7 +111,9 @@ end = Pivot.WithUnsolved (struct
     let p, c = subst p n q in
     if Q.is_zero c then None else Some p
 
-  let set d cl abs = SolveSign.iter_eqs d cl ~f:(fun sign -> set d cl abs sign)
+  let set d cl ~old_ ~new_ =
+    SolveSign.iter_eqs d cl ~f:(fun sign ->
+        set d cl ~old_abs:old_ ~old_sign:sign new_ sign)
 
   type data = Q.t
 
@@ -176,7 +204,9 @@ end = Pivot.WithUnsolved (struct
 
   let attach_info_change d f = Events.attach_any_dom d Dom_interval.dom f
 
-  let set d cl sign = SolveAbs.iter_eqs d cl ~f:(fun abs -> set d cl abs sign)
+  let set d cl ~old_ ~new_ =
+    SolveAbs.iter_eqs d cl ~f:(fun abs ->
+        set d cl ~old_abs:abs ~old_sign:old_ abs new_)
 
   type info = Sign_product.presolve * Sign_product.t
 
@@ -234,14 +264,14 @@ let factorize res a coef b d _ =
                 | NODE n, NODE n' when Egraph.is_equal d n n' ->
                     (cst, (n, v) :: acc)
                 | _ ->
-                    let n = node_of_product abs sign in
+                    let n = node_of_product d abs sign in
                     Egraph.register d n;
                     (cst, (n, v) :: acc))
               (Q.zero, [])
               [ (pa, sa, Q.one); (pb, sb, coef) ]
           in
           let p = Polynome.of_list cst l in
-          let n = Dom_polynome.node_of_polynome p in
+          let n = Dom_polynome.node_of_polynome d p in
           let pp_coef fmt coef =
             if Q.equal Q.one coef then Fmt.pf fmt "+" else Fmt.pf fmt "-"
           in

src_colibri2/theories/LRA/dom_product.mli

@@ -20,7 +20,7 @@
 
 (* val assume_equality : Egraph.wt -> Node.t -> Product.t -> unit *)
 
-val node_of_product : Product.t -> Sign_product.t -> Node.t
+val node_of_product : _ Egraph.t -> Product.t -> Sign_product.t -> Node.t
 
 module SolveAbs : sig
   val get_repr : _ Egraph.t -> Node.t -> Product.t option

src_colibri2/theories/LRA/fourier.ml

@@ -91,7 +91,7 @@ let divide d (p : Polynome.t) =
               | NODE n, NODE n' when Egraph.is_equal d n n' ->
                   (cst, (n, v) :: acc)
               | _ ->
-                  let n = Dom_product.node_of_product abs sign in
+                  let n = Dom_product.node_of_product d abs sign in
                   (cst, (n, v) :: acc))
             (Q.zero, []) l
         in

src_colibri2/theories/LRA/pivot.ml

@@ -55,7 +55,7 @@ module WithUnsolved (P : sig
 
   val solve : info -> info -> t solve_with_unsolved
 
-  val set : Egraph.wt -> Node.t -> t -> unit
+  val set : Egraph.wt -> Node.t -> old_:t -> new_:t -> unit
 end) : sig
   val assume_equality : Egraph.wt -> Node.t -> P.t -> unit
 
@@ -96,7 +96,7 @@ end = struct
 
   let set_poly d cl p chg =
     Egraph.set_dom d dom cl p;
-    List.iter (fun p -> P.set d cl p) chg
+    List.iter (fun (old_, new_) -> P.set d cl ~old_ ~new_) chg
 
   let add_used_product d cl' new_cls =
     Node.M.iter
@@ -143,7 +143,7 @@ end = struct
               in
               match P.subst q cl p with
               | None -> (new_cl, P.S.add q acc, chg)
-              | Some q -> (new_cl, P.S.add q acc, q :: chg)
+              | Some q' -> (new_cl, P.S.add q' acc, (q, q') :: chg)
             in
             let new_cl, acc, chg = fold (Node.M.empty, P.S.empty, []) q.repr in
             let repr = P.S.choose acc in
@@ -227,7 +227,7 @@ end = struct
       match po with
       | None ->
           add_used_product d cl (P.nodes eq);
-          set_poly d cl { repr = eq; eqs = P.S.empty } [ eq ]
+          set_poly d cl { repr = eq; eqs = P.S.empty } [ (eq, eq) ]
       | Some p -> (
           if (not (P.S.mem eq p.eqs)) && not (P.equal eq p.repr) then
             match
@@ -246,7 +246,7 @@ end = struct
                 let eqs = p.eqs |> P.S.add eq |> P.S.remove repr in
                 let p = { repr; eqs } in
                 add_used_product d cl (P.nodes eq);
-                set_poly d cl p [ eq ])
+                set_poly d cl p [ (eq, eq) ])
 
     and subst d cl eq =
       Debug.dprintf4 debug "[Pivot] subst %a with %a" Node.pp cl P.pp eq;
@@ -255,7 +255,7 @@ end = struct
       | None ->
           let p = { repr = eq; eqs = P.S.empty } in
           add_used_product d cl (P.nodes eq);
-          set_poly d cl p [ eq ]
+          set_poly d cl p [ (eq, eq) ]
       | Some p ->
           assert (Option.equal Node.equal (P.is_one_node p.repr) (Some cl));
           subst_doms d cl eq;
@@ -396,7 +396,7 @@ module Total (P : sig
 
   val solve : t -> t -> t solve_total
 
-  val set : Egraph.wt -> Node.t -> t -> unit
+  val set : Egraph.wt -> Node.t -> old_:t option -> new_:t -> unit
 end) : sig
   val assume_equality : Egraph.wt -> Node.t -> P.t -> unit
 
@@ -428,9 +428,9 @@ end = struct
   let used_in_poly : Node.t Bag.t Node.HC.t =
     Node.HC.create (Bag.pp Pp.semi Node.pp) "used_in_poly"
 
-  let set_poly d cl p =
-    Egraph.set_dom d dom cl p;
-    P.set d cl p
+  let set_poly d cl old_ new_ =
+    Egraph.set_dom d dom cl new_;
+    P.set d cl ~old_ ~new_
 
   let add_used d cl' new_cl =
     Node.M.iter
@@ -463,12 +463,12 @@ end = struct
         | None -> assert false (* absurd: can't be used and absent *)
         | Some q ->
             let new_cl = Node.M.set_diff (P.nodes p) (P.nodes q) in
-            let q = P.subst q cl p in
+            let q_new = P.subst q cl p in
             add_used d cl' new_cl;
-            set_poly d cl' q)
+            set_poly d cl' (Some q) q_new)
       b;
     add_used d cl (P.nodes p);
-    set_poly d cl p
+    set_poly d cl None p
 
   module Th = struct
     include P

src_colibri2/theories/LRA/pivot.mli

@@ -69,7 +69,7 @@ module WithUnsolved (P : sig
   (** [solve t1 t2] solve the equation [t1 = t2] by returning a substitution.
         Return Unsolved if the equation can't be yet solved *)
 
-  val set : Egraph.wt -> Node.t -> t -> unit
+  val set : Egraph.wt -> Node.t -> old_:t -> new_:t -> unit
   (** Called a new term equal to this node is found *)
 end) : sig
   val assume_equality : Egraph.wt -> Node.t -> P.t -> unit
@@ -125,7 +125,7 @@ module Total (P : sig
   val solve : t -> t -> t solve_total
   (** [solve t1 t2] solve the equation [t1 = t2] by returning a substitution. *)
 
-  val set : Egraph.wt -> Node.t -> t -> unit
+  val set : Egraph.wt -> Node.t -> old_:t option -> new_:t -> unit
   (** Called a new term equal to this node is found *)
 end) : sig
   val assume_equality : Egraph.wt -> Node.t -> P.t -> unit