1
|
(* Example of a use of Z3 Fixedpoint that doesn't work
|
2
|
The file is self-contained and shall be compiled as follow:
|
3
|
|
4
|
in File _tags, add the simple line
|
5
|
<**/*>: package(z3)
|
6
|
|
7
|
Then compile as
|
8
|
ocamlbuild -use-ocamlfind zustre_test.native
|
9
|
|
10
|
We obtain the following output:
|
11
|
$ ./zustre_test.native
|
12
|
Registered rules:
|
13
|
Rule: (forall ((x Int) (y Int)) (=> (= x y) (f x y)))
|
14
|
Rule: INIT_STATE
|
15
|
Rule: (forall ((x Int) (y Int)) (=> (and (f x y) INIT_STATE) (MAIN x y)))
|
16
|
Rule: (forall ((x Int) (y Int)) (=> (and (not (= x y)) (MAIN x y)) ERR))
|
17
|
|
18
|
Fatal error: exception Z3.Error("Uninterpreted 'y' in <null>:
|
19
|
f(#0,#1) :-
|
20
|
(= (:var 1) y),
|
21
|
(= (:var 0) x),
|
22
|
(= x y).
|
23
|
")
|
24
|
|
25
|
*)
|
26
|
|
27
|
|
28
|
|
29
|
let rec fprintf_list ~sep:sep f fmt = function
|
30
|
| [] -> ()
|
31
|
| [e] -> f fmt e
|
32
|
| x::r -> Format.fprintf fmt "%a%(%)%a" f x sep (fprintf_list ~sep f) r
|
33
|
|
34
|
(* Global references to declare Z3 context and Fixedpoint engine *)
|
35
|
|
36
|
let ctx = ref (Z3.mk_context [])
|
37
|
let fp = ref (Z3.Fixedpoint.mk_fixedpoint !ctx)
|
38
|
|
39
|
(* Shortcuts to basic sorts *)
|
40
|
|
41
|
let bool_sort = Z3.Boolean.mk_sort !ctx
|
42
|
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx
|
43
|
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx
|
44
|
|
45
|
|
46
|
let _ =
|
47
|
|
48
|
|
49
|
(* Setting up the fixed point engine *)
|
50
|
fp := Z3.Fixedpoint.mk_fixedpoint !ctx;
|
51
|
let module P = Z3.Params in
|
52
|
let module S = Z3.Symbol in
|
53
|
let mks = S.mk_string !ctx in
|
54
|
let params = P.mk_params !ctx in
|
55
|
P.add_symbol params (mks "engine") (mks "spacer");
|
56
|
Z3.Fixedpoint.set_parameters !fp params;
|
57
|
|
58
|
(* Three rules
|
59
|
R1: (x = y) => f(x,y)
|
60
|
R2: INIT and f(x,y) => MAIN(x,y)
|
61
|
R3: x!=y and MAIN(x,y) => ERR(x,y)
|
62
|
INIT is assumed as the beginning
|
63
|
|
64
|
Querying ERR shall be unsat since the only valid MAIN(x,y) are x=y and
|
65
|
therefore ERR is unsat.
|
66
|
*)
|
67
|
|
68
|
(* Simple rule : forall x, y, (x=y => f(x,y)) *)
|
69
|
let x = Z3.FuncDecl.mk_func_decl_s !ctx "x" [] int_sort in
|
70
|
let y = Z3.FuncDecl.mk_func_decl_s !ctx "y" [] int_sort in
|
71
|
let x_expr = Z3.Expr.mk_const_f !ctx x in
|
72
|
let y_expr = Z3.Expr.mk_const_f !ctx y in
|
73
|
|
74
|
let decl_f = Z3.FuncDecl.mk_func_decl_s !ctx "f" [int_sort; int_sort] bool_sort in
|
75
|
Z3.Fixedpoint.register_relation !fp decl_f; (* since f appears in the rhs of a rule *)
|
76
|
let f_x_y_expr = Z3.Expr.mk_app !ctx decl_f [x_expr; y_expr] in
|
77
|
let x_eq_y_expr = Z3.Boolean.mk_eq !ctx x_expr y_expr in
|
78
|
|
79
|
let expr_f_lhs = (* x = y *)
|
80
|
x_eq_y_expr
|
81
|
in
|
82
|
let expr_f_rhs = f_x_y_expr in
|
83
|
let expr_f = Z3.Boolean.mk_implies !ctx expr_f_lhs expr_f_rhs in
|
84
|
(* Adding forall as prefix *)
|
85
|
let expr_forall_f = Z3.Quantifier.mk_forall_const
|
86
|
!ctx (* context *)
|
87
|
(* [int_sort; int_sort] (\* sort list*\) *)
|
88
|
(* [Z3.FuncDecl.get_name x; Z3.FuncDecl.get_name y] (\* symbol list *\) *)
|
89
|
(* [x_expr; y_expr] Second try with expr list "const" *)
|
90
|
[Z3.Expr.mk_const_f !ctx x; Z3.Expr.mk_const_f !ctx y]
|
91
|
expr_f (* expression *)
|
92
|
None (* quantifier weight, None means 1 *)
|
93
|
[] (* pattern list ? *)
|
94
|
[] (* ? *)
|
95
|
None (* ? *)
|
96
|
None (* ? *)
|
97
|
in
|
98
|
let expr_forall_f = Z3.Quantifier.expr_of_quantifier expr_forall_f in
|
99
|
Z3.Fixedpoint.add_rule !fp expr_forall_f None;
|
100
|
|
101
|
|
102
|
(* INIT RULE *)
|
103
|
let decl_init = Z3.FuncDecl.mk_func_decl_s !ctx "INIT_STATE" [] bool_sort in
|
104
|
Z3.Fixedpoint.register_relation !fp decl_init;
|
105
|
let init_expr = Z3.Expr.mk_app !ctx decl_init [] in
|
106
|
Z3.Fixedpoint.add_rule !fp init_expr None;
|
107
|
|
108
|
(* MAIN is defined by two rules : INIT and induction *)
|
109
|
let decl_main = Z3.FuncDecl.mk_func_decl_s !ctx "MAIN" [int_sort; int_sort] bool_sort in
|
110
|
Z3.Fixedpoint.register_relation !fp decl_main;
|
111
|
let main_x_y_expr = Z3.Expr.mk_app !ctx decl_main [x_expr; y_expr] in
|
112
|
|
113
|
(* Rule 1: forall x, y, INIT_STATE and f(x,y) => MAIN(x,y) : at the beginning x=y *)
|
114
|
let expr_main1_lhs = (* INIT_STATE and f(x, y) *)
|
115
|
Z3.Boolean.mk_and !ctx [f_x_y_expr; init_expr] in
|
116
|
let expr_main1_rhs = main_x_y_expr in
|
117
|
let expr_main1 = Z3.Boolean.mk_implies !ctx expr_main1_lhs expr_main1_rhs in
|
118
|
(* Adding forall as prefix *)
|
119
|
let expr_forall_main1 = Z3.Quantifier.mk_forall_const
|
120
|
!ctx (* context *)
|
121
|
(*
|
122
|
[int_sort; int_sort] (* sort list*)
|
123
|
[Z3.FuncDecl.get_name x; Z3.FuncDecl.get_name y] (* symbol list *)
|
124
|
*)
|
125
|
(* [x_expr; y_expr] Second try with expr list "const" *)
|
126
|
[Z3.Expr.mk_const_f !ctx x; Z3.Expr.mk_const_f !ctx y]
|
127
|
expr_main1 (* expression *)
|
128
|
None (* quantifier weight, None means 1 *)
|
129
|
[] (* pattern list ? *)
|
130
|
[] (* ? *)
|
131
|
None (* ? *)
|
132
|
None (* ? *)
|
133
|
in
|
134
|
let expr_forall_main1 = Z3.Quantifier.expr_of_quantifier expr_forall_main1 in
|
135
|
Z3.Fixedpoint.add_rule !fp expr_forall_main1 None;
|
136
|
|
137
|
(* Rule 2: forall x,y, MAIN(x,y) => MAIN(x+1, y+1) *)
|
138
|
let expr_main2_lhs = main_x_y_expr in
|
139
|
let plus_one x = Z3.Arithmetic.mk_add !ctx
|
140
|
[
|
141
|
x;
|
142
|
(* Z3.Arithmetic.Integer.mk_const_s !ctx "1" *)
|
143
|
Z3.Expr.mk_numeral_int !ctx 1 int_sort
|
144
|
] in
|
145
|
let main_x_y_plus_one_expr = Z3.Expr.mk_app !ctx decl_main [plus_one x_expr; plus_one y_expr] in
|
146
|
let expr_main2_rhs = main_x_y_plus_one_expr in
|
147
|
let expr_main2 = Z3.Boolean.mk_implies !ctx expr_main2_lhs expr_main2_rhs in
|
148
|
(* Adding forall as prefix *)
|
149
|
let expr_forall_main2 = Z3.Quantifier.mk_forall_const
|
150
|
!ctx (* context *)
|
151
|
(*
|
152
|
[int_sort; int_sort] (* sort list*)
|
153
|
[Z3.FuncDecl.get_name x; Z3.FuncDecl.get_name y] (* symbol list *)
|
154
|
*)
|
155
|
(* [x_expr; y_expr] Second try with expr list "const" *)
|
156
|
[Z3.Expr.mk_const_f !ctx x; Z3.Expr.mk_const_f !ctx y]
|
157
|
expr_main2 (* expression *)
|
158
|
None (* quantifier weight, None means 1 *)
|
159
|
[] (* pattern list ? *)
|
160
|
[] (* ? *)
|
161
|
None (* ? *)
|
162
|
None (* ? *)
|
163
|
in
|
164
|
let expr_forall_main2 = Z3.Quantifier.expr_of_quantifier expr_forall_main2 in
|
165
|
Z3.Fixedpoint.add_rule !fp expr_forall_main2 None;
|
166
|
|
167
|
|
168
|
|
169
|
(* TODO: not implemented yet since the error is visible without it *)
|
170
|
|
171
|
(* Query: is it possible to have MAIN(x,y) and x!=y ? *)
|
172
|
(* This is performed as follow:
|
173
|
rule (forall x, y, MAIN(x,y) and x!=y => ERR)
|
174
|
*)
|
175
|
let decl_err = Z3.FuncDecl.mk_func_decl_s !ctx "ERR" [] bool_sort in
|
176
|
Z3.Fixedpoint.register_relation !fp decl_err;
|
177
|
let err_expr = Z3.Expr.mk_app !ctx decl_err [] in
|
178
|
let x_diff_y_expr = Z3.Boolean.mk_not !ctx x_eq_y_expr in
|
179
|
let expr_err_lhs =
|
180
|
Z3.Boolean.mk_and !ctx [x_diff_y_expr; main_x_y_expr] in
|
181
|
let expr_err_rhs = err_expr in
|
182
|
let expr_err = Z3.Boolean.mk_implies !ctx expr_err_lhs expr_err_rhs in
|
183
|
(* Adding forall as prefix *)
|
184
|
let expr_forall_err = Z3.Quantifier.mk_forall_const
|
185
|
!ctx (* context *)
|
186
|
(* [int_sort; int_sort] (* sort list*)
|
187
|
[Z3.FuncDecl.get_name x; Z3.FuncDecl.get_name y] (* symbol list *)
|
188
|
*)
|
189
|
(* [x_expr; y_expr] Second try with expr list "const" *)
|
190
|
[Z3.Expr.mk_const_f !ctx x; Z3.Expr.mk_const_f !ctx y]
|
191
|
expr_err (* expression *)
|
192
|
None (* quantifier weight, None means 1 *)
|
193
|
[] (* pattern list ? *)
|
194
|
[] (* ? *)
|
195
|
None (* ? *)
|
196
|
None (* ? *)
|
197
|
in
|
198
|
let expr_forall_err = Z3.Quantifier.expr_of_quantifier expr_forall_err in
|
199
|
Z3.Fixedpoint.add_rule !fp expr_forall_err None;
|
200
|
|
201
|
(* Printing the rules for sanity check *)
|
202
|
|
203
|
let rules_expr = Z3.Fixedpoint.get_rules !fp in
|
204
|
Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
|
205
|
(fprintf_list ~sep:"@ "
|
206
|
(fun fmt e ->
|
207
|
(* let e2 = Z3.Quantifier.get_body eq in *)
|
208
|
(* let fd = Z3.Expr.get_func_decl e in *)
|
209
|
Format.fprintf fmt "Rule: %s@ "
|
210
|
(Z3.Expr.to_string e);
|
211
|
)) rules_expr;
|
212
|
|
213
|
|
214
|
let res_status = Z3.Fixedpoint.query_r !fp [decl_err] in
|
215
|
|
216
|
Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);
|
217
|
|
218
|
|
219
|
let ts = Z3.Tactic.get_tactic_names !ctx in
|
220
|
List.iter (fun s -> Format.printf "%s@." s) ts;
|
221
|
()
|
222
|
|
223
|
|
224
|
|
225
|
|
226
|
|