Project

General

Profile

« Previous | Next » 

Revision 3d1f9d9f

Added by LĂ©lio Brun over 2 years ago

more agressive optim propagation in spec in order to remove unecessarry existential variables that were eliminated (helps the solvers)

View differences:

src/spec_common.ml
6 6

  
7 7
let is_false = function False -> true | _ -> false
8 8

  
9
let type_of_l_value = function
9
let type_of_value = function
10
  | Val v -> v.Machine_code_types.value_type
11
  | Tag (_, t) -> t
10 12
  | Var v ->
11 13
    v.var_type
12 14
  | Memory ResetFlag ->
13 15
    Type_predef.type_bool
14 16
  | Memory (StateVar v) ->
15 17
    v.var_type
16
  | _ -> assert false
17 18

  
18
let expr_eq a b =
19
  match a, b with
20
  | Var x, Var y ->
21
    x = y
22
  | Memory r1, Memory r2 ->
23
    r1 = r2
24
  | _ ->
25
    false
19
let expr_eq a b = a = b
20
  (* match a, b with *)
21
  (* | Var x, Var y -> *)
22
  (*   x = y *)
23
  (* | Memory r1, Memory r2 -> *)
24
  (*   r1 = r2 *)
25
  (* | _ -> *)
26
  (*   false *)
26 27

  
27 28
let rec red = function
28 29
  | Equal (a, b) when expr_eq a b ->
......
124 125
  | hl ->
125 126
    let n = List.length hl in
126 127
    And (List.mapi (fun k (t, spec) ->
127
        let c = if k = n - 1 then GEqual (Var x, Tag t) else Equal (Var x, Tag t) in
128
        let tag = Tag (t, x.var_type) in
129
        let x = Var x in
130
        let c = if k = n - 1 then GEqual (x, tag) else Equal (x, tag) in
128 131
        Imply (c, spec)) hl)
129 132

  
130 133
let mk_assign_tr x v = Equal (Var x, Val v)

Also available in: Unified diff