From 31065ed0addc6471416ae81b8b915f04dda9eb42 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 27 Dec 2023 19:47:11 +0100
Subject: [PATCH] Make computations in show directly on Z

---
 .../apron/affineEqualityDomain.apron.ml       | 50 ++++++++++---------
 1 file changed, 26 insertions(+), 24 deletions(-)

diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 4f47f6f494..a1653bb423 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -230,39 +230,41 @@ struct
 
   let show t =
     let conv_to_ints row =
-      let module BI = IntOps.BigIntOps in
-      let row = Array.copy @@ Vector.to_array row
-      in
-      for i = 0 to Array.length row -1 do
-        let val_i = Mpqf.of_mpz @@ Z_mlgmpidl.mpzf_of_z @@ Mpqf.get_den row.(i)
-        in Array.iteri(fun j x -> row.(j) <- val_i *: x)  row
-      done;
-      let int_arr = Array.init (Array.length row) (fun i -> Mpqf.get_num row.(i))
-      in let div = Mpqf.of_mpz @@ Z_mlgmpidl.mpzf_of_z @@ Array.fold_left BI.gcd int_arr.(0) int_arr
-      in Array.iteri (fun i x -> row.(i) <- x /: div) row;
-      Vector.of_array @@ row
+      let row = Array.copy @@ Vector.to_array row in
+      let mpqf_of_z x = Mpqf.of_mpz @@ Z_mlgmpidl.mpzf_of_z x in
+      let lcm = mpqf_of_z @@ Array.fold_left (fun x y -> Z.lcm x (Mpqf.get_den y)) Z.one row in
+      Array.modify (fun x -> x *: lcm) row;
+      let int_arr = Array.map (fun x -> Mpqf.get_num x) row in
+      let div = Array.fold_left Z.gcd int_arr.(0) int_arr in
+      Array.modify (fun x -> Z.div x div) int_arr;
+      int_arr
     in
-    let vec_to_constraint vec env =
+    let vec_to_constraint arr env =
       let vars, _ = Environment.vars env in 
       let dim_to_str var =
-        let vl =  Vector.nth vec (Environment.dim_of_var env var) in 
+        let vl =  arr.(Environment.dim_of_var env var) in 
         let var_str = Var.to_string var in 
-        if vl =: Mpqf.one then "+" ^ var_str
-        else if vl =: Mpqf.mone then "-" ^ var_str
-        else if vl <: Mpqf.mone then Mpqf.to_string vl ^ var_str
-        else if vl >: Mpqf.one then Format.asprintf "+%s" (Mpqf.to_string vl) ^ var_str
-        else ""
+        if Z.equal vl Z.zero then 
+          ""
+        else if Z.equal vl Z.one then 
+          "+" ^ var_str
+        else if Z.equal vl Z.minus_one then 
+          "-" ^ var_str
+        else if Z.lt vl Z.minus_one then
+          Z.to_string vl ^ var_str
+        else
+          Format.asprintf "+%s" (Z.to_string vl) ^ var_str
       in
-      let c_to_str vl =
-        if vl =: Mpqf.zero then 
+      let const_to_str vl =
+        if Z.equal vl Z.zero then 
           ""
         else
-          let negated = vl *: Mpqf.mone in
-          if negated >: Mpqf.zero then "+" ^ Mpqf.to_string negated
-          else Mpqf.to_string negated
+          let negated = Z.mul vl Z.minus_one in
+          if Z.gt negated Z.zero then "+" ^ Z.to_string negated
+          else Z.to_string negated
       in
       let res = (String.concat "" @@ Array.to_list @@ Array.map dim_to_str vars)
-                ^ (c_to_str @@ Vector.nth vec (Vector.length vec - 1)) ^ "=0" in 
+                ^ (const_to_str arr.(Array.length arr - 1)) ^ "=0" in 
       if String.starts_with res "+" then 
         String.sub res 1 (String.length res - 1)
       else