## lustrec / src / tools / zustre / zustre_common.ml @ 51106b7e

History | View | Annotate | Download (29 KB)

1 | e4edf171 | ploc | open Lustre_types |
---|---|---|---|

2 | open Machine_code_types |
||

3 | open Machine_code_common |
||

4 | ad4774b0 | ploc | open Format |

5 | c1785a55 | ploc | (* open Horn_backend_common |

6 | * open Horn_backend *) |
||

7 | 5778dd5e | ploc | open Zustre_data |

8 | c1785a55 | ploc | |

9 | module HBC = Horn_backend_common |
||

10 | let node_name = HBC.node_name |
||

11 | 5778dd5e | ploc | |

12 | c1785a55 | ploc | let concat = HBC.concat |

13 | 5778dd5e | ploc | |

14 | c1785a55 | ploc | let rename_machine = HBC.rename_machine |

15 | let rename_machine_list = HBC.rename_machine_list |
||

16 | 5778dd5e | ploc | |

17 | c1785a55 | ploc | let rename_next = HBC.rename_next |

18 | 5778dd5e | ploc | let rename_mid = HBC.rename_mid |

19 | c1785a55 | ploc | let rename_current = HBC.rename_current |

20 | 5778dd5e | ploc | |

21 | c1785a55 | ploc | let rename_current_list = HBC.rename_current_list |

22 | let rename_mid_list = HBC.rename_mid_list |
||

23 | let rename_next_list = HBC.rename_next_list |
||

24 | 5778dd5e | ploc | |

25 | c1785a55 | ploc | let full_memory_vars = HBC.full_memory_vars |

26 | e4edf171 | ploc | let inout_vars = HBC.inout_vars |

27 | let reset_vars = HBC.reset_vars |
||

28 | let step_vars = HBC.step_vars |
||

29 | let local_memory_vars = HBC.local_memory_vars |
||

30 | 5778dd5e | ploc | let step_vars_m_x = HBC.step_vars_m_x |

31 | let step_vars_c_m_x = HBC.step_vars_c_m_x |
||

32 | e4edf171 | ploc | |

33 | c1785a55 | ploc | let machine_reset_name = HBC.machine_reset_name |

34 | 5778dd5e | ploc | let machine_step_name = HBC.machine_step_name |

35 | ff2d7a82 | ploc | let machine_stateless_name = HBC.machine_stateless_name |

36 | c1785a55 | ploc | |

37 | e4edf171 | ploc | let preprocess = Horn_backend.preprocess |

38 | |||

39 | 5778dd5e | ploc | |

40 | c1785a55 | ploc | (** Sorts |

41 | |||

42 | A sort is introduced for each basic type and each enumerated type. |
||

43 | ad4774b0 | ploc | |

44 | c1785a55 | ploc | A hashtbl records these and allow easy access to sort values, when |

45 | provided with a enumerated type name. |
||

46 | |||

47 | *) |
||

48 | |||

49 | ad4774b0 | ploc | let bool_sort = Z3.Boolean.mk_sort !ctx |

50 | let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx |
||

51 | let real_sort = Z3.Arithmetic.Real.mk_sort !ctx |
||

52 | |||

53 | c1785a55 | ploc | |

54 | let get_const_sort = Hashtbl.find const_sorts |
||

55 | let get_sort_elems = Hashtbl.find sort_elems |
||

56 | let get_tag_sort = Hashtbl.find const_tags |
||

57 | |||

58 | ad4774b0 | ploc | |

59 | c1785a55 | ploc | |

60 | ad4774b0 | ploc | let decl_sorts () = |

61 | Hashtbl.iter (fun typ decl -> |
||

62 | match typ with |
||

63 | | Tydec_const var -> |
||

64 | (match decl.top_decl_desc with |
||

65 | | TypeDef tdef -> ( |
||

66 | match tdef.tydef_desc with |
||

67 | | Tydec_enum tl -> |
||

68 | let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in |
||

69 | c1785a55 | ploc | Hashtbl.add const_sorts var new_sort; |

70 | Hashtbl.add sort_elems new_sort tl; |
||

71 | List.iter (fun t -> Hashtbl.add const_tags t new_sort) tl |
||

72 | |||

73 | 46cb4020 | ploc | | _ -> Format.eprintf "Unknown type : %a@.@?" Printers.pp_var_type_dec_desc typ; assert false |

74 | ad4774b0 | ploc | ) |

75 | | _ -> assert false |
||

76 | ) |
||

77 | | _ -> ()) Corelang.type_table |
||

78 | |||

79 | c1785a55 | ploc | |

80 | ad4774b0 | ploc | let rec type_to_sort t = |

81 | if Types.is_bool_type t then bool_sort else |
||

82 | if Types.is_int_type t then int_sort else |
||

83 | if Types.is_real_type t then real_sort else |
||

84 | match (Types.repr t).Types.tdesc with |
||

85 | | Types.Tconst ty -> get_const_sort ty |
||

86 | | Types.Tclock t -> type_to_sort t |
||

87 | | Types.Tarray(dim,ty) -> Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty) |
||

88 | | Types.Tstatic(d, ty)-> type_to_sort ty |
||

89 | | Types.Tarrow _ |
||

90 | | _ -> Format.eprintf "internal error: pp_type %a@." |
||

91 | Types.print_ty t; assert false |
||

92 | |||

93 | 7d77632f | ploc | |

94 | (* let idx_var = *) |
||

95 | (* Z3.FuncDecl.mk_func_decl_s !ctx "__idx__" [] idx_sort *) |
||

96 | |||

97 | (* let uid_var = *) |
||

98 | (* Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort *) |
||

99 | |||

100 | c1785a55 | ploc | (** Func decls |

101 | |||

102 | 9f3de818 | ploc | Similarly fun_decls are registerd, by their name, into a hashtbl. The |

103 | proposed encoding introduces a 0-ary fun_decl to model variables and |
||

104 | fun_decl with arguments to declare reset and step predicates. |
||

105 | c1785a55 | ploc | |

106 | |||

107 | |||

108 | 9f3de818 | ploc | *) |

109 | c1785a55 | ploc | let register_fdecl id fd = Hashtbl.add decls id fd |

