Project

General

Profile

Revision dbab1fe5 src/tools/zustre/zustre_test.ml

View differences:

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