Revision dbab1fe5 src/tools/zustre/zustre_test.ml
src/tools/zustre/zustre_test.ml | ||
---|---|---|
135 | 135 |
Z3.Fixedpoint.add_rule !fp expr_forall_main1 None; |
136 | 136 |
|
137 | 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 |
|
|
138 | 167 |
|
139 | 168 |
|
140 | 169 |
(* TODO: not implemented yet since the error is visible without it *) |
Also available in: Unified diff