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