From 43a3e0760ed672d3ca5c47670ad147549f0a9be4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 11 Aug 2021 12:33:20 +0200
Subject: [PATCH] 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 | 38 +++++++++++++++---
src_colibri2/theories/LRA/dom_polynome.mli | 2 +-
src_colibri2/theories/LRA/dom_product.ml | 46 ++++++++++++++++++----
src_colibri2/theories/LRA/dom_product.mli | 2 +-
src_colibri2/theories/LRA/fourier.ml | 2 +-
src_colibri2/theories/LRA/pivot.ml | 26 ++++++------
src_colibri2/theories/LRA/pivot.mli | 4 +-
7 files changed, 88 insertions(+), 32 deletions(-)
diff --git a/src_colibri2/theories/LRA/dom_polynome.ml b/src_colibri2/theories/LRA/dom_polynome.ml
index 4b22129c3..9217b9591 100644
--- a/src_colibri2/theories/LRA/dom_polynome.ml
+++ b/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'
diff --git a/src_colibri2/theories/LRA/dom_polynome.mli b/src_colibri2/theories/LRA/dom_polynome.mli
index b88d42211..f9051653d 100644
--- a/src_colibri2/theories/LRA/dom_polynome.mli
+++ b/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
diff --git a/src_colibri2/theories/LRA/dom_product.ml b/src_colibri2/theories/LRA/dom_product.ml
index be0975b67..62d3bbffc 100644
--- a/src_colibri2/theories/LRA/dom_product.ml
+++ b/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
diff --git a/src_colibri2/theories/LRA/dom_product.mli b/src_colibri2/theories/LRA/dom_product.mli
index 3b2f1ac3c..df0dd22e7 100644
--- a/src_colibri2/theories/LRA/dom_product.mli
+++ b/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
diff --git a/src_colibri2/theories/LRA/fourier.ml b/src_colibri2/theories/LRA/fourier.ml
index 7f4daa6c1..311f557d4 100644
--- a/src_colibri2/theories/LRA/fourier.ml
+++ b/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
diff --git a/src_colibri2/theories/LRA/pivot.ml b/src_colibri2/theories/LRA/pivot.ml
index 5d5be6e49..c5199deb8 100644
--- a/src_colibri2/theories/LRA/pivot.ml
+++ b/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
diff --git a/src_colibri2/theories/LRA/pivot.mli b/src_colibri2/theories/LRA/pivot.mli
index 54857e51a..ee9fc5306 100644
--- a/src_colibri2/theories/LRA/pivot.mli
+++ b/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
--
GitLab