lustrec / src / tools / zustre / zustre_test.ml @ dbab1fe5
History  View  Annotate  Download (7.46 KB)
1 
(* Example of a use of Z3 Fixedpoint that doesn't work 

2 
The file is selfcontained 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 useocamlfind 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  
220  
221 
