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
|
open Ast
open Formula
open Ast_printer
let string_of_binary_rel = function
| AST_EQ -> "="
| AST_NE -> "≠"
| AST_LT -> "<"
| AST_LE -> "≤"
| AST_GT -> ">"
| AST_GE -> "≥"
let ne_prec = function
| NUnary(op, _) -> unary_precedence
| NBinary(op, _, _) -> binary_op_precedence op
| _ -> 100
let be_prec = function
| BRel(op, _, _) -> binary_rel_precedence op
| BAnd _ -> binary_bool_precedence AST_AND
| BOr _ -> binary_bool_precedence AST_OR
| BNot _ -> unary_precedence
| _ -> 100
let is_or = function
| BOr _ -> true
| _ -> false
let is_and = function
| BAnd _ -> true
| _ -> false
let print_ch fmt pf fa a fe e =
if fa a < fe e
then Format.fprintf fmt "@[<hv 2>(%a)@]" pf a
else Format.fprintf fmt "@[<hv 2>%a@]" pf a
let print_ah fmt pf fa a fe e =
if fa a <= fe e
then Format.fprintf fmt "@[<hv 2>(%a)@]" pf a
else Format.fprintf fmt "@[<hv 2>%a@]" pf a
let print_id fmt id =
let re = Str.regexp "/" in
Format.fprintf fmt "%s" (Str.global_replace re "·" id)
let rec print_num_expr fmt e = match e with
| NIntConst i -> Format.fprintf fmt "%d" i
| NRealConst f -> Format.fprintf fmt "%f" f
| NIdent id ->
print_id fmt id
| NBinary(op, a, b) ->
print_ch fmt print_num_expr ne_prec a ne_prec e;
Format.fprintf fmt "@ %s " (string_of_binary_op op);
print_ah fmt print_num_expr ne_prec b ne_prec e
| NUnary(op, a) ->
Format.fprintf fmt "%s " (string_of_unary_op op);
print_ah fmt print_num_expr ne_prec a ne_prec e
(* Print boolean form of formula *)
let rec print_bool_expr fmt e = match e with
| BConst b -> Format.fprintf fmt "%s" (if b then "true" else "false")
| BRel(op, a, b) ->
print_ch fmt print_num_expr ne_prec a be_prec e;
Format.fprintf fmt "@ %s " (string_of_binary_rel op);
print_ch fmt print_num_expr ne_prec b be_prec e
| BAnd (a, b) ->
if is_and a then
Format.fprintf fmt "%a" print_bool_expr a
else
if be_prec a < be_prec e || is_or a
then Format.fprintf fmt "@[<hv 2>(%a)@]" print_bool_expr a
else Format.fprintf fmt "@[<hv 2>%a@]" print_bool_expr a;
Format.fprintf fmt "@ ∧ ";
if is_and b then
Format.fprintf fmt "%a" print_bool_expr b
else
if be_prec b < be_prec e || is_or b
then Format.fprintf fmt "@[<hv 2>(%a)@]" print_bool_expr b
else Format.fprintf fmt "@[<hv 2>%a@]" print_bool_expr b
| BOr (a, b) ->
print_ch fmt print_bool_expr be_prec a be_prec e;
Format.fprintf fmt "@ ∨ ";
print_ch fmt print_bool_expr be_prec b be_prec e
| BNot (a) ->
Format.pp_print_string fmt "¬";
print_ch fmt print_bool_expr be_prec a be_prec e
let print_expr fmt e =
Format.fprintf fmt "@[<hv 2>%a@]" print_bool_expr e
(* Print constraint list form of formula *)
let print_cons_sg fmt sg =
let sg_str = match sg with
| CONS_EQ -> "="
| CONS_NE -> "≠"
| CONS_GT -> ">"
| CONS_GE -> "≥"
in
Format.fprintf fmt "%s" sg_str
let print_cons fmt (eq, sg) =
Format.fprintf fmt "@[<hv 2>%a %a 0@]"
print_num_expr eq print_cons_sg sg
let rec print_conslist fmt (cons, e) =
let rec aux = function
| [] -> false
| [a] ->
Format.fprintf fmt "@[<hv 2>%a@]" print_cons a; true
| p::q ->
Format.fprintf fmt "@[<hv 2>%a@]" print_cons p;
Format.fprintf fmt "@ ∧ ";
aux q
in
match e with
| CLTrue ->
Format.fprintf fmt "@[<hv 2>(";
ignore (aux cons);
Format.fprintf fmt ")@]"
| CLFalse ->
Format.fprintf fmt "false"
| _ ->
Format.fprintf fmt "@[<hv 2>(";
if aux cons then Format.fprintf fmt "@ ∧ ";
print_conslist_expr fmt e;
Format.fprintf fmt ")@]"
and print_conslist_expr fmt = function
| CLTrue -> Format.fprintf fmt "true"
| CLFalse -> Format.fprintf fmt "false"
| CLOr(a, b) ->
Format.fprintf fmt "@[<hv 2>(%a@ ∨ %a)@]"
print_conslist a
print_conslist b
| CLAnd(a, b) ->
Format.fprintf fmt "%a@ ∧ %a"
print_conslist_expr a
print_conslist_expr b
|
