From 659fa7ba5bab735f34fa33949cf2d982f0f3537b Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 9 Sep 2022 22:16:59 -0400
Subject: [PATCH] wip: feat(lra): update to newer preprocessing

---
 src/algos/simplex/linear_expr.ml      | 6 ++++++
 src/algos/simplex/linear_expr_intf.ml | 3 +++
 src/th-lra/sidekick_th_lra.ml         | 5 ++---
 3 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/src/algos/simplex/linear_expr.ml b/src/algos/simplex/linear_expr.ml
index e7516754..4fc38827 100644
--- a/src/algos/simplex/linear_expr.ml
+++ b/src/algos/simplex/linear_expr.ml
@@ -95,6 +95,11 @@ module Make (C : COEFF) (Var : VAR) = struct
 
     let eval (subst : subst) (e : t) : C.t =
       Var_map.fold (fun x c acc -> C.(acc + (c * subst x))) e C.zero
+
+    let map ~f self : t =
+      Var_map.fold (fun v c acc -> add c (f v) acc) self empty
+
+    let of_list l = List.fold_left (fun e (c, x) -> add c x e) empty l
   end
 
   (** A linear arithmetic expression, composed of a combination of variables
@@ -121,6 +126,7 @@ module Make (C : COEFF) (Var : VAR) = struct
     let is_zero e = C.equal C.zero e.const && Comb.is_empty e.comb
     let is_const e = Comb.is_empty e.comb
     let map2 f g e e' = make (f e.comb e'.comb) (g e.const e'.const)
+    let map ~f e = make (Comb.map ~f e.comb) e.const
 
     module Infix = struct
       let ( + ) = map2 Comb.( + ) C.( + )
diff --git a/src/algos/simplex/linear_expr_intf.ml b/src/algos/simplex/linear_expr_intf.ml
index cff06aba..3f55cb5d 100644
--- a/src/algos/simplex/linear_expr_intf.ml
+++ b/src/algos/simplex/linear_expr_intf.ml
@@ -120,6 +120,8 @@ module type S = sig
     val add : C.t -> var -> t -> t
     (** [add n v t] adds the monome [n * v] to the combination [t]. *)
 
+    val map : f:(var -> var) -> t -> t
+
     (** Infix operations on combinations
 
         This module defines usual operations on linear combinations,
@@ -187,6 +189,7 @@ module type S = sig
     val make : Comb.t -> C.t -> t
     (** [make c n] makes the linear expression [c + n]. *)
 
+    val map : f:(var -> var) -> t -> t
     val monomial : C.t -> var -> t
     val monomial1 : var -> t
 
diff --git a/src/th-lra/sidekick_th_lra.ml b/src/th-lra/sidekick_th_lra.ml
index c3412a0d..0073ef4e 100644
--- a/src/th-lra/sidekick_th_lra.ml
+++ b/src/th-lra/sidekick_th_lra.ml
@@ -358,7 +358,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
       let box_t = Box.box self.tst t in
       let l1 = as_linexp t1 in
       let l2 = as_linexp t2 in
-      let le = LE.(l1 - l2) in
+      let le = LE.(l1 - l2) |> LE.map ~f:recurse in
       let le_comb, le_const = LE.comb le, LE.const le in
       let le_const = A.Q.neg le_const in
       let op = s_op_of_pred pred in
@@ -400,7 +400,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
       | None ->
         let box_t = Box.box self.tst t in
         (* we define these terms so their value in the model make sense *)
-        let le = as_linexp t in
+        let le = as_linexp t |> LE.map ~f:recurse in
         Term.Tbl.add self.simp_defined t (box_t, le);
         Some box_t)
     | LRA_const _n -> None
@@ -671,7 +671,6 @@ module Make (A : ARG) = (* : S with module A = A *) struct
     let changed = ref false in
     Iter.iter (add_trail_lit_ ~changed self si acts) trail;
 
-    (* add equalities between linear-expressions merged in the congruence closure *)
     ST_exprs.iter_all self.st_exprs (fun (_, l) ->
         Iter.diagonal_l l (fun (s1, s2) -> add_local_eq self si acts s1.n s2.n));