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
|
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
(* boolean operators *)
| BAnd of bool_expr * bool_expr
| BOr of bool_expr * bool_expr
| BNot of bool_expr
(* 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)
| 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 cons = match op with
| AST_EQ -> NBinary(AST_MINUS, a, b), CONS_EQ
| AST_NE -> NBinary(AST_MINUS, a, b), CONS_NE
| AST_GT -> NBinary(AST_MINUS, a, b), CONS_GT
| AST_GE -> NBinary(AST_MINUS, a, b), CONS_GE
| AST_LT -> NBinary(AST_MINUS, b, a), CONS_GT
| AST_LE -> NBinary(AST_MINUS, b, a), CONS_GE
in [cons], CLTrue
| BConst x ->
[], if x then CLTrue else CLFalse
| 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
|
