Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/tools/zustre/zustre_test.ml | ||
---|---|---|
1 |
(* Example of a use of Z3 Fixedpoint that doesn't work |
|
2 |
The file is self-contained and shall be compiled as follow:
|
|
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 | 3 |
|
4 |
in File _tags, add the simple line |
|
5 |
<**/*>: package(z3) |
|
4 |
in File _tags, add the simple line <**/*>: package(z3) |
|
6 | 5 |
|
7 |
Then compile as |
|
8 |
ocamlbuild -use-ocamlfind zustre_test.native |
|
6 |
Then compile as ocamlbuild -use-ocamlfind zustre_test.native |
|
9 | 7 |
|
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 |
") |
|
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)) |
|
24 | 12 |
|
25 |
*) |
|
13 |
Fatal error: exception Z3.Error("Uninterpreted 'y' in <null>: f(#0,#1) :- (= |
|
14 |
(:var 1) y), (= (:var 0) x), (= x y). ") *) |
|
26 | 15 |
|
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 |
|
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 |
|
33 | 23 |
|
34 | 24 |
(* Global references to declare Z3 context and Fixedpoint engine *) |
35 |
|
|
25 |
|
|
36 | 26 |
let ctx = ref (Z3.mk_context []) |
27 |
|
|
37 | 28 |
let fp = ref (Z3.Fixedpoint.mk_fixedpoint !ctx) |
38 | 29 |
|
39 | 30 |
(* Shortcuts to basic sorts *) |
40 | 31 |
|
41 | 32 |
let bool_sort = Z3.Boolean.mk_sort !ctx |
33 |
|
|
42 | 34 |
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx |
35 |
|
|
43 | 36 |
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx |
44 | 37 |
|
45 |
|
|
46 | 38 |
let _ = |
47 |
|
|
48 |
|
|
49 | 39 |
(* Setting up the fixed point engine *) |
50 | 40 |
fp := Z3.Fixedpoint.mk_fixedpoint !ctx; |
51 | 41 |
let module P = Z3.Params in |
... | ... | |
55 | 45 |
P.add_symbol params (mks "engine") (mks "spacer"); |
56 | 46 |
Z3.Fixedpoint.set_parameters !fp params; |
57 | 47 |
|
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 |
|
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 |
|
63 | 50 |
|
64 | 51 |
Querying ERR shall be unsat since the only valid MAIN(x,y) are x=y and |
65 |
therefore ERR is unsat. |
|
66 |
*) |
|
67 |
|
|
52 |
therefore ERR is unsat. *) |
|
53 |
|
|
68 | 54 |
(* Simple rule : forall x, y, (x=y => f(x,y)) *) |
69 | 55 |
let x = Z3.FuncDecl.mk_func_decl_s !ctx "x" [] int_sort in |
70 | 56 |
let y = Z3.FuncDecl.mk_func_decl_s !ctx "y" [] int_sort in |
71 | 57 |
let x_expr = Z3.Expr.mk_const_f !ctx x in |
72 | 58 |
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 |
|
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 |
|
77 | 66 |
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 |
|
67 |
|
|
68 |
let expr_f_lhs = |
|
69 |
(* x = y *) |
|
70 |
x_eq_y_expr |
|
81 | 71 |
in |
82 | 72 |
let expr_f_rhs = f_x_y_expr in |
83 | 73 |
let expr_f = Z3.Boolean.mk_implies !ctx expr_f_lhs expr_f_rhs in |
84 | 74 |
(* 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 (* ? *) |
|
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 |
(* ? *) |
|
97 | 85 |
in |
98 | 86 |
let expr_forall_f = Z3.Quantifier.expr_of_quantifier expr_forall_f in |
99 | 87 |
Z3.Fixedpoint.add_rule !fp expr_forall_f None; |
100 |
|
|
101 |
|
|
88 |
|
|
102 | 89 |
(* INIT RULE *) |
103 | 90 |
let decl_init = Z3.FuncDecl.mk_func_decl_s !ctx "INIT_STATE" [] bool_sort in |
104 |
Z3.Fixedpoint.register_relation !fp decl_init;
|
|
91 |
Z3.Fixedpoint.register_relation !fp decl_init; |
|
105 | 92 |
let init_expr = Z3.Expr.mk_app !ctx decl_init [] in |
106 | 93 |
Z3.Fixedpoint.add_rule !fp init_expr None; |
107 | 94 |
|
108 | 95 |
(* 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 |
|
96 |
let decl_main = |
|
97 |
Z3.FuncDecl.mk_func_decl_s !ctx "MAIN" [ int_sort; int_sort ] bool_sort |
|
98 |
in |
|
110 | 99 |
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 |
|
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 |
|
116 | 108 |
let expr_main1_rhs = main_x_y_expr in |
117 | 109 |
let expr_main1 = Z3.Boolean.mk_implies !ctx expr_main1_lhs expr_main1_rhs in |
118 | 110 |
(* 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 (* ? *) |
|
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 |
(* ? *) |
|
133 | 121 |
in |
134 | 122 |
let expr_forall_main1 = Z3.Quantifier.expr_of_quantifier expr_forall_main1 in |
135 | 123 |
Z3.Fixedpoint.add_rule !fp expr_forall_main1 None; |
136 | 124 |
|
137 | 125 |
(* Rule 2: forall x,y, MAIN(x,y) => MAIN(x+1, y+1) *) |
138 | 126 |
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 |
|
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 |
|
146 | 138 |
let expr_main2_rhs = main_x_y_plus_one_expr in |
147 | 139 |
let expr_main2 = Z3.Boolean.mk_implies !ctx expr_main2_lhs expr_main2_rhs in |
148 | 140 |
(* 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 (* ? *) |
|
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 |
(* ? *) |
|
163 | 151 |
in |
164 | 152 |
let expr_forall_main2 = Z3.Quantifier.expr_of_quantifier expr_forall_main2 in |
165 | 153 |
Z3.Fixedpoint.add_rule !fp expr_forall_main2 None; |
166 |
|
|
167 |
|
|
168 |
|
|
154 |
|
|
169 | 155 |
(* TODO: not implemented yet since the error is visible without it *) |
170 |
|
|
156 |
|
|
171 | 157 |
(* 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 |
*) |
|
158 |
(* This is performed as follow: rule (forall x, y, MAIN(x,y) and x!=y => ERR) *) |
|
175 | 159 |
let decl_err = Z3.FuncDecl.mk_func_decl_s !ctx "ERR" [] bool_sort in |
176 |
Z3.Fixedpoint.register_relation !fp decl_err;
|
|
160 |
Z3.Fixedpoint.register_relation !fp decl_err; |
|
177 | 161 |
let err_expr = Z3.Expr.mk_app !ctx decl_err [] in |
178 | 162 |
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 |
|
163 |
let expr_err_lhs = Z3.Boolean.mk_and !ctx [ x_diff_y_expr; main_x_y_expr ] in |
|
181 | 164 |
let expr_err_rhs = err_expr in |
182 | 165 |
let expr_err = Z3.Boolean.mk_implies !ctx expr_err_lhs expr_err_rhs in |
183 | 166 |
(* 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 (* ? *) |
|
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 |
(* ? *) |
|
197 | 177 |
in |
198 | 178 |
let expr_forall_err = Z3.Quantifier.expr_of_quantifier expr_forall_err in |
199 | 179 |
Z3.Fixedpoint.add_rule !fp expr_forall_err None; |
200 | 180 |
|
201 | 181 |
(* Printing the rules for sanity check *) |
202 |
|
|
203 | 182 |
let rules_expr = Z3.Fixedpoint.get_rules !fp in |
204 | 183 |
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 |
|
|
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; |
|
213 | 189 |
|
214 |
let res_status = Z3.Fixedpoint.query_r !fp [decl_err] in
|
|
190 |
let res_status = Z3.Fixedpoint.query_r !fp [ decl_err ] in
|
|
215 | 191 |
|
216 | 192 |
Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status); |
217 | 193 |
|
218 |
|
|
219 | 194 |
let ts = Z3.Tactic.get_tactic_names !ctx in |
220 | 195 |
List.iter (fun s -> Format.printf "%s@." s) ts; |
221 | 196 |
() |
222 |
|
|
223 |
|
|
224 |
|
|
225 |
|
|
226 |
|
Also available in: Unified diff
reformatting