110 | 5778dd5e | ploc | let get_fdecl id = |

111 | try |
||

112 | Hashtbl.find decls id |
||

113 | with Not_found -> (Format.eprintf "Unable to find func_decl %s@.@?" id; raise Not_found) |
||

114 | 51ec4e8c | ploc | |

115 | let pp_fdecls fmt = |
||

116 | Format.fprintf fmt "Registered fdecls: @[%a@]@ " |
||

117 | (Utils.fprintf_list ~sep:"@ " Format.pp_print_string) (Hashtbl.fold (fun id _ accu -> id::accu) decls []) |
||

118 | |||

119 | 5778dd5e | ploc | |

120 | ad4774b0 | ploc | let decl_var id = |

121 | dbab1fe5 | ploc | (* Format.eprintf "Declaring var %s@." id.var_id; *) |

122 | c1785a55 | ploc | let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in |

123 | register_fdecl id.var_id fdecl; |
||

124 | fdecl |
||

125 | |||

126 | 7d77632f | ploc | let idx_sort = int_sort |

127 | let uid_sort = Z3.Z3List.mk_sort !ctx (Z3.Symbol.mk_string !ctx "uid_list") int_sort |
||

128 | let uid_conc = |
||

129 | let fd = Z3.Z3List.get_cons_decl uid_sort in |
||

130 | fun head tail -> Z3.FuncDecl.apply fd [head;tail] |
||

131 | |||

132 | let get_instance_uid = |
||

133 | let hash : (string, int) Hashtbl.t = Hashtbl.create 13 in |
||

134 | let cpt = ref 0 in |
||

135 | fun i -> |
||

136 | let id = |
||

137 | if Hashtbl.mem hash i then |
||

138 | Hashtbl.find hash i |
||

139 | else ( |
||

140 | incr cpt; |
||

141 | Hashtbl.add hash i !cpt; |
||

142 | !cpt |
||

143 | ) |
||

144 | in |
||

145 | Z3.Arithmetic.Integer.mk_numeral_i !ctx id |
||

146 | |||

147 | |||

148 | |||

149 | let decl_rel ?(no_additional_vars=false) name args_sorts = |
||

150 | (* Enriching arg_sorts with two new variables: a counting index and an |
||

151 | uid *) |
||

152 | let args_sorts = |
||

153 | if no_additional_vars then args_sorts else idx_sort::uid_sort::args_sorts in |
||

154 | 2f7c9195 | ploc | |

155 | (* let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in *) |
||

156 | 4300981b | ploc | if !debug then |

157 | Format.eprintf "Registering fdecl %s (%a)@." |
||

158 | name |
||

159 | (Utils.fprintf_list ~sep:"@ " |
||

160 | (fun fmt sort -> Format.fprintf fmt "%s" (Z3.Sort.to_string sort))) |
||

161 | args_sorts |
||

162 | ; |
||

163 | c1785a55 | ploc | let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in |

164 | 5778dd5e | ploc | Z3.Fixedpoint.register_relation !fp fdecl; |

165 | c1785a55 | ploc | register_fdecl name fdecl; |

166 | fdecl |
||

167 | |||

168 | |||

169 | 7d77632f | ploc | |

170 | (* Shared variables to describe counter and uid *) |
||

171 | |||

172 | let idx = Corelang.dummy_var_decl "__idx__" Type_predef.type_int |
||

173 | let idx_var = Z3.Expr.mk_const_f !ctx (decl_var idx) |
||

174 | let uid = Corelang.dummy_var_decl "__uid__" Type_predef.type_int |
||

175 | let uid_fd = Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort |
||

176 | let _ = register_fdecl "__uid__" uid_fd |
||

177 | let uid_var = Z3.Expr.mk_const_f !ctx uid_fd |
||

178 | |||

179 | e4edf171 | ploc | (** Conversion functions |

180 | c1785a55 | ploc | |

181 | 9f3de818 | ploc | The following is similar to the Horn backend. Each printing function is |

182 | rephrased from pp_xx to xx_to_expr and produces a Z3 value. |
||

183 | c1785a55 | ploc | |

184 | 9f3de818 | ploc | *) |

185 | c1785a55 | ploc | |

186 | |||

187 | (* Returns the f_decl associated to the variable v *) |
||

188 | let horn_var_to_expr v = |
||

189 | Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id) |
||

190 | |||

191 | |||

192 | |||

193 | |||

194 | (* Used to print boolean constants *) |
||

195 | let horn_tag_to_expr t = |
||

196 | if t = Corelang.tag_true then |
||

197 | Z3.Boolean.mk_true !ctx |
||

198 | else if t = Corelang.tag_false then |
||

199 | Z3.Boolean.mk_false !ctx |
||

200 | else |
||

201 | (* Finding the associated sort *) |
||

202 | let sort = get_tag_sort t in |
||

203 | let elems = get_sort_elems sort in |
||

204 | let res : Z3.Expr.expr option = |
||

205 | List.fold_left2 (fun res cst expr -> |
||

206 | match res with |
||

207 | | Some _ -> res |
||

208 | | None -> if t = cst then Some (expr:Z3.Expr.expr) else None |
||

209 | ) None elems (Z3.Enumeration.get_consts sort) |
||

210 | in |
||

211 | match res with None -> assert false | Some s -> s |
||

212 | |||

213 | (* Prints a constant value *) |
||

214 | let rec horn_const_to_expr c = |
||

215 | match c with |
||

216 | | Const_int i -> Z3.Arithmetic.Integer.mk_numeral_i !ctx i |
||

217 | | Const_real (_,_,s) -> Z3.Arithmetic.Real.mk_numeral_i !ctx 0 |
||

218 | | Const_tag t -> horn_tag_to_expr t |
||

219 | | _ -> assert false |
||

220 | |||

221 | |||

222 | |||

