Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

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