Skip to content

Commit

Permalink
Simplify
Browse files Browse the repository at this point in the history
  • Loading branch information
michael-schwarz committed Jan 12, 2024
1 parent 022a9bc commit f99f320
Showing 1 changed file with 6 additions and 10 deletions.
16 changes: 6 additions & 10 deletions src/cdomains/apron/affineEqualityDomain.apron.ml
Original file line number Diff line number Diff line change
Expand Up @@ -680,19 +680,15 @@ struct

let invariant t =
let invariant m =
let earray = Lincons1.array_make t.env (Matrix.num_rows m) in
for i = 0 to (Lincons1.array_length earray -1) do
let one_constraint i =
let row = Matrix.get_row m i in
let coeff_vars = List.map (fun x -> Coeff.s_of_mpqf @@ Vector.nth row (Environment.dim_of_var t.env x), x) (vars t) in
let cst = Coeff.s_of_mpqf @@ Vector.nth row (Vector.length row - 1) in
Lincons1.set_list (Lincons1.array_get earray i) coeff_vars (Some cst)
done;
let {lincons0_array; array_env}: Lincons1.earray = earray in
Array.enum lincons0_array
|> Enum.map (fun (lincons0: Lincons0.t) ->
Lincons1.{lincons0; env = array_env}
)
|> List.of_enum
let e1 = Linexpr1.make t.env in
Linexpr1.set_list e1 coeff_vars (Some cst);
Lincons1.make e1 EQ
in
List.init (Matrix.num_rows m) (one_constraint)
in
BatOption.map_default invariant [] t.d

Expand Down

0 comments on commit f99f320

Please sign in to comment.