223 | (* Default value for each type, used when building arrays. Eg integer array |
||

224 | [2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value |
||

225 | for the type integer (arrays). |
||

226 | *) |
||

227 | let rec horn_default_val t = |
||

228 | let t = Types.dynamic_type t in |
||

229 | if Types.is_bool_type t then Z3.Boolean.mk_true !ctx else |
||

230 | if Types.is_int_type t then Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 else |
||

231 | if Types.is_real_type t then Z3.Arithmetic.Real.mk_numeral_i !ctx 0 else |
||

232 | (* match (Types.dynamic_type t).Types.tdesc with |
||

233 | * | Types.Tarray(dim, l) -> (\* TODO PL: this strange code has to be (heavily) checked *\) |
||

234 | * let valt = Types.array_element_type t in |
||

235 | * fprintf fmt "((as const (Array Int %a)) %a)" |
||

236 | * pp_type valt |
||

237 | * pp_default_val valt |
||

238 | * | Types.Tstruct(l) -> assert false |
||

239 | * | Types.Ttuple(l) -> assert false |
||

240 | * |_ -> *) assert false |
||

241 | |||

242 | e4edf171 | ploc | (* Conversion of basic library functions *) |

243 | |||

244 | c1785a55 | ploc | let horn_basic_app i val_to_expr vl = |

245 | match i, vl with |
||

246 | | "ite", [v1; v2; v3] -> |
||

247 | Z3.Boolean.mk_ite |
||

248 | !ctx |
||

249 | (val_to_expr v1) |
||

250 | (val_to_expr v2) |
||

251 | (val_to_expr v3) |
||

252 | |||

253 | | "uminus", [v] -> |
||

254 | Z3.Arithmetic.mk_unary_minus |
||

255 | !ctx |
||

256 | (val_to_expr v) |
||

257 | | "not", [v] -> |
||

258 | Z3.Boolean.mk_not |
||

259 | !ctx |
||

260 | (val_to_expr v) |
||

261 | | "=", [v1; v2] -> |
||

262 | Z3.Boolean.mk_eq |
||

263 | !ctx |
||

264 | (val_to_expr v1) |
||

265 | (val_to_expr v2) |
||

266 | | "&&", [v1; v2] -> |
||

267 | Z3.Boolean.mk_and |
||

268 | !ctx |
||

269 | [val_to_expr v1; |
||

270 | val_to_expr v2] |
||

271 | | "||", [v1; v2] -> |
||

272 | Z3.Boolean.mk_or |
||

273 | !ctx |
||

274 | [val_to_expr v1; |
||

275 | val_to_expr v2] |
||

276 | |||

277 | | "impl", [v1; v2] -> |
||

278 | Z3.Boolean.mk_implies |
||

279 | !ctx |
||

280 | (val_to_expr v1) |
||

281 | (val_to_expr v2) |
||

282 | | "mod", [v1; v2] -> |
||

283 | Z3.Arithmetic.Integer.mk_mod |
||

284 | !ctx |
||

285 | (val_to_expr v1) |
||

286 | (val_to_expr v2) |
||

287 | | "equi", [v1; v2] -> |
||

288 | Z3.Boolean.mk_eq |
||

289 | !ctx |
||

290 | (val_to_expr v1) |
||

291 | (val_to_expr v2) |
||

292 | | "xor", [v1; v2] -> |
||

293 | Z3.Boolean.mk_xor |
||

294 | !ctx |
||

295 | (val_to_expr v1) |
||

296 | (val_to_expr v2) |
||

297 | | "!=", [v1; v2] -> |
||

298 | Z3.Boolean.mk_not |
||

299 | !ctx |
||

300 | ( |
||

301 | Z3.Boolean.mk_eq |
||

302 | !ctx |
||

303 | (val_to_expr v1) |
||

304 | (val_to_expr v2) |
||

305 | ) |
||

306 | | "/", [v1; v2] -> |
||

307 | Z3.Arithmetic.mk_div |
||

308 | !ctx |
||

309 | (val_to_expr v1) |
||

310 | (val_to_expr v2) |
||

311 | |||

312 | 46cb4020 | ploc | | "+", [v1; v2] -> |

313 | Z3.Arithmetic.mk_add |
||

314 | !ctx |
||

315 | [val_to_expr v1; val_to_expr v2] |
||

316 | |||

317 | | "-", [v1; v2] -> |
||

318 | Z3.Arithmetic.mk_sub |
||

319 | !ctx |
||

320 | [val_to_expr v1 ; val_to_expr v2] |
||

321 | |||

322 | | "*", [v1; v2] -> |
||

323 | Z3.Arithmetic.mk_mul |
||

324 | !ctx |
||

325 | [val_to_expr v1; val_to_expr v2] |
||

326 | |||

327 | |||

328 | | "<", [v1; v2] -> |
||

329 | Z3.Arithmetic.mk_lt |
||

330 | !ctx |
||

331 | (val_to_expr v1) |
||

332 | (val_to_expr v2) |
||

333 | |||

334 | | "<=", [v1; v2] -> |
||

335 | Z3.Arithmetic.mk_le |
||

336 | !ctx |
||

337 | (val_to_expr v1) |
||

338 | (val_to_expr v2) |
||

339 | |||

340 | | ">", [v1; v2] -> |
||

341 | Z3.Arithmetic.mk_gt |
||

342 | !ctx |
||

343 | (val_to_expr v1) |
||

344 | (val_to_expr v2) |
||

345 | |||

346 | | ">=", [v1; v2] -> |
||

347 | Z3.Arithmetic.mk_ge |
||

348 | !ctx |
||

349 | (val_to_expr v1) |
||

350 | (val_to_expr v2) |
||

351 | |||

352 | |||

353 | c1785a55 | ploc | (* | _, [v1; v2] -> Z3.Boolean.mk_and |

354 | * !ctx |
||

355 | * (val_to_expr v1) |
||

356 | * (val_to_expr v2) |
||

357 | * |
||

358 | * Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *) |
||

359 | | _ -> ( |
||

360 | Format.eprintf |
||

361 | "internal error: zustre unkown function %s@." i; |
||

362 | assert false) |
||

363 | |||

364 | |||

365 | 9f3de818 | ploc | (* Convert a value expression [v], with internal function calls only. [pp_var] |

366 | is a printer for variables (typically [pp_c_var_read]), but an offset suffix |
||

367 | may be added for array variables |
||

368 | c1785a55 | ploc | *) |

369 | 51106b7e | ploc | let rec horn_val_to_expr ?(is_lhs=false) m self v = |

370 | c1785a55 | ploc | match v.value_desc with |

371 | | Cst c -> horn_const_to_expr c |
||

372 | |||

373 | (* Code specific for arrays *) |
||

374 | | Array il -> |
||

375 | (* An array definition: |
||

376 | (store ( |
||

377 | ... |
||

378 | (store ( |
||

379 | store ( |
||

380 | default_val |
||

381 | ) |
||

382 | idx_n val_n |
||

383 | ) |
||

384 | idx_n-1 val_n-1) |
||

385 | ... |
||

386 | idx_1 val_1 |
||

387 | ) *) |
||

388 | let rec build_array (tab, x) = |
||

389 | match tab with |
||

390 | | [] -> horn_default_val v.value_type(* (get_type v) *) |
||

391 | | h::t -> |
||

392 | Z3.Z3Array.mk_store |
||

393 | !ctx |
||

394 | (build_array (t, (x+1))) |
||

395 | (Z3.Arithmetic.Integer.mk_numeral_i !ctx x) |
||

396 | 51106b7e | ploc | (horn_val_to_expr ~is_lhs:is_lhs m self h) |

397 | c1785a55 | ploc | in |

398 | build_array (il, 0) |
||

399 | 51106b7e | ploc | |

400 | c1785a55 | ploc | | Access(tab,index) -> |

401 | Z3.Z3Array.mk_select !ctx |
||

402 | 51106b7e | ploc | (horn_val_to_expr ~is_lhs:is_lhs m self tab) |

403 | (horn_val_to_expr ~is_lhs:is_lhs m self index) |
||

404 | c1785a55 | ploc | |

405 | (* Code specific for arrays *) |
||

406 | |||

407 | | Power (v, n) -> assert false |
||

408 | 51106b7e | ploc | | Var v -> |

409 | if is_memory m v then |
||

410 | if Types.is_array_type v.var_type |
||

411 | then assert false |
||

412 | else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) |
||

413 | |||

414 | else |
||

415 | horn_var_to_expr |
||

416 | (rename_machine |
||

417 | self |
||

418 | v) |
||

419 | | Fun (n, vl) -> horn_basic_app n (horn_val_to_expr m self) vl |
||

420 | c1785a55 | ploc | |

421 | let no_reset_to_exprs machines m i = |
||

422 | let (n,_) = List.assoc i m.minstances in |
||

423 | let target_machine = List.find (fun m -> m.mname.node_id = (Corelang.node_name n)) machines in |
||

424 | ad4774b0 | ploc | |

425 | c1785a55 | ploc | let m_list = |

426 | rename_machine_list |
||

427 | (concat m.mname.node_id i) |
||

428 | (rename_mid_list (full_memory_vars machines target_machine)) |
||

429 | in |
||

430 | let c_list = |
||

431 | rename_machine_list |
||

432 | (concat m.mname.node_id i) |
||

433 | (rename_current_list (full_memory_vars machines target_machine)) |
||

434 | in |
||

435 | match c_list, m_list with |
||

436 | | [chd], [mhd] -> |
||

437 | let expr = |
||

438 | Z3.Boolean.mk_eq !ctx |
||

439 | (horn_var_to_expr mhd) |
||

440 | (horn_var_to_expr chd) |
||

441 | in |
||

442 | [expr] |
||

443 | | _ -> ( |
||

444 | let exprs = |
||

445 | List.map2 (fun mhd chd -> |
||

446 | Z3.Boolean.mk_eq !ctx |
||

447 | (horn_var_to_expr mhd) |
||

448 | (horn_var_to_expr chd) |
||

449 | ) |
||

450 | m_list |
||

451 | c_list |
||

452 | in |
||

453 | exprs |
||

454 | ) |
||

455 | |||

456 | let instance_reset_to_exprs machines m i = |
||

457 | let (n,_) = List.assoc i m.minstances in |
||

458 | let target_machine = List.find (fun m -> m.mname.node_id = (Corelang.node_name n)) machines in |
||

459 | let vars = |
||

460 | 7d77632f | ploc | (rename_machine_list |

461 | (concat m.mname.node_id i) |
||

462 | (rename_current_list (full_memory_vars machines target_machine))@ (rename_mid_list (full_memory_vars machines target_machine)) |
||

463 | c1785a55 | ploc | ) |

464 | 7d77632f | ploc | |

465 | c1785a55 | ploc | in |

466 | let expr = |
||

467 | Z3.Expr.mk_app |
||

468 | !ctx |
||

469 | (get_fdecl (machine_reset_name (Corelang.node_name n))) |
||

470 | 7d77632f | ploc | (List.map (horn_var_to_expr) (idx::uid::vars)) |

471 | c1785a55 | ploc | in |

472 | [expr] |
||

473 | |||

474 | let instance_call_to_exprs machines reset_instances m i inputs outputs = |
||

475 | let self = m.mname.node_id in |
||

476 | 7d77632f | ploc | |

477 | (* Building call args *) |
||

478 | let idx_uid_inout = |
||

479 | (* Additional input to register step counters, and uid *) |
||

480 | let idx = horn_var_to_expr idx in |
||

481 | let uid = uid_conc (get_instance_uid i) (horn_var_to_expr uid) in |
||

482 | let inout = |
||

483 | 51106b7e | ploc | List.map (horn_val_to_expr m self) |

484 | (inputs @ (List.map (fun v -> mk_val (Var v) v.var_type) outputs)) |
||

485 | 7d77632f | ploc | in |

486 | idx::uid::inout |
||

487 | in |
||

488 | |||

489 | c1785a55 | ploc | try (* stateful node instance *) |

490 | begin |
||

491 | let (n,_) = List.assoc i m.minstances in |
||

492 | let target_machine = List.find (fun m -> m.mname.node_id = Corelang.node_name n) machines in |
||

493 | |||

494 | (* Checking whether this specific instances has been reset yet *) |
||

495 | let reset_exprs = |
||

496 | if not (List.mem i reset_instances) then |
||

497 | (* If not, declare mem_m = mem_c *) |
||

498 | no_reset_to_exprs machines m i |
||

499 | else |
||

500 | [] (* Nothing to add yet *) |
||

501 | in |
||

502 | |||

503 | let mems = full_memory_vars machines target_machine in |
||

504 | let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in |
||

505 | let mid_mems = rename_mems rename_mid_list in |
||

506 | let next_mems = rename_mems rename_next_list in |
||

507 | |||

508 | let call_expr = |
||

509 | 7d77632f | ploc | match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with |

510 | | "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin |
||

511 | c1785a55 | ploc | let stmt1 = (* out = ite mem_m then i1 else i2 *) |

512 | Z3.Boolean.mk_eq !ctx |
||

513 | ( (* output var *) |
||

514 | 51106b7e | ploc | horn_val_to_expr |

515 | c1785a55 | ploc | ~is_lhs:true |

516 | 51106b7e | ploc | m self |

517 | (mk_val (Var o) o.var_type) |
||

518 | c1785a55 | ploc | ) |

519 | ( |
||

520 | Z3.Boolean.mk_ite !ctx |
||

521 | (horn_var_to_expr mem_m) |
||

522 | 51106b7e | ploc | (horn_val_to_expr m self i1) |

523 | (horn_val_to_expr m self i2) |
||

524 | c1785a55 | ploc | ) |

525 | in |
||

526 | let stmt2 = (* mem_X = false *) |
||

527 | Z3.Boolean.mk_eq !ctx |
||

528 | (horn_var_to_expr mem_x) |
||

529 | (Z3.Boolean.mk_false !ctx) |
||

530 | in |
||

531 | [stmt1; stmt2] |
||

532 | 7d77632f | ploc | end |

533 | |||

534 | | node_name_n -> |
||

535 | let expr = |
||

536 | Z3.Expr.mk_app |
||

537 | !ctx |
||

538 | (get_fdecl (machine_step_name (node_name n))) |
||

539 | ( (* Arguments are input, output, mid_mems, next_mems *) |
||

540 | idx_uid_inout @ List.map (horn_var_to_expr) (mid_mems@next_mems) |
||

541 | |||

542 | ) |
||

543 | in |
||

544 | [expr] |
||

545 | c1785a55 | ploc | in |

546 | |||

547 | reset_exprs@call_expr |
||

548 | end |
||

549 | with Not_found -> ( (* stateless node instance *) |
||

550 | let (n,_) = List.assoc i m.mcalls in |
||

551 | let expr = |
||

552 | Z3.Expr.mk_app |
||

553 | !ctx |
||

554 | (get_fdecl (machine_stateless_name (node_name n))) |
||

555 | 7d77632f | ploc | idx_uid_inout (* Arguments are inputs, outputs *) |

556 | c1785a55 | ploc | in |

557 | [expr] |
||

558 | ) |
||

559 | e4edf171 | ploc | |

560 | |||

561 | |||

562 | (* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *) |
||

563 | (* let rec value_suffix_to_expr self value = *) |
||

564 | (* match value.value_desc with *) |
||

565 | (* | Fun (n, vl) -> *) |
||

566 | (* horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *) |
||

567 | c1785a55 | ploc | |

568 | e4edf171 | ploc | (* | _ -> *) |

569 | (* horn_val_to_expr self value *) |
||

570 | |||

571 | c1785a55 | ploc | |

572 | e4edf171 | ploc | (* type_directed assignment: array vs. statically sized type |

573 | - [var_type]: type of variable to be assigned |
||

574 | - [var_name]: name of variable to be assigned |
||

575 | - [value]: assigned value |
||

576 | - [pp_var]: printer for variables |
||

577 | *) |
||

578 | let assign_to_exprs m var_name value = |
||

579 | let self = m.mname.node_id in |
||

580 | let e = |
||

581 | Z3.Boolean.mk_eq |
||

582 | !ctx |
||

583 | 51106b7e | ploc | (horn_val_to_expr ~is_lhs:true m self var_name) |

584 | (horn_val_to_expr m self value) |
||

585 | e4edf171 | ploc | (* was: TODO deal with array accesses (value_suffix_to_expr self value) *) |

586 | in |
||

587 | [e] |
||

588 | |||

589 | |||

590 | c1785a55 | ploc | (* Convert instruction to Z3.Expr and update the set of reset instances *) |

591 | e4edf171 | ploc | let rec instr_to_exprs machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list = |

592 | ff2d7a82 | ploc | match Corelang.get_instr_desc instr with |

593 | c1785a55 | ploc | | MComment _ -> [], reset_instances |

594 | | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *) |
||

