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
|
open Ast
open Util
open Ast_util
(* AST for logical formulas *)
(* Numerical part *)
type num_expr =
(* constants *)
| NIntConst of int
| NRealConst of float
(* operators *)
| NBinary of binary_op * num_expr * num_expr
| NUnary of unary_op * num_expr
(* 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 * enum_expr * 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
(* operators on enumerated types *)
| BEnumCons of enum_cons
(* boolean operators *)
| BAnd of bool_expr * bool_expr
| BOr of bool_expr * bool_expr
| BNot of bool_expr
let f_and a b = match a, b with
| BConst false, _ | _, BConst false -> BConst false
| BConst true, b -> b
| a, BConst true -> a
| a, b -> BAnd(a, b)
let f_or a b = match a, b with
| BConst true, _ | _, BConst true -> BConst true
| BConst false, b -> b
| a, BConst false -> a
| a, b -> BOr(a, b)
let f_e_eq a b = match a, b with
| EItem u, EItem v -> BConst (u = v)
| _ -> BEnumCons(E_EQ, a, b)
(* 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)
| 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) ->
if r = AST_EQ then
BOr(BRel(AST_LT, a, b), BRel(AST_GT, a, b))
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)
| 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) ->
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
then (x, op)
else (NBinary(AST_MINUS, x, y), 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
|
