1
|
open Spec_types
|
2
|
|
3
|
(* a small reduction engine *)
|
4
|
let is_true = function True -> true | _ -> false
|
5
|
|
6
|
let is_false = function False -> true | _ -> false
|
7
|
|
8
|
let expr_eq : type a b. (a, left_v) expression_t -> (a, b) expression_t -> bool
|
9
|
=
|
10
|
fun a b ->
|
11
|
match a, b with
|
12
|
| Var x, Var y ->
|
13
|
x = y
|
14
|
| Memory r1, Memory r2 ->
|
15
|
r1 = r2
|
16
|
| _ ->
|
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
|
| And l -> (
|
23
|
let l' =
|
24
|
List.filter_map
|
25
|
(fun a ->
|
26
|
let a' = red a in
|
27
|
if is_true a' then None else Some a')
|
28
|
l
|
29
|
in
|
30
|
match l' with
|
31
|
| [] ->
|
32
|
True
|
33
|
| [ a ] ->
|
34
|
a
|
35
|
| l' when List.exists is_false l' ->
|
36
|
False
|
37
|
| _ ->
|
38
|
And l')
|
39
|
| Or l -> (
|
40
|
let l' =
|
41
|
List.filter_map
|
42
|
(fun a ->
|
43
|
let a' = red a in
|
44
|
if is_false a' then None else Some a')
|
45
|
l
|
46
|
in
|
47
|
match l' with
|
48
|
| [] ->
|
49
|
assert false
|
50
|
| [ a ] ->
|
51
|
a
|
52
|
| l' when List.exists is_true l' ->
|
53
|
True
|
54
|
| _ ->
|
55
|
Or l')
|
56
|
| Imply (a, b) ->
|
57
|
let a' = red a in
|
58
|
let b' = red b in
|
59
|
if a' = b' || is_false a' || is_true b' then True
|
60
|
else if is_true a' && is_false b' then False
|
61
|
else Imply (a', b')
|
62
|
| Exists (x, p) -> (
|
63
|
let p' = red p in
|
64
|
if is_true p' then True else match x with [] -> p' | x -> Exists (x, p'))
|
65
|
| Forall (x, p) -> (
|
66
|
let p' = red p in
|
67
|
if is_true p' then True else match x with [] -> p' | x -> Forall (x, p'))
|
68
|
| Ternary (x, a, b) ->
|
69
|
let a' = red a in
|
70
|
let b' = red b in
|
71
|
Ternary (x, a', b')
|
72
|
| f ->
|
73
|
f
|
74
|
|
75
|
(* smart constructors *)
|
76
|
(* let mk_condition x l =
|
77
|
* if l = tag_true then Ternary (Val x, True, False)
|
78
|
* else if l = tag_false then Ternary (Val x, False, True)
|
79
|
* else Equal (Val x, Tag l) *)
|
80
|
|
81
|
let vals vs = List.map (fun v -> Val v) vs
|
82
|
|
83
|
let mk_pred_call pred = Predicate pred
|
84
|
|
85
|
(* let mk_clocked_on id =
|
86
|
* mk_pred_call (Clocked_on id) *)
|
87
|
|
88
|
let mk_transition ?(mems = Utils.ISet.empty) ?r ?i ?inst id inputs locals
|
89
|
outputs =
|
90
|
let tr =
|
91
|
mk_pred_call
|
92
|
(Transition
|
93
|
( id,
|
94
|
inst,
|
95
|
i,
|
96
|
vals inputs,
|
97
|
vals locals,
|
98
|
vals outputs,
|
99
|
(match r with Some _ -> true | None -> false),
|
100
|
mems ))
|
101
|
in
|
102
|
match r, inst with
|
103
|
| Some r, Some inst ->
|
104
|
ExistsMem (id, mk_pred_call (Reset (id, inst, r)), tr)
|
105
|
| _ ->
|
106
|
tr
|
107
|
|
108
|
let mk_memory_pack ?i ?inst id = mk_pred_call (MemoryPack (id, inst, i))
|
109
|
|
110
|
let mk_state_variable_pack x = StateVarPack (StateVar x)
|
111
|
|
112
|
let mk_state_assign_tr x v = Equal (Memory (StateVar x), Val v)
|
113
|
|
114
|
let mk_conditional_tr v t f = Ternary (Val v, t, f)
|
115
|
|
116
|
let mk_branch_tr x hl =
|
117
|
And (List.map (fun (t, spec) -> Imply (Equal (Var x, Tag t), spec)) hl)
|
118
|
|
119
|
let mk_assign_tr x v = Equal (Var x, Val v)
|