595 | no_reset_to_exprs machines m i, |
||

596 | i::reset_instances |
||

597 | | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *) |
||

598 | instance_reset_to_exprs machines m i, |
||

599 | i::reset_instances |
||

600 | | MLocalAssign (i,v) -> |
||

601 | assign_to_exprs |
||

602 | e4edf171 | ploc | m |

603 | 51106b7e | ploc | (mk_val (Var i) i.var_type) v, |

604 | c1785a55 | ploc | reset_instances |

605 | | MStateAssign (i,v) -> |
||

606 | assign_to_exprs |
||

607 | e4edf171 | ploc | m |

608 | 51106b7e | ploc | (mk_val (Var i) i.var_type) v, |

609 | c1785a55 | ploc | reset_instances |

610 | | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) -> |
||

611 | assert false (* This should not happen anymore *) |
||

612 | | MStep (il, i, vl) -> |
||

613 | (* if reset instance, just print the call over mem_m , otherwise declare mem_m = |
||

614 | mem_c and print the call to mem_m *) |
||

615 | instance_call_to_exprs machines reset_instances m i vl il, |
||

616 | reset_instances (* Since this instance call will only happen once, we |
||

617 | don't have to update reset_instances *) |
||

618 | |||

619 | | MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ... |
||

620 | should not be produced yet. Later, we will have to |
||

621 | compare the reset_instances of each branch and |
||

622 | introduced the mem_m = mem_c for branches to do not |
||

623 | address it while other did. Am I clear ? *) |
||

