1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
|
open Ast
open Util
open Ast_util
(* AST for logical formulas *)
(* Numerical part *)
(* bool on numerical operators : is it float ? *)
type num_expr =
(* constants *)
| NIntConst of int
| NRealConst of float
(* operators *)
| NBinary of binary_op * num_expr * num_expr * bool
| NUnary of unary_op * num_expr * bool
(* identifier *)
| NIdent of id
type num_cons_op =
| CONS_EQ | CONS_NE
| CONS_GT | CONS_GE
type num_cons = num_expr * num_cons_op (* always imply right member = 0 *)
(* Logical part *)
(* Enumerated types *)
type enum_expr =
| EIdent of id
| EItem of string
type enum_op =
| E_EQ | E_NE
type enum_cons = enum_op * id * enum_expr
type bool_expr =
(* constants *)
| BConst of bool
(* operators from numeric values to boolean values *)
| BRel of binary_rel_op * num_expr * num_expr * bool
(* operators on enumerated types *)
| BEnumCons of enum_cons
(* boolean operators *)
| BAnd of bool_expr * bool_expr
| BOr of bool_expr * bool_expr
| BTernary of bool_expr * bool_expr * bool_expr
(* (A and B) or ((not A) and C) *)
| BNot of bool_expr
let is_false = function
| BConst false | BNot(BConst true) -> true
| _ -> false
let is_true = function
| BConst true | BNot(BConst false) -> true
| _ -> false
let f_and a b =
if is_false a || is_false b then BConst false
else if is_true a then b
else if is_true b then a
else BAnd(a, b)
let f_and_list = List.fold_left f_and (BConst true)
let f_or a b =
if is_true a || is_true b then BConst true
else if is_false a then b
else if is_false b then a
else BOr(a, b)
let f_ternary c a b =
if is_true c then a
else if is_false c then b
else
BTernary(c, a, b)
let f_e_op op a b = match a, b with
| EItem i, EItem j -> BConst (if op = E_EQ then i = j else i <> j)
| EIdent x, v | v, EIdent x -> BEnumCons(op, x, v)
let f_e_eq = f_e_op E_EQ
(* Write all formula without using the NOT operator *)
let rec eliminate_not = function
| BNot e -> eliminate_not_negate e
| BAnd(a, b) -> BAnd(eliminate_not a, eliminate_not b)
| BOr(a, b) -> BOr(eliminate_not a, eliminate_not b)
| BTernary(c, a, b) ->
BTernary(eliminate_not c, eliminate_not a, eliminate_not b)
| x -> x
and eliminate_not_negate = function
| BConst x -> BConst(not x)
| BEnumCons(op, a, b) -> BEnumCons((if op = E_EQ then E_NE else E_EQ), a, b)
| BNot e -> eliminate_not e
| BRel(r, a, b, is_real) ->
if r = AST_EQ then
BOr(BRel(AST_LT, a, b, is_real), BRel(AST_GT, a, b, is_real))
else
let r' = match r with
| AST_EQ -> AST_NE
| AST_NE -> AST_EQ
| AST_LT -> AST_GE
| AST_LE -> AST_GT
| AST_GT -> AST_LE
| AST_GE -> AST_LT
in
BRel(r', a, b, is_real)
| BTernary (c, a, b) ->
eliminate_not_negate(BOr(BAnd(c, a), BAnd(BNot c, b)))
| BAnd(a, b) ->
BOr(eliminate_not_negate a, eliminate_not_negate b)
| BOr(a, b) ->
BAnd(eliminate_not_negate a, eliminate_not_negate b)
(*
In big ANDs, try to separate levels of /\ and levels of \/
We also use this step to simplify trues and falses that may be present.
*)
type conslist = enum_cons list * num_cons list * conslist_bool_expr
and conslist_bool_expr =
| CLTrue
| CLFalse
| CLAnd of conslist_bool_expr * conslist_bool_expr
| CLOr of conslist * conslist
let rec conslist_of_f = function
| BNot e -> conslist_of_f (eliminate_not_negate e)
| BRel (op, a, b, is_real) ->
let x, y, op = match op with
| AST_EQ -> a, b, CONS_EQ
| AST_NE -> a, b, CONS_NE
| AST_GT -> a, b, CONS_GT
| AST_GE -> a, b, CONS_GE
| AST_LT -> b, a, CONS_GT
| AST_LE -> b, a, CONS_GE
in
let cons = if y = NIntConst 0 || y = NRealConst 0.
then (x, op)
else (NBinary(AST_MINUS, x, y, is_real), op)
in [], [cons], CLTrue
| BConst x ->
[], [], if x then CLTrue else CLFalse
| BEnumCons e ->
[e], [], CLTrue
| BOr(a, b) ->
let eca, ca, ra = conslist_of_f a in
let ecb, cb, rb = conslist_of_f b in
begin match eca, ca, ra, ecb, cb, rb with
| _, _, CLFalse, _, _, _ -> ecb, cb, rb
| _, _, _, _, _, CLFalse -> eca, ca, ra
| [], [], CLTrue, _, _, _ -> [], [], CLTrue
| _, _, _, [], [], CLTrue -> [], [], CLTrue
| _ -> [], [], CLOr((eca, ca, ra), (ecb, cb, rb))
end
| BAnd(a, b) ->
let eca, ca, ra = conslist_of_f a in
let ecb, cb, rb = conslist_of_f b in
let cons = ca @ cb in
let econs = eca @ ecb in
begin match ra, rb with
| CLFalse, _ | _, CLFalse -> [], [], CLFalse
| CLTrue, _ -> econs, cons, rb
| _, CLTrue -> econs, cons, ra
| _, _ -> econs, cons, CLAnd(ra, rb)
end
| BTernary(c, a, b) ->
conslist_of_f (BOr (BAnd(c, a), BAnd(BNot(c), b)))
(*
Simplify formula considering something is true
*)
let rec get_root_true = function
| BAnd(a, b) ->
get_root_true a @ get_root_true b
| BEnumCons e -> [BEnumCons e]
| BRel (a, b, c, d) -> [BRel (a, b, c, d)]
| _ -> []
let rec simplify true_eqs e =
if List.exists
(fun f ->
try eliminate_not e = eliminate_not f with _ -> false)
true_eqs
then BConst true
else if List.exists
(fun f ->
match e, f with
| BEnumCons(E_EQ, a, EItem v), BEnumCons(E_EQ, b, EItem w)
when a = b && v <> w -> true
| _ -> try eliminate_not e = eliminate_not_negate f with _ -> false)
true_eqs
then BConst false
else
match e with
| BAnd(a, b) ->
f_and
(simplify true_eqs a)
(simplify true_eqs b)
| BOr(a, b) ->
f_or
(simplify true_eqs a)
(simplify true_eqs b)
| BTernary(c, a, b) ->
let c, a, b =
simplify true_eqs c,
simplify true_eqs a,
simplify true_eqs b in
begin match c with
| BConst true -> a
| BConst false -> b
| _ -> BTernary(c, a, b)
end
| BNot(n) ->
begin match simplify true_eqs n with
| BConst e -> BConst (not e)
| x -> BNot x
end
| v -> v
let rec simplify_k true_eqs e =
List.fold_left f_and (simplify true_eqs e) true_eqs
|
