Revision ca7ff3f7
Added by Lélio Brun 7 months 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