624 | (* For each branch we obtain the logical encoding, and the information |
||

625 | whether a sub node has been reset or not. If a node has been reset in one |
||

626 | of the branch, then all others have to have the mem_m = mem_c |
||

627 | statement. *) |
||

628 | let self = m.mname.node_id in |
||

629 | let branch_to_expr (tag, instrs) = |
||

630 | e4edf171 | ploc | let branch_def, branch_resets = instrs_to_expr machines reset_instances m instrs in |

631 | let e = |
||

632 | Z3.Boolean.mk_implies !ctx |
||

633 | (Z3.Boolean.mk_eq !ctx |
||

634 | 51106b7e | ploc | (horn_val_to_expr m self g) |

635 | e4edf171 | ploc | (horn_tag_to_expr tag)) |

636 | branch_def in |
||

637 | |||

638 | [e], branch_resets |
||

639 | |||

640 | c1785a55 | ploc | in |

641 | e4edf171 | ploc | List.fold_left (fun (instrs, resets) b -> |

642 | let b_instrs, b_resets = branch_to_expr b in |
||

643 | instrs@b_instrs, resets@b_resets |
||

644 | ) ([], reset_instances) hl |
||

645 | c1785a55 | ploc | |

646 | and instrs_to_expr machines reset_instances m instrs = |
||

