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
|
open Ast
(* AST for logical formulas *)
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 bool_expr =
(* constants *)
| BConst of bool
(* operators from numeric values to boolean values *)
| BRel of binary_rel_op * num_expr * num_expr
| BBoolEq of id * bool
(* 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)
(* 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)
| BBoolEq(id, v) -> BBoolEq(id, not v)
| BNot e -> eliminate_not e
| BRel(r, a, b) ->
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 cons_op =
| CONS_EQ | CONS_NE
| CONS_GT | CONS_GE
type cons = num_expr * cons_op (* always imply right member = 0 *)
type conslist = 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
| BBoolEq(id, v) ->
if v then
[NBinary(AST_MINUS, NIdent id, NIntConst 1), CONS_EQ], CLTrue
else
[NIdent id, CONS_EQ], CLTrue
| BOr(a, b) ->
let ca, ra = conslist_of_f a in
let cb, rb = conslist_of_f b in
begin match ca, ra, cb, rb with
| _, CLFalse, _, _ -> cb, rb
| _, _, _, CLFalse -> ca, ra
| [], CLTrue, _, _ -> [], CLTrue
| _, _, [], CLTrue -> [], CLTrue
| _ -> [], CLOr((ca, ra), (cb, rb))
end
| BAnd(a, b) ->
let ca, ra = conslist_of_f a in
let cb, rb = conslist_of_f b in
let cons = ca @ cb in
begin match ra, rb with
| CLFalse, _ | _, CLFalse -> [], CLFalse
| CLTrue, _ -> cons, rb
| ra, CLTrue -> cons, ra
| _, _ -> cons, CLAnd(ra, rb)
end
|
