add two_matrix

src/dune

@@ -13,7 +13,7 @@
         (name wordgen_lib)
         (flags (:standard -w -27 -w -32))
         (instrumentation (backend bisect_ppx))
-        (modules puf semantic zoneGraph zoneGraphInput forward_reach prism_to_ta fl flq polynomial expPoly sampling outFormat low_disc_sampler)
+        (modules puf semantic zoneGraph zoneGraphInput forward_reach prism_to_ta fl flq polynomial expPoly sampling outFormat low_disc_sampler two_matrix)
         (libraries yojson zarith num xml-light symrob_extract common Prism)
 )
 

src/two_matrix.ml

+module Make (F : Fl.FSIG) = struct
+  type t = F.t * F.t * F.t * F.t
+
+  type vec = F.t * F.t
+
+  let ( *.. ) s (a, b, c, d) = (F.mul s a, F.mul s b, F.mul s c, F.mul s d)
+
+  let is_inv (a, b, c, d) = F.sub (F.mul a d) (F.mul b c) <> F.zero
+
+  let inv (a, b, c, d) =
+    let discr = F.sub (F.mul a d) (F.mul b c) in
+    let dm1 = F.div F.one discr in
+    dm1 *.. (d, F.neg b, F.neg c, a)
+
+  let norm_vec (x, y) = F.add (F.mul x x) (F.mul y y)
+
+  let sub_vec (a, b) (c, d) = (F.sub a c, F.sub b d)
+
+  let mul_vec (a, b, c, d) (x, y) =
+    (F.add (F.mul a x) (F.mul b y), F.add (F.mul c x) (F.mul d y))
+end

src/two_matrix.mli

+module Make : functor (F : Fl.FSIG) -> sig
+  type t = F.t * F.t * F.t * F.t
+
+  type vec = F.t * F.t
+
+  val ( *.. ) : F.t -> t -> t
+
+  val inv : t -> t
+
+  val is_inv : t -> bool
+
+  val norm_vec : vec -> F.t
+
+  val sub_vec : vec -> vec -> vec
+
+  val mul_vec : t -> vec -> vec
+end

src/wordgen.ml

@@ -140,7 +140,6 @@ let _ =
       (Format.formatter_of_out_channel fdot);
     close_out fdot );
 
-
   (* Compute z from expected_size *)
   let boltz =
     match !expected_size with
@@ -190,14 +189,13 @@ let _ =
   in
 
   ( match smp with
-   Some sparam when not FunIt.P.F.is_exact ->
+  | Some sparam when not FunIt.P.F.is_exact ->
       ZoneGraph.map_polynomials rgpoly (fun p ->
           FunIt.P.apply_const ?smp p FunIt.s (FunIt.P.F.of_float sparam))
-    |_ -> () );
+  | _ -> () );
 
-  if !print_rg && !verbose>4 then (
-      printf "%a@." (ZoneGraph.print Bound.print) rgpoly;
-    );
+  if !print_rg && !verbose > 4 then
+    printf "%a@." (ZoneGraph.print Bound.print) rgpoly;
 
   (* tidying up memory after the distribution computation*)
   Gc.compact ();