647 | e4edf171 | ploc | let instr_to_exprs rs i = instr_to_exprs machines rs m i in |

648 | let e_list, rs = |
||

649 | match instrs with |
||

650 | | [x] -> instr_to_exprs reset_instances x |
||

651 | | _::_ -> (* TODO: check whether we should compuyte a AND on the exprs (expr list) built here. It was performed in the printer setting but seems to be useless here since the output is a list of exprs *) |
||

652 | |||

653 | List.fold_left (fun (exprs, rs) i -> |
||

654 | let exprs_i, rs_i = instr_to_exprs rs i in |
||

655 | exprs@exprs_i, rs@rs_i |
||

656 | ) |
||

657 | ([], reset_instances) instrs |
||

658 | |||

659 | |||

660 | | [] -> [], reset_instances |
||

661 | in |
||

662 | let e = |
||

663 | match e_list with |
||

664 | | [e] -> e |
||

665 | | [] -> Z3.Boolean.mk_true !ctx |
||

666 | | _ -> Z3.Boolean.mk_and !ctx e_list |
||

667 | in |
||

668 | e, rs |
||

669 | ff2d7a82 | ploc | |

670 | 51ec4e8c | ploc | |

671 | (*********************************************************) |
||

672 | |||

673 | (* Quantifiying universally all occuring variables *) |
||

674 | let add_rule ?(dont_touch=[]) vars expr = |
||

675 | (* let fds = Z3.Expr.get_args expr in *) |
||

676 | (* Format.eprintf "Expr %s: args: [%a]@." *) |
||

677 | (* (Z3.Expr.to_string expr) *) |
||

678 | (* (Utils.fprintf_list ~sep:", " (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e))) fds; *) |
||

679 | |||

680 | (* (\* Old code relying on provided vars *\) *) |
||

681 | (* let sorts = (List.map (fun id -> type_to_sort id.var_type) vars) in *) |
||

682 | (* let symbols = (List.map (fun id -> Z3.FuncDecl.get_name (get_fdecl id.var_id)) vars) in *) |
||

683 | |||

684 | (* New code: we extract vars from expr *) |
||

685 | let module FDSet = Set.Make (struct type t = Z3.FuncDecl.func_decl |
||

686 | let compare = compare |
||

687 | let hash = Hashtbl.hash |
||

688 | end) |
||

689 | in |
||

690 | let rec get_expr_vars e = |
||

691 | let open Utils in |
||

692 | let nb_args = Z3.Expr.get_num_args e in |
||

693 | if nb_args <= 0 then ( |
||

694 | let fdecl = Z3.Expr.get_func_decl e in |
||

695 | (* let params = Z3.FuncDecl.get_parameters fdecl in *) |
||

696 | dbab1fe5 | ploc | (* Format.eprintf "Extracting info about %s: @." (Z3.Expr.to_string e); *) |

697 | 51ec4e8c | ploc | let dkind = Z3.FuncDecl.get_decl_kind fdecl in |

698 | match dkind with Z3enums.OP_UNINTERPRETED -> ( |
||

699 | (* Format.eprintf "kind = %s, " (match dkind with Z3enums.OP_TRUE -> "true" | Z3enums.OP_UNINTERPRETED -> "uninter"); *) |
||

700 | (* let open Z3.FuncDecl.Parameter in *) |
||

701 | (* List.iter (fun p -> *) |
||

702 | (* match p with *) |
||

703 | (* P_Int i -> Format.eprintf "int %i" i *) |
||

704 | (* | P_Dbl f -> Format.eprintf "dbl %f" f *) |
||

705 | (* | P_Sym s -> Format.eprintf "symb" *) |
||

706 | (* | P_Srt s -> Format.eprintf "sort" *) |
||

707 | (* | P_Ast _ ->Format.eprintf "ast" *) |
||

708 | (* | P_Fdl f -> Format.eprintf "fundecl" *) |
||

709 | (* | P_Rat s -> Format.eprintf "rat %s" s *) |
||

710 | |||

711 | (* ) params; *) |
||

712 | (* Format.eprintf "]@."; *) |
||

713 | FDSet.singleton fdecl |
||

714 | ) |
||

715 | | _ -> FDSet.empty |
||

716 | ) |
||

717 | else (*if nb_args > 0 then*) |
||

718 | List.fold_left |
||

719 | (fun accu e -> FDSet.union accu (get_expr_vars e)) |
||

720 | FDSet.empty (Z3.Expr.get_args e) |
||

721 | in |
||

722 | let extracted_vars = FDSet.elements (FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in |
||

723 | let extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in |
||

724 | let extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in |
||

725 | |||

726 | 4300981b | ploc | if !debug then ( |

727 | Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%a@ ]@]@ @." |
||

728 | (Z3.Expr.to_string expr) |
||

729 | (Utils.fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) (List.map horn_var_to_expr vars) |
||

730 | ) |
||

731 | ; |
||

732 | 51ec4e8c | ploc | let expr = Z3.Quantifier.mk_forall_const |

