Project

General

Profile

Download (2.68 KB) Statistics
| Branch: | Tag: | Revision:
1
open Spec_types
2

    
3
(* a small reduction engine *)
4
let is_true = function
5
  | True -> true
6
  | _ -> false
7

    
8
let is_false = function
9
  | False -> true
10
  | _ -> false
11

    
12
let expr_eq: type a b. (a, left_v) expression_t -> (a, b) expression_t -> bool =
13
  fun a b ->
14
  match a, b with
15
  | Var x, Var y -> x = y
16
  | Memory r1, Memory r2 -> r1 = r2
17
  | _ -> false
18

    
19
let rec red: type a. a formula_t -> a formula_t = function
20
  | Equal (a, b) when expr_eq a b ->
21
    True
22

    
23
  | And l ->
24
    let l' = List.filter_map (fun a ->
25
        let a' = red a in
26
        if is_true a' then None else Some a') l in
27
    begin match l' with
28
      | [] -> True
29
      | [a] -> a
30
      | l' when List.exists is_false l' -> False
31
      | _ -> And l'
32
    end
33

    
34
  | Or l ->
35
    let l' = List.filter_map (fun a ->
36
        let a' = red a in
37
        if is_false a' then None else Some a') l in
38
    begin match l' with
39
      | [] -> assert false
40
      | [a] -> a
41
      | l' when List.exists is_true l' -> True
42
      | _ -> Or l'
43
    end
44

    
45
  | Imply (a, b) ->
46
    let a' = red a in
47
    let b' = red b in
48
    if a' = b' || is_false a' || is_true b' then True
49
    else if is_true a' && is_false b' then False
50
    else Imply (a', b')
51

    
52
  | Exists (x, p) ->
53
    let p' = red p in
54
    if is_true p' then True else begin match x with
55
      | [] -> p'
56
      | x -> Exists (x, p')
57
    end
58

    
59
  | Forall (x, p) ->
60
    let p' = red p in
61
    if is_true p' then True else begin match x with
62
      | [] -> p'
63
      | x -> Forall (x, p')
64
    end
65

    
66
  | Ternary (x, a, b) ->
67
    let a' = red a in
68
    let b' = red b in
69
    Ternary (x, a', b')
70

    
71
  | f -> f
72

    
73
(* smart constructors *)
74
(* let mk_condition x l =
75
 *   if l = tag_true then Ternary (Val x, True, False)
76
 *   else if l = tag_false then Ternary (Val x, False, True)
77
 *   else Equal (Val x, Tag l) *)
78

    
79
let vals vs = List.map (fun v -> Val v) vs
80

    
81
let mk_pred_call pred =
82
  Predicate pred
83

    
84
(* let mk_clocked_on id =
85
 *   mk_pred_call (Clocked_on id) *)
86

    
87
let mk_transition ?(mems=Utils.ISet.empty) ?r ?i ?inst id inputs locals outputs =
88
  let tr =
89
    mk_pred_call
90
      (Transition (id, inst, i, vals inputs, vals locals, vals outputs,
91
                  (match r with Some _ -> true | None -> false), mems)) in
92
    (match r, inst with
93
     | Some r, Some inst ->
94
       ExistsMem (id, mk_pred_call (Reset (id, inst, r)), tr)
95
     | _ ->
96
       tr)
97

    
98
let mk_memory_pack ?i ?inst id =
99
  mk_pred_call (MemoryPack (id, inst, i))
100

    
101
let mk_state_variable_pack x =
102
  StateVarPack (StateVar x)
103

    
104
let mk_state_assign_tr x v =
105
  Equal (Memory (StateVar x), Val v)
106

    
107
let mk_conditional_tr v t f =
108
  Ternary (Val v, t, f)
109

    
110
let mk_branch_tr x hl =
111
  And (List.map (fun (t, spec) -> Imply (Equal (Var x, Tag t), spec)) hl)
112

    
113
let mk_assign_tr x v =
114
  Equal (Var x, Val v)
115

    
(57-57/66)