Sparsification of Affine Equality Matrix

src/analyses/apron/affineEqualityAnalysis.apron.ml

@@ -4,11 +4,14 @@
 
 open Analyses
 
+open SparseVector
+open ListMatrix
+
 include RelationAnalysis
 
 let spec_module: (module MCPSpec) Lazy.t =
   lazy (
-    let module AD = AffineEqualityDomain.D2 (VectorMatrix.ArrayVector) (VectorMatrix.ArrayMatrix) in
+    let module AD = AffineEqualityDomain.D2 (SparseVector) (ListMatrix) in
     let module Priv = (val RelationPriv.get_priv ()) in
     let module Spec =
     struct

src/cdomains/affineEquality/abstractMatrix.ml

@@ -0,0 +1,11 @@
+open RatOps
+open AbstractVector
+open Matrix
+
+(** Some functions inside have the suffix _with, which means that the function has side effects. *)
+module type AbstractMatrix =
+  functor (A: RatOps) (V: AbstractVector) ->
+  sig
+    include Matrix with type vec := V(A).t and type num := A.t
+  end
+

src/cdomains/affineEquality/abstractVector.ml

@@ -0,0 +1,9 @@
+open RatOps
+open Vector
+
+module type AbstractVector =
+  functor (A: RatOps) ->
+  sig
+    include Vector with type num:= A.t
+  end
+