733 | !ctx (* context *) |
||

734 | (List.map horn_var_to_expr vars) (* TODO provide bounded variables as expr *) |
||

735 | (* sorts (\* sort list*\) *) |
||

736 | (* symbols (\* symbol list *\) *) |
||

737 | expr (* expression *) |
||

738 | None (* quantifier weight, None means 1 *) |
||

739 | [] (* pattern list ? *) |
||

740 | [] (* ? *) |
||

741 | None (* ? *) |
||

742 | None (* ? *) |
||

743 | in |
||

744 | dbab1fe5 | ploc | (* Format.eprintf "OK@.@?"; *) |

745 | 51ec4e8c | ploc | |

746 | 9f3de818 | ploc | (* |

747 | TODO: bizarre la declaration de INIT tout seul semble poser pb. |
||

748 | *) |
||

749 | 51ec4e8c | ploc | Z3.Fixedpoint.add_rule !fp |

750 | (Z3.Quantifier.expr_of_quantifier expr) |
||

751 | None |
||

752 | |||

753 | 9f3de818 | ploc | |

754 | 51ec4e8c | ploc | (********************************************************) |

755 | |||

756 | e4edf171 | ploc | let machine_reset machines m = |

757 | let locals = local_memory_vars machines m in |
||

758 | |||

759 | (* print "x_m = x_c" for each local memory *) |
||

760 | let mid_mem_def = |
||

761 | List.map (fun v -> |
||

762 | Z3.Boolean.mk_eq !ctx |
||

763 | (horn_var_to_expr (rename_mid v)) |
||

764 | (horn_var_to_expr (rename_current v)) |
||

765 | ) locals |
||

766 | in |
||

767 | ff2d7a82 | ploc | |

768 | e4edf171 | ploc | (* print "child_reset ( associated vars _ {c,m} )" for each subnode. |

769 | Special treatment for _arrow: _first = true |
||

770 | *) |
||

771 | |||

772 | let reset_instances = |
||

773 | |||

774 | List.map (fun (id, (n, _)) -> |
||

775 | let name = node_name n in |
||

776 | if name = "_arrow" then ( |
||

777 | Z3.Boolean.mk_eq !ctx |
||

778 | ( |
||

779 | let vdecl = get_fdecl ((concat m.mname.node_id id) ^ "._arrow._first_m") in |
||

780 | Z3.Expr.mk_const_f !ctx vdecl |
||

781 | ) |
||

782 | (Z3.Boolean.mk_true !ctx) |
||

783 | |||

784 | ) else ( |
||

785 | let machine_n = get_machine machines name in |
||

786 | |||

787 | Z3.Expr.mk_app |
||

788 | !ctx |
||

789 | (get_fdecl (name ^ "_reset")) |
||

790 | (List.map (horn_var_to_expr) |
||

791 | 7d77632f | ploc | (idx::uid:: (* Additional vars: counters, uid *) |

792 | (rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n)) |
||

793 | )) |
||

794 | e4edf171 | ploc | |

795 | ) |
||

796 | ) m.minstances |
||

797 | |||

798 | |||

799 | ff2d7a82 | ploc | in |

800 | e4edf171 | ploc | |

801 | Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances) |
||

802 | |||

803 | |||

804 | ff2d7a82 | ploc | |

805 | e4edf171 | ploc | (* TODO: empty list means true statement *) |

806 | ad4774b0 | ploc | let decl_machine machines m = |

807 | e4edf171 | ploc | if m.mname.node_id = Arrow.arrow_id then |

808 | (* We don't do arrow function *) |
||

809 | ad4774b0 | ploc | () |

810 | else |
||

811 | begin |
||

812 | 5778dd5e | ploc | let _ = |

813 | List.map decl_var |
||

814 | c1785a55 | ploc | ( |

815 | 5778dd5e | ploc | (inout_vars machines m)@ |

816 | (rename_current_list (full_memory_vars machines m)) @ |
||

817 | (rename_mid_list (full_memory_vars machines m)) @ |
||

818 | (rename_next_list (full_memory_vars machines m)) @ |
||

819 | (rename_machine_list m.mname.node_id m.mstep.step_locals) |
||

820 | ) |
||

821 | ad4774b0 | ploc | in |

822 | if is_stateless m then |
||

823 | begin |
||

824 | 4300981b | ploc | if !debug then |

825 | Format.eprintf "Declaring a stateless machine: %s@." m.mname.node_id; |
||

826 | |||

827 | ad4774b0 | ploc | (* Declaring single predicate *) |

828 | 5778dd5e | ploc | let vars = inout_vars machines m in |

829 | 2f7c9195 | ploc | let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in |

830 | let _ = decl_rel (machine_stateless_name m.mname.node_id) vars_types in |
||

831 | 4300981b | ploc | |

832 | e4edf171 | ploc | let horn_body, _ (* don't care for reset here *) = |

833 | instrs_to_expr |
||

834 | machines |
||

835 | ([] (* No reset info for stateless nodes *) ) |
||

836 | m |
||

837 | m.mstep.step_instrs |
||

838 | in |
||

839 | let horn_head = |
||

840 | Z3.Expr.mk_app |
||

841 | !ctx |
||

842 | (get_fdecl (machine_stateless_name m.mname.node_id)) |
||

843 | 7d77632f | ploc | ( List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars)) |

844 | e4edf171 | ploc | in |

845 | 4300981b | ploc | (* this line seems useless *) |

846 | 7d77632f | ploc | let vars = idx::uid::vars@(rename_machine_list m.mname.node_id m.mstep.step_locals) in |

847 | 4300981b | ploc | (* Format.eprintf "useless Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *) |

848 | e4edf171 | ploc | match m.mstep.step_asserts with |

849 | ad4774b0 | ploc | | [] -> |

850 | begin |
||

851 | e4edf171 | ploc | (* Rule for single predicate : "; Stateless step rule @." *) |

852 | 4300981b | ploc | (*let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in*) |

853 | (* TODO clean code *) |
||

854 | (* Format.eprintf "used Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *) |
||

855 | 5778dd5e | ploc | add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head) |

856 | |||

857 | ad4774b0 | ploc | end |

858 | | assertsl -> |
||

859 | begin |
||

860 | e4edf171 | ploc | (*Rule for step "; Stateless step rule with Assertions @.";*) |

861 | let body_with_asserts = |
||

862 | 51106b7e | ploc | Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl) |

863 | e4edf171 | ploc | in |

864 | 51ec4e8c | ploc | let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in |

865 | 5778dd5e | ploc | add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head) |

866 | ad4774b0 | ploc | end |

867 | end |
||

868 | else |
||

869 | begin |
||

870 | |||

871 | (* Rule for reset *) |
||

872 | |||

873 | 5778dd5e | ploc | let vars = reset_vars machines m in |

874 | 2f7c9195 | ploc | let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in |

875 | let _ = decl_rel (machine_reset_name m.mname.node_id) vars_types in |
||

876 | e4edf171 | ploc | let horn_reset_body = machine_reset machines m in |

877 | let horn_reset_head = |
||

878 | Z3.Expr.mk_app |
||

879 | !ctx |
||

880 | (get_fdecl (machine_reset_name m.mname.node_id)) |
||

881 | 7d77632f | ploc | ( List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars)) |

882 | e4edf171 | ploc | in |

883 | 51ec4e8c | ploc | |

884 | e4edf171 | ploc | |

885 | let _ = |
||

886 | 7d77632f | ploc | add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head) |

887 | 5778dd5e | ploc | |

888 | e4edf171 | ploc | in |

889 | |||

890 | (* Rule for step*) |
||

891 | 5778dd5e | ploc | let vars = step_vars machines m in |

892 | 2f7c9195 | ploc | let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in |

893 | let _ = decl_rel (machine_step_name m.mname.node_id) vars_types in |
||

894 | e4edf171 | ploc | let horn_step_body, _ (* don't care for reset here *) = |

895 | instrs_to_expr |
||

896 | machines |
||

897 | [] |
||

898 | m |
||

899 | m.mstep.step_instrs |
||

900 | in |
||

901 | let horn_step_head = |
||

902 | Z3.Expr.mk_app |
||

903 | !ctx |
||

904 | (get_fdecl (machine_step_name m.mname.node_id)) |
||

905 | 7d77632f | ploc | ( List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars)) |

906 | e4edf171 | ploc | in |

907 | match m.mstep.step_asserts with |
||

908 | ad4774b0 | ploc | | [] -> |

909 | begin |
||

910 | dbab1fe5 | ploc | (* Rule for single predicate *) |

911 | let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in |
||

912 | 7d77632f | ploc | add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head) |

913 | 5778dd5e | ploc | |

914 | ad4774b0 | ploc | end |

915 | e4edf171 | ploc | | assertsl -> |

916 | ad4774b0 | ploc | begin |

917 | e4edf171 | ploc | (* Rule for step Assertions @.; *) |

918 | let body_with_asserts = |
||

919 | Z3.Boolean.mk_and !ctx |
||

920 | 51106b7e | ploc | (horn_step_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl) |

921 | e4edf171 | ploc | in |

922 | dbab1fe5 | ploc | let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in |

923 | 7d77632f | ploc | add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head) |

924 | 5778dd5e | ploc | |

925 | ad4774b0 | ploc | end |

926 | |||

927 | end |
||

928 | c1785a55 | ploc | end |

929 | ad4774b0 | ploc | |

930 | c1785a55 | ploc | |

931 | 51ec4e8c | ploc | |

932 | (* Debug functions *) |
||

933 | |||

934 | let rec extract_expr_fds e = |
||

935 | dbab1fe5 | ploc | (* Format.eprintf "@[<v 2>Extracting fundecls from expr %s@ " *) |

936 | (* (Z3.Expr.to_string e); *) |
||

937 | 51ec4e8c | ploc | |

938 | (* Removing quantifier is there are some *) |
||

939 | let e = (* I didn't found a nicer way to do it than with an exception. My |
||

940 | bad *) |
||

941 | try |
||

942 | let eq = Z3.Quantifier.quantifier_of_expr e in |
||

943 | let e2 = Z3.Quantifier.get_body eq in |
||

944 | dbab1fe5 | ploc | (* Format.eprintf "Extracted quantifier body@ "; *) |

945 | 51ec4e8c | ploc | e2 |

946 | |||

947 | with _ -> Format.eprintf "No quantifier info@ "; e |
||

948 | in |
||

949 | let _ = |
||

950 | try |
||

951 | ( |
||

952 | let fd = Z3.Expr.get_func_decl e in |
||

953 | let fd_symbol = Z3.FuncDecl.get_name fd in |
||

954 | let fd_name = Z3.Symbol.to_string fd_symbol in |
||

955 | if not (Hashtbl.mem decls fd_name) then |
||

956 | register_fdecl fd_name fd; |
||

957 | dbab1fe5 | ploc | (* Format.eprintf "fdecls (%s): %s@ " *) |

958 | (* fd_name *) |
||

959 | (* (Z3.FuncDecl.to_string fd); *) |
||

960 | 51ec4e8c | ploc | try |

961 | ( |
||

962 | let args = Z3.Expr.get_args e in |
||

963 | dbab1fe5 | ploc | (* Format.eprintf "@[<v>@ "; *) |

964 | (* List.iter extract_expr_fds args; *) |
||

965 | (* Format.eprintf "@]@ "; *) |
||

966 | () |
||

967 | 51ec4e8c | ploc | ) |

968 | with _ -> |
||

969 | Format.eprintf "Impossible to extract fundecl args for expression %s@ " |
||

970 | (Z3.Expr.to_string e) |
||

971 | ) |
||

972 | with _ -> |
||

973 | Format.eprintf "Impossible to extract anything from expression %s@ " |
||

974 | (Z3.Expr.to_string e) |
||

975 | in |
||

976 | dbab1fe5 | ploc | (* Format.eprintf "@]@ " *) |

977 | () |
||

978 | 51ec4e8c | ploc | |

979 | 5778dd5e | ploc | (* Local Variables: *) |

980 | (* compile-command:"make -C ../.." *) |
||

981 | (* End: *) |