## lustrec / src / tools / seal / seal_extract.ml @ d75eb6f1

History | View | Annotate | Download (40.1 KB)

1 | 0d79d0f3 | ploc | open Lustre_types |
---|---|---|---|

2 | open Utils |
||

3 | open Seal_utils |
||

4 | 8c934ccd | ploc | open Zustre_data (* Access to Z3 context *) |

5 | |||

6 | 0d79d0f3 | ploc | |

7 | 3b7f916b | ploc | (* Switched system extraction: expression are memoized *) |

8 | (*let expr_mem = Hashtbl.create 13*) |
||

9 | |||

10 | 0d79d0f3 | ploc | type element = IsInit | Expr of expr |

11 | 3b7f916b | ploc | |

12 | 0d79d0f3 | ploc | type guard = (element * bool) list |

13 | type guarded_expr = guard * element |
||

14 | type mdef_t = guarded_expr list |
||

15 | |||

16 | let pp_elem fmt e = |
||

17 | match e with |
||

18 | | IsInit -> Format.fprintf fmt "init" |
||

19 | 3b7f916b | ploc | | Expr e -> Format.fprintf fmt "%a" Printers.pp_expr e |

20 | 0d79d0f3 | ploc | |

21 | 7aaacbc9 | ploc | let pp_guard_list fmt gl = |

22 | (fprintf_list ~sep:"; " |
||

23 | (fun fmt (e,b) -> if b then pp_elem fmt e else Format.fprintf fmt "not(%a)" pp_elem e)) fmt gl |
||

24 | |||

25 | 0d79d0f3 | ploc | let pp_guard_expr fmt (gl,e) = |

26 | Format.fprintf fmt "%a -> %a" |
||

27 | 7aaacbc9 | ploc | pp_guard_list gl |

28 | 0d79d0f3 | ploc | pp_elem e |

29 | |||

30 | let pp_mdefs fmt gel = fprintf_list ~sep:"@ " pp_guard_expr fmt gel |
||

31 | |||

32 | |||

33 | let add_init defs vid = |
||

34 | Hashtbl.add defs vid [[], IsInit] |
||

35 | |||

36 | let deelem e = match e with |
||

37 | Expr e -> e |
||

38 | | IsInit -> assert false (* Wasn't expecting isinit here: we are building values! *) |
||

39 | |||

40 | let is_eq_elem elem elem' = |
||

41 | match elem, elem' with |
||

42 | | IsInit, IsInit -> true |
||

43 | 3b7f916b | ploc | | Expr e, Expr e' -> e = e' (* |

44 | Corelang.is_eq_expr e e' *) |
||

45 | 0d79d0f3 | ploc | | _ -> false |

46 | |||

47 | let select_elem elem (gelem, _) = |
||

48 | is_eq_elem elem gelem |
||

49 | |||

50 | 8c934ccd | ploc | |

51 | (**************************************************************) |
||

52 | (* Convert from Lustre expressions to Z3 expressions and back *) |
||

53 | (* All (free) variables have to be declared in the Z3 context *) |
||

54 | (**************************************************************) |
||

55 | |||

56 | let is_init_name = "__is_init" |
||

57 | |||

58 | let const_defs = Hashtbl.create 13 |
||

59 | let is_const id = Hashtbl.mem const_defs id |
||

60 | let get_const id = Hashtbl.find const_defs id |
||

61 | |||

62 | (* expressions are only basic constructs here, no more ite, tuples, |
||

63 | arrows, fby, ... *) |
||

64 | 3b7f916b | ploc | |

65 | (* Set of hash to support memoization *) |
||

66 | let expr_hash: (expr * Utils.tag) list ref = ref [] |
||

67 | let ze_hash: (Z3.Expr.expr, Utils.tag) Hashtbl.t = Hashtbl.create 13 |
||

68 | let e_hash: (Utils.tag, Z3.Expr.expr) Hashtbl.t = Hashtbl.create 13 |
||

69 | let pp_hash pp_key pp_v fmt h = Hashtbl.iter (fun key v -> Format.fprintf fmt "%a -> %a@ " pp_key key pp_v v) h |
||

70 | let pp_e_map fmt = List.iter (fun (e,t) -> Format.fprintf fmt "%i -> %a@ " t Printers.pp_expr e) !expr_hash |
||

71 | let pp_ze_hash fmt = pp_hash |
||

72 | (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e)) |
||

73 | Format.pp_print_int |
||

74 | fmt |
||

75 | ze_hash |
||

76 | let pp_e_hash fmt = pp_hash |
||

77 | Format.pp_print_int |
||

78 | (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e)) |
||

79 | fmt |
||

80 | e_hash |
||

81 | let mem_expr e = |
||

82 | (* Format.eprintf "Searching for %a in map: @[<v 0>%t@]" |
||

83 | * Printers.pp_expr e |
||

84 | * pp_e_map; *) |
||

85 | let res = List.exists (fun (e',_) -> Corelang.is_eq_expr e e') !expr_hash in |
||

86 | (* Format.eprintf "found?%b@." res; *) |
||

87 | res |
||

88 | |||

89 | let mem_zexpr ze = |
||

90 | Hashtbl.mem ze_hash ze |
||

91 | let get_zexpr e = |
||

92 | let eref, uid = List.find (fun (e',_) -> Corelang.is_eq_expr e e') !expr_hash in |
||

93 | (* Format.eprintf "found expr=%a id=%i@." Printers.pp_expr eref eref.expr_tag; *) |
||

94 | Hashtbl.find e_hash uid |
||

95 | let get_expr ze = |
||

96 | let uid = Hashtbl.find ze_hash ze in |
||

97 | let e,_ = List.find (fun (e,t) -> t = uid) !expr_hash in |
||

98 | e |
||

99 | |||

100 | let neg_ze z3e = Z3.Boolean.mk_not !ctx z3e |
||

101 | let is_init_z3e = |
||

102 | Z3.Expr.mk_const_s !ctx is_init_name Zustre_common.bool_sort |
||

103 | |||

104 | let get_zid (ze:Z3.Expr.expr) : Utils.tag = |
||

105 | try |
||

106 | if Z3.Expr.equal ze is_init_z3e then -1 else |
||

107 | if Z3.Expr.equal ze (neg_ze is_init_z3e) then -2 else |
||

108 | Hashtbl.find ze_hash ze |
||

109 | with _ -> (Format.eprintf "Looking for ze %s in Hash %a" |
||

110 | (Z3.Expr.to_string ze) |
||

111 | (fun fmt hash -> Hashtbl.iter (fun ze uid -> Format.fprintf fmt "%s -> %i@ " (Z3.Expr.to_string ze) uid) hash ) ze_hash; |
||

112 | assert false) |
||

113 | let add_expr = |
||

114 | let cpt = ref 0 in |
||

115 | fun e ze -> |
||

116 | incr cpt; |
||

117 | let uid = !cpt in |
||

118 | expr_hash := (e, uid)::!expr_hash; |
||

119 | Hashtbl.add e_hash uid ze; |
||

120 | Hashtbl.add ze_hash ze uid |
||

121 | |||

122 | |||

123 | 8c934ccd | ploc | let expr_to_z3_expr, zexpr_to_expr = |

124 | 47851ec2 | ploc | (* List to store converted expression. *) |

125 | 3b7f916b | ploc | (* let hash = ref [] in |

126 | * let comp_expr e (e', _) = Corelang.is_eq_expr e e' in |
||

127 | * let comp_zexpr ze (_, ze') = Z3.Expr.equal ze ze' in *) |
||

128 | |||

129 | 8c934ccd | ploc | let rec e2ze e = |

130 | if mem_expr e then ( |
||

131 | get_zexpr e |
||

132 | ) |
||

133 | else ( |
||

134 | let res = |
||

135 | match e.expr_desc with |
||

136 | | Expr_const c -> |
||

137 | let z3e = Zustre_common.horn_const_to_expr c in |
||

138 | add_expr e z3e; |
||

139 | z3e |
||

140 | | Expr_ident id -> ( |
||

141 | if is_const id then ( |
||

142 | let c = get_const id in |
||

143 | let z3e = Zustre_common.horn_const_to_expr c in |
||

144 | add_expr e z3e; |
||

145 | z3e |
||

146 | ) |
||

147 | else ( |
||

148 | let fdecl_id = Zustre_common.get_fdecl id in |
||

149 | let z3e = Z3.Expr.mk_const_f !ctx fdecl_id in |
||

150 | add_expr e z3e; |
||

151 | z3e |
||

152 | ) |
||

153 | ) |
||

154 | | Expr_appl (id,args, None) (* no reset *) -> |
||

155 | let z3e = Zustre_common.horn_basic_app id e2ze (Corelang.expr_list_of_expr args) in |
||

156 | add_expr e z3e; |
||

157 | z3e |
||

158 | 47851ec2 | ploc | | Expr_tuple [e] -> |

159 | let z3e = e2ze e in |
||

160 | add_expr e z3e; |
||

161 | z3e |
||

162 | | _ -> ( match e.expr_desc with Expr_tuple _ -> Format.eprintf "tuple e2ze(%a)@.@?" Printers.pp_expr e |
||

163 | | _ -> Format.eprintf "e2ze(%a)@.@?" Printers.pp_expr e) |
||

164 | ; assert false |
||

165 | 8c934ccd | ploc | in |

166 | res |
||

167 | ) |
||

168 | in |
||

169 | let rec ze2e ze = |
||

170 | let ze_name ze = |
||

171 | let fd = Z3.Expr.get_func_decl ze in |
||

172 | Z3.Symbol.to_string (Z3.FuncDecl.get_name fd) |
||

173 | in |
||

174 | if mem_zexpr ze then |
||

175 | None, Some (get_expr ze) |
||

176 | else |
||

177 | let open Corelang in |
||

178 | let fd = Z3.Expr.get_func_decl ze in |
||

179 | let zel = Z3.Expr.get_args ze in |
||

180 | match Z3.Symbol.to_string (Z3.FuncDecl.get_name fd), zel with |
||

181 | (* | var, [] -> (* should be in env *) get_e *) |
||

182 | |||

183 | (* Extracting IsInit status *) |
||

184 | | "not", [ze] when ze_name ze = is_init_name -> |
||

185 | Some false, None |
||

186 | | name, [] when name = is_init_name -> Some true, None |
||

187 | (* Other constructs are converted to a lustre expression *) |
||

188 | | op, _ -> ( |
||

189 | |||

190 | |||

191 | if Z3.Expr.is_numeral ze then |
||

192 | let e = |
||

193 | if Z3.Arithmetic.is_real ze then |
||

194 | let num = Num.num_of_ratio (Z3.Arithmetic.Real.get_ratio ze) in |
||

195 | let s = Z3.Arithmetic.Real.numeral_to_string ze in |
||

196 | mkexpr |
||

197 | Location.dummy_loc |
||

198 | (Expr_const |
||

199 | (Const_real |
||

200 | (num, 0, s))) |
||

201 | else if Z3.Arithmetic.is_int ze then |
||

202 | mkexpr |
||

203 | Location.dummy_loc |
||

204 | (Expr_const |
||

205 | (Const_int |
||

206 | (Big_int.int_of_big_int (Z3.Arithmetic.Integer.get_big_int ze)))) |
||

207 | else if Z3.Expr.is_const ze then |
||

208 | match Z3.Expr.to_string ze with |
||

209 | | "true" -> mkexpr Location.dummy_loc |
||

210 | (Expr_const (Const_tag (tag_true))) |
||

211 | | "false" -> |
||

212 | mkexpr Location.dummy_loc |
||

213 | (Expr_const (Const_tag (tag_false))) |
||

214 | | _ -> assert false |
||

215 | else |
||

216 | ( |
||

217 | Format.eprintf "Const err: %s %b@." (Z3.Expr.to_string ze) (Z3.Expr.is_const ze); |
||

218 | assert false (* a numeral but no int nor real *) |
||

219 | ) |
||

220 | in |
||

221 | None, Some e |
||

222 | else |
||

223 | match op with |
||

224 | | "not" | "=" | "-" | "*" | "/" |
||

225 | | ">=" | "<=" | ">" | "<" |
||

226 | -> |
||

227 | let args = List.map (fun ze -> Utils.desome (snd (ze2e ze))) zel in |
||

228 | None, Some (mkpredef_call Location.dummy_loc op args) |
||

229 | | "+" -> ( (* Special treatment of + for 2+ args *) |
||

230 | let args = List.map (fun ze -> Utils.desome (snd (ze2e ze))) zel in |
||

231 | let e = match args with |
||

232 | [] -> assert false |
||

233 | | [hd] -> hd |
||

234 | | e1::e2::tl -> |
||

235 | let first_binary_and = mkpredef_call Location.dummy_loc op [e1;e2] in |
||

236 | if tl = [] then first_binary_and else |
||

237 | List.fold_left (fun e e_new -> |
||

238 | mkpredef_call Location.dummy_loc op [e;e_new] |
||

239 | ) first_binary_and tl |
||

240 | |||

241 | in |
||

242 | None, Some e |
||

243 | ) |
||

244 | 47851ec2 | ploc | | "and" | "or" -> ( |

245 | 8c934ccd | ploc | (* Special case since it can contain is_init pred *) |

246 | let args = List.map (fun ze -> ze2e ze) zel in |
||

247 | 47851ec2 | ploc | let op = if op = "and" then "&&" else if op = "or" then "||" else assert false in |

248 | 8c934ccd | ploc | match args with |

249 | | [] -> assert false |
||

250 | | [hd] -> hd |
||

251 | | hd::tl -> |
||

252 | List.fold_left |
||

253 | (fun (is_init_opt1, expr_opt1) (is_init_opt2, expr_opt2) -> |
||

254 | (match is_init_opt1, is_init_opt2 with |
||

255 | None, x | x, None -> x |
||

256 | | Some _, Some _ -> assert false), |
||

257 | (match expr_opt1, expr_opt2 with |
||

258 | | None, x | x, None -> x |
||

259 | | Some e1, Some e2 -> |
||

260 | 47851ec2 | ploc | Some (mkpredef_call Location.dummy_loc op [e1; e2]) |

261 | 8c934ccd | ploc | )) |

262 | hd tl |
||

263 | ) |
||

264 | | op -> |
||

265 | let args = List.map (fun ze -> (snd (ze2e ze))) zel in |
||

266 | 47851ec2 | ploc | Format.eprintf "deal with op %s (nb args: %i). Expr is %s@." op (List.length args) (Z3.Expr.to_string ze); assert false |

267 | 8c934ccd | ploc | ) |

268 | in |
||

269 | (fun e -> e2ze e), (fun ze -> ze2e ze) |
||

270 | |||

271 | 3b7f916b | ploc | |

272 | 47851ec2 | ploc | let zexpr_to_guard_list ze = |

273 | let init_opt, expr_opt = zexpr_to_expr ze in |
||

274 | (match init_opt with |
||

275 | | None -> [] |
||

276 | |Some b -> [IsInit, b] |
||

277 | ) @ (match expr_opt with |
||

278 | | None -> [] |
||

279 | | Some e -> [Expr e, true] |
||

280 | ) |
||

281 | 3b7f916b | ploc | |

282 | |||

283 | 47851ec2 | ploc | let simplify_neg_guard l = |

284 | List.map (fun (g,posneg) -> |
||

285 | match g with |
||

286 | | IsInit -> g, posneg |
||

287 | | Expr g -> |
||

288 | if posneg then |
||

289 | Expr (Corelang.push_negations g), |
||

290 | true |
||

291 | else |
||

292 | (* Pushing the negation in the expression *) |
||

293 | Expr(Corelang.push_negations ~neg:true g), |
||

294 | true |
||

295 | ) l |
||

296 | |||

297 | (* TODO: |
||

298 | individuellement demander si g1 => g2. Si c'est le cas, on peut ne garder que g1 dans la liste |
||

299 | *) |
||

300 | 8c934ccd | ploc | (*****************************************************************) |

301 | (* Checking sat(isfiability) of an expression and simplifying it *) |
||

302 | (* All (free) variables have to be declared in the Z3 context *) |
||

303 | (*****************************************************************) |
||

304 | 3b7f916b | ploc | (* |

305 | 47851ec2 | ploc | let goal_simplify zl = |

306 | let goal = Z3.Goal.mk_goal !ctx false false false in |
||

307 | Z3.Goal.add goal zl; |
||

308 | let goal' = Z3.Goal.simplify goal None in |
||

309 | (* Format.eprintf "Goal before: %s@.Goal after : %s@.Sat? %s@." |
||

310 | * (Z3.Goal.to_string goal) |
||

311 | * (Z3.Goal.to_string goal') |
||

312 | * (Z3.Solver.string_of_status status_res) |
||

313 | * ; *) |
||

314 | let ze = Z3.Goal.as_expr goal' in |
||

315 | (* Format.eprintf "as an expr: %s@." (Z3.Expr.to_string ze); *) |
||

316 | 3b7f916b | ploc | zexpr_to_guard_list ze |

317 | *) |
||

318 | |||

319 | let implies = |
||

320 | let ze_implies_hash : ((Utils.tag * Utils.tag), bool) Hashtbl.t = Hashtbl.create 13 in |
||

321 | fun ze1 ze2 -> |
||

322 | let ze1_uid = get_zid ze1 in |
||

323 | let ze2_uid = get_zid ze2 in |
||

324 | if Hashtbl.mem ze_implies_hash (ze1_uid, ze2_uid) then |
||

325 | Hashtbl.find ze_implies_hash (ze1_uid, ze2_uid) |
||

326 | else |
||

327 | begin |
||

328 | 81229f63 | ploc | if !debug then ( |

329 | Format.eprintf "Checking implication: %s => %s? " |
||

330 | (Z3.Expr.to_string ze1) (Z3.Expr.to_string ze2) |
||

331 | ); |
||

332 | 3b7f916b | ploc | let solver = Z3.Solver.mk_simple_solver !ctx in |

333 | let tgt = Z3.Boolean.mk_not !ctx (Z3.Boolean.mk_implies !ctx ze1 ze2) in |
||

334 | let res = |
||

335 | try |
||

336 | let status_res = Z3.Solver.check solver [tgt] in |
||

337 | match status_res with |
||

338 | 81229f63 | ploc | | Z3.Solver.UNSATISFIABLE -> if !debug then Format.eprintf "Valid!@."; |

339 | 3b7f916b | ploc | true |

340 | 81229f63 | ploc | | _ -> if !debug then Format.eprintf "not proved valid@."; |

341 | 3b7f916b | ploc | false |

342 | with Zustre_common.UnknownFunction(id, msg) -> ( |
||

343 | report ~level:1 msg; |
||

344 | false |
||

345 | ) |
||

346 | in |
||

347 | Hashtbl.add ze_implies_hash (ze1_uid,ze2_uid) res ; |
||

348 | res |
||

349 | end |
||

350 | 47851ec2 | ploc | |

351 | let rec simplify zl = |
||

352 | match zl with |
||

353 | | [] | [_] -> zl |
||

354 | | hd::tl -> ( |
||

355 | 3b7f916b | ploc | (* Forall e in tl, checking whether hd => e or e => hd, to keep hd |

356 | 47851ec2 | ploc | in the first case and e in the second one *) |

357 | let tl = simplify tl in |
||

358 | let keep_hd, tl = |
||

359 | List.fold_left (fun (keep_hd, accu) e -> |
||

360 | if implies hd e then |
||

361 | true, accu (* throwing away e *) |
||

362 | else if implies e hd then |
||

363 | false, e::accu (* throwing away hd *) |
||

364 | else |
||

365 | keep_hd, e::accu (* keeping both *) |
||

366 | ) (true,[]) tl |
||

367 | in |
||

368 | (* Format.eprintf "keep_hd?%b hd=%s, tl=[%a]@." |
||

369 | * keep_hd |
||

370 | * (Z3.Expr.to_string hd) |
||

371 | * (Utils.fprintf_list ~sep:"; " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) tl |
||

372 | * ; *) |
||

373 | if keep_hd then |
||

374 | hd::tl |
||

375 | else |
||

376 | tl |
||

377 | ) |
||

378 | |||

379 | let check_sat ?(just_check=false) (l:guard) : bool * guard = |
||

380 | (* Syntactic simplification *) |
||

381 | 3b7f916b | ploc | if false then |

382 | Format.eprintf "Before simplify: %a@." pp_guard_list l; |
||

383 | 47851ec2 | ploc | let l = simplify_neg_guard l in |

384 | 3b7f916b | ploc | if false then ( |

385 | Format.eprintf "After simplify: %a@." pp_guard_list l; |
||

386 | Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " pp_guard_list l; |
||

387 | ); |
||

388 | 47851ec2 | ploc | let solver = Z3.Solver.mk_simple_solver !ctx in |

389 | try ( |
||

390 | 8c934ccd | ploc | let zl = |

391 | List.map (fun (e, posneg) -> |
||

392 | let ze = |
||

393 | match e with |
||

394 | | IsInit -> is_init_z3e |
||

395 | | Expr e -> expr_to_z3_expr e |
||

396 | in |
||

397 | if posneg then |
||

398 | ze |
||

399 | else |
||

400 | neg_ze ze |
||

401 | ) l |
||

402 | in |
||

403 | 3b7f916b | ploc | if false then Format.eprintf "Z3 exprs1: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; |

404 | 47851ec2 | ploc | let zl = simplify zl in |

405 | 3b7f916b | ploc | if false then Format.eprintf "Z3 exprs2: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; |

406 | 8c934ccd | ploc | let status_res = Z3.Solver.check solver zl in |

407 | 3b7f916b | ploc | if false then Format.eprintf "Z3 status: %s@ @]@. " (Z3.Solver.string_of_status status_res); |

408 | 47851ec2 | ploc | match status_res with |

409 | | Z3.Solver.UNSATISFIABLE -> false, [] |
||

410 | | _ -> ( |
||

411 | if false && just_check then |
||

412 | true, l |
||

413 | else |
||

414 | 3b7f916b | ploc | (* TODO: may be reactivate but it may create new expressions *) |

415 | (* let l = goal_simplify zl in *) |
||

416 | let l = List.fold_left |
||

417 | (fun accu ze -> accu @ (zexpr_to_guard_list ze)) |
||

418 | [] |
||

419 | zl |
||

420 | in |
||

421 | 47851ec2 | ploc | (* Format.eprintf "@.@[<v 2>Check_Sat:@ before: %a@ after: |

422 | %a@. Goal precise? %b/%b@]@.@. " * pp_guard_list l |
||

423 | pp_guard_list l' * (Z3.Goal.is_precise goal) * |
||

424 | (Z3.Goal.is_precise goal'); *) |
||

425 | 8c934ccd | ploc | |

426 | 47851ec2 | ploc | |

427 | true, l |
||

428 | |||

429 | |||

430 | 8c934ccd | ploc | ) |

431 | 47851ec2 | ploc | |

432 | 8c934ccd | ploc | ) |

433 | 47851ec2 | ploc | with Zustre_common.UnknownFunction(id, msg) -> ( |

434 | report ~level:1 msg; |
||

435 | true, l (* keeping everything. *) |
||

436 | ) |
||

437 | |||

438 | |||

439 | 8c934ccd | ploc | |

440 | |||

441 | (**************************************************************) |
||

442 | |||

443 | |||

444 | let clean_sys sys = |
||

445 | List.fold_left (fun accu (guards, updates) -> |
||

446 | 47851ec2 | ploc | let sat, guards' = check_sat (List.map (fun (g, pn) -> Expr g, pn) guards) in |

447 | 8c934ccd | ploc | (*Format.eprintf "Guard: %a@.Guard cleaned: %a@.Sat? %b@." |

448 | (fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr)) guards |
||

449 | (fprintf_list ~sep:"@ " (pp_guard_expr Printers.pp_expr)) guards' |
||

450 | sat |
||

451 | |||

452 | ;*) |
||

453 | if sat then |
||

454 | 47851ec2 | ploc | (List.map (fun (e, b) -> (deelem e, b)) guards', updates)::accu |

455 | 8c934ccd | ploc | else |

456 | accu |
||

457 | ) |
||

458 | [] sys |
||

459 | 3b7f916b | ploc | |

460 | (* Most costly function: has the be efficiently implemented. All |
||

461 | registered guards are initially produced by the call to |
||

462 | combine_guards. We csan normalize the guards to ease the |
||

463 | comparisons. |
||

464 | |||

465 | We assume that gl1 and gl2 are already both satisfiable and in a |
||

466 | kind of reduced form. Let lshort and llong be the short and long |
||

467 | list of gl1, gl2. We check whether each element elong of llong is |
||

468 | satisfiable with lshort. If no, stop. If yes, we search to reduce |
||

469 | the list. If elong => eshort_i, we can remove eshort_i from |
||

470 | lshort. we can continue with this lshort shortened, lshort'; it is |
||

471 | not necessary to add yet elong in lshort' since we already know |
||

472 | rthat elong is somehow reduced with respect to other elements of |
||

473 | llong. If eshort_i => elong, then we keep ehosrt_i in lshort and do |
||

474 | not store elong. |
||

475 | |||

476 | After iterating through llong, we have a shortened version of |
||

477 | lshort + some elements of llong that have to be remembered. We add |
||

478 | them to this new consolidated list. |
||

479 | |||

480 | *) |
||

481 | |||

482 | (* combine_guards ~fresh:Some(e,b) gl1 gl2 returns ok, gl with ok=true |
||

483 | when (e=b) ang gl1 and gl2 is satisfiable and gl is a consilidated |
||

484 | version of it. *) |
||

485 | 0d79d0f3 | ploc | let combine_guards ?(fresh=None) gl1 gl2 = |

486 | (* Filtering out trivial cases. More semantics ones would have to be |
||

487 | addressed later *) |
||

488 | 3b7f916b | ploc | let check_sat e = (* temp function before we clean the original one *) |

489 | let ok, _ = check_sat e in |
||

490 | ok |
||

491 | 0d79d0f3 | ploc | in |

492 | 3b7f916b | ploc | let implies (e1,pn1) (e2,pn2) = |

493 | let e2z e pn = |
||

494 | match e with |
||

495 | | IsInit -> if pn then is_init_z3e else neg_ze is_init_z3e |
||

496 | | Expr e -> expr_to_z3_expr (if pn then e else (Corelang.push_negations ~neg:true e)) |
||

497 | in |
||

498 | implies (e2z e1 pn1) (e2z e2 pn2) |
||

499 | in |
||

500 | let lshort, llong = |
||

501 | if List.length gl1 > List.length gl2 then gl2, gl1 else gl1, gl2 |
||

502 | in |
||

503 | let merge long short = |
||

504 | let short, long_sel, ok = |
||

505 | List.fold_left (fun (short,long_sel, ok) long_e -> |
||

506 | if not ok then |
||

507 | [],[], false (* Propagating unsat case *) |
||

508 | else if check_sat (long_e::short) then |
||

509 | let short, keep_long_e = |
||

510 | List.fold_left (fun (accu_short, keep_long_e) eshort_i -> |
||

511 | if not keep_long_e then (* shorten the algo *) |
||

512 | eshort_i :: accu_short, false |
||

513 | else (* keep_long_e = true in the following *) |
||

514 | if implies eshort_i long_e then |
||

515 | (* First case is trying to remove long_e! |
||

516 | |||

517 | Since short is already normalized, we can remove |
||

518 | long_e. If later long_e is stronger than another |
||

519 | element of short, then necessarily eshort_i => |
||

520 | long_e -> |
||

521 | that_other_element_of_short. Contradiction. *) |
||

522 | eshort_i::accu_short, false |
||

523 | else if implies long_e eshort_i then |
||

524 | (* removing eshort_i, keeping long_e. *) |
||

525 | accu_short, true |
||

526 | else (* Not comparable, keeping both *) |
||

527 | eshort_i::accu_short, true |
||

528 | ) |
||

529 | ([],true) (* Initially we assume that we will keep long_e *) |
||

530 | short |
||

531 | in |
||

532 | if keep_long_e then |
||

533 | short, long_e::long_sel, true |
||

534 | else |
||

535 | short, long_sel, true |
||

536 | 0d79d0f3 | ploc | else |

537 | 3b7f916b | ploc | [],[],false |

538 | ) (short, [], true) long |
||

539 | in |
||

540 | ok, long_sel@short |
||

541 | 0d79d0f3 | ploc | in |

542 | 3b7f916b | ploc | let ok, l = match fresh with |

543 | | None -> true, [] |
||

544 | | Some g -> merge [g] [] |
||

545 | in |
||

546 | if not ok then |
||

547 | 7aaacbc9 | ploc | false, [] |

548 | 3b7f916b | ploc | else |

549 | let ok, lshort = merge lshort l in |
||

550 | if not ok then |
||

551 | false, [] |
||

552 | else |
||

553 | merge llong lshort |
||

554 | |||

555 | 0d79d0f3 | ploc | |

556 | (* Encode "If gel1=posneg then gel2": |
||

557 | - Compute the combination of guarded exprs in gel1 and gel2: |
||

558 | - Each guarded_expr in gel1 is transformed as a guard: the |
||

559 | expression is associated to posneg. |
||

560 | - Existing guards in gel2 are concatenated to that list of guards |
||

561 | - We keep expr in the ge of gel2 as the legitimate expression |
||

562 | *) |
||

563 | let concatenate_ge gel1 posneg gel2 = |
||

564 | 3b7f916b | ploc | let l, all_invalid = |

565 | List.fold_left ( |
||

566 | fun (accu, all_invalid) (g2,e2) -> |
||

567 | List.fold_left ( |
||

568 | fun (accu, all_invalid) (g1,e1) -> |
||

569 | (* Format.eprintf "@[<v 2>Combining guards: (%a=%b) AND [%a] AND [%a]@ " |
||

570 | * pp_elem e1 |
||

571 | * posneg |
||

572 | * pp_guard_list g1 |
||

573 | * pp_guard_list g2; *) |
||

574 | |||

575 | let ok, gl = combine_guards ~fresh:(Some(e1,posneg)) g1 g2 in |
||

576 | (* Format.eprintf "@]@ Result is [%a]@ " |
||

577 | * pp_guard_list gl; *) |
||

578 | |||

579 | if ok then |
||

580 | (gl, e2)::accu, false |
||

581 | else ( |
||

582 | accu, all_invalid |
||

583 | ) |
||

584 | ) (accu, all_invalid) gel1 |
||

585 | ) ([], true) gel2 |
||

586 | in |
||

587 | not all_invalid, l |
||

588 | |||

589 | (* Rewrite the expression expr, replacing any occurence of a variable |
||

590 | by its definition. |
||

591 | *) |
||

592 | 0d79d0f3 | ploc | let rec rewrite defs expr : guarded_expr list = |

593 | let rewrite = rewrite defs in |
||

594 | 7aaacbc9 | ploc | let res = |

595 | match expr.expr_desc with |
||

596 | | Expr_appl (id, args, None) -> |
||

597 | let args = rewrite args in |
||

598 | List.map (fun (guards, e) -> |
||

599 | 0d79d0f3 | ploc | guards, |

600 | 81229f63 | ploc | Expr (Corelang.mkexpr expr.expr_loc (Expr_appl(id, deelem e, None))) |

601 | 7aaacbc9 | ploc | ) args |

602 | | Expr_const _ -> [[], Expr expr] |
||

603 | | Expr_ident id -> |
||

604 | if Hashtbl.mem defs id then |
||

605 | Hashtbl.find defs id |
||

606 | else |
||

607 | (* id should be an input *) |
||

608 | [[], Expr expr] |
||

609 | | Expr_ite (g, e1, e2) -> |
||

610 | let g = rewrite g and |
||

611 | e1 = rewrite e1 and |
||

612 | e2 = rewrite e2 in |
||

613 | 3b7f916b | ploc | let ok_then, g_then = concatenate_ge g true e1 in |

614 | let ok_else, g_else = concatenate_ge g false e2 in |
||

615 | (if ok_then then g_then else [])@ |
||

616 | (if ok_else then g_else else []) |
||

617 | 7aaacbc9 | ploc | | Expr_merge (g, branches) -> |

618 | assert false (* TODO: deal with merges *) |
||

619 | |||

620 | | Expr_when (e, _, _) -> rewrite e |
||

621 | | Expr_arrow _ -> [[], IsInit] (* At this point the only arrow should be true -> false *) |
||

622 | | Expr_tuple el -> |
||

623 | (* Each expr is associated to its flatten guarded expr list *) |
||

624 | let gell = List.map rewrite el in |
||

625 | (* Computing all combinations: we obtain a list of guarded tuple *) |
||

626 | let rec aux gell : (guard * expr list) list = |
||

627 | match gell with |
||

628 | | [] -> assert false (* Not happening *) |
||

629 | | [gel] -> List.map (fun (g,e) -> g, [deelem e]) gel |
||

630 | | gel::getl -> |
||

631 | let getl = aux getl in |
||

632 | List.fold_left ( |
||

633 | fun accu (g,e) -> |
||

634 | List.fold_left ( |
||

635 | 0d79d0f3 | ploc | fun accu (gl, minituple) -> |

636 | let is_compat, guard_comb = combine_guards g gl in |
||

637 | if is_compat then |
||

638 | let new_gt : guard * expr list = (guard_comb, (deelem e)::minituple) in |
||

639 | new_gt::accu |
||

640 | else |
||

641 | accu |
||

642 | 7aaacbc9 | ploc | |

643 | 0d79d0f3 | ploc | ) accu getl |

644 | 7aaacbc9 | ploc | ) [] gel |

645 | in |
||

646 | let gtuples = aux gell in |
||

647 | (* Rebuilding the valid type: guarded expr list (with tuple exprs) *) |
||

648 | 81229f63 | ploc | List.map |

649 | (fun (g,tuple) -> g, Expr (Corelang.mkexpr expr.expr_loc (Expr_tuple tuple))) |
||

650 | gtuples |
||

651 | 7aaacbc9 | ploc | | Expr_fby _ |

652 | | Expr_appl _ |
||

653 | (* Should be removed by mormalization and inlining *) |
||

654 | -> Format.eprintf "Pb expr: %a@.@?" Printers.pp_expr expr; assert false |
||

655 | | Expr_array _ | Expr_access _ | Expr_power _ |
||

656 | (* Arrays not handled here yet *) |
||

657 | -> assert false |
||

658 | | Expr_pre _ -> (* Not rewriting mem assign *) |
||

659 | assert false |
||

660 | in |
||

661 | (* Format.eprintf "Rewriting %a as [@[<v 0>%a@]]@ " |
||

662 | * Printers.pp_expr expr |
||

663 | * (Utils.fprintf_list ~sep:"@ " |
||

664 | * pp_guard_expr) res; *) |
||

665 | res |
||

666 | 0d79d0f3 | ploc | and add_def defs vid expr = |

667 | 7aaacbc9 | ploc | let vid_defs = rewrite defs expr in |

668 | (* Format.eprintf "Add_def: %s = %a@. -> @[<v 0>%a@]@." |
||

669 | 47851ec2 | ploc | * vid |

670 | * Printers.pp_expr expr |
||

671 | * ( |
||

672 | * (Utils.fprintf_list ~sep:"@ " |
||

673 | * pp_guard_expr)) vid_defs; *) |
||

674 | 7aaacbc9 | ploc | Hashtbl.add defs vid vid_defs |

675 | 0d79d0f3 | ploc | |

676 | (* Takes a list of guarded exprs (ge) and a guard |
||

677 | returns the same list of ge splited into the ones where the guard is true and the ones where it is false. In both lists the associated ge do not mention that guard anymore. |
||

678 | |||

679 | When a given ge doesn't mention positively or negatively such guards, it is duplicated in both lists *) |
||

680 | let split_mdefs elem (mdefs: guarded_expr list) = |
||

681 | List.fold_left ( |
||

682 | fun (selected, left_out) |
||

683 | ((guards, expr) as ge) -> |
||

684 | (* select the element of guards that match the argument elem *) |
||

685 | let sel, others_guards = List.partition (select_elem elem) guards in |
||

686 | match sel with |
||

687 | (* we extract the element from the list and add it to the |
||

688 | appropriate list *) |
||

689 | | [_, sel_status] -> |
||

690 | if sel_status then |
||

691 | (others_guards,expr)::selected, left_out |
||

692 | else selected, (others_guards,expr)::left_out |
||

693 | | [] -> (* no such guard exists, we have to duplicate the |
||

694 | guard_expr in both lists *) |
||

695 | ge::selected, ge::left_out |
||

696 | | _ -> ( |
||

697 | Format.eprintf "@.Spliting list on elem %a.@.List:%a@." |
||

698 | pp_elem elem |
||

699 | pp_mdefs mdefs; |
||

700 | assert false (* more then one element selected. Should |
||

701 | not happen , or trival dead code like if |
||

702 | x then if not x then dead code *) |
||

703 | ) |
||

704 | ) ([],[]) mdefs |
||

705 | |||

706 | let split_mem_defs |
||

707 | (elem: element) |
||

708 | 8c934ccd | ploc | (mem_defs: (ident * guarded_expr list) list) |

709 | : |
||

710 | 0d79d0f3 | ploc | ((ident * mdef_t) list) * ((ident * mdef_t) list) |

711 | 8c934ccd | ploc | |

712 | 0d79d0f3 | ploc | = |

713 | List.fold_right (fun (m,mdefs) |
||

714 | (accu_pos, accu_neg) -> |
||

715 | let pos, neg = |
||

716 | 8c934ccd | ploc | split_mdefs elem mdefs |

717 | 0d79d0f3 | ploc | in |

718 | (m, pos)::accu_pos, |
||

719 | (m, neg)::accu_neg |
||

720 | ) mem_defs ([],[]) |
||

721 | |||

722 | |||

723 | (* Split a list of mem_defs into init and step lists of guarded |
||

724 | expressions per memory. *) |
||

725 | let split_init mem_defs = |
||

726 | 8c934ccd | ploc | split_mem_defs IsInit mem_defs |

727 | 0d79d0f3 | ploc | |

728 | 3b7f916b | ploc | (* Previous version of the function: way too costly |

729 | let pick_guard mem_defs : expr option = |
||

730 | 0d79d0f3 | ploc | let gel = List.flatten (List.map snd mem_defs) in |

731 | let gl = List.flatten (List.map fst gel) in |
||

732 | let all_guards = |
||

733 | List.map ( |
||

734 | (* selecting guards and getting rid of boolean *) |
||

735 | fun (e,b) -> |
||

736 | match e with |
||

737 | | Expr e -> e |
||

738 | | _ -> assert false |
||

739 | (* should have been filtered out |
||

740 | yet *) |
||

741 | ) gl |
||

742 | in |
||

743 | (* TODO , one could sort by occurence and provided the most common |
||

744 | one *) |
||

745 | 8c934ccd | ploc | try |

746 | Some (List.hd all_guards) |
||

747 | with _ -> None |
||

748 | 3b7f916b | ploc | *) |

749 | |||

750 | (* Returning the first non empty guard expression *) |
||

751 | let rec pick_guard mem_defs : expr option = |
||

752 | match mem_defs with |
||

753 | | [] -> None |
||

754 | | (_, gel)::tl -> ( |
||

755 | let found = |
||

756 | List.fold_left (fun found (g,_) -> |
||

757 | if found = None then |
||

758 | match g with |
||

759 | | [] -> None |
||

760 | | (Expr e, _)::_ -> Some e |
||

761 | | (IsInit, _)::_ -> assert false (* should be removed already *) |
||

762 | else |
||

763 | found |
||

764 | ) None gel |
||

765 | in |
||

766 | if found = None then pick_guard tl else found |
||

767 | ) |
||

768 | |||

769 | |||

770 | 0d79d0f3 | ploc | (* Transform a list of variable * guarded exprs into a list of guarded pairs (variable, expressions) |

771 | *) |
||

772 | let rec build_switch_sys |
||

773 | (mem_defs : (Utils.ident * guarded_expr list) list ) |
||

774 | prefix |
||

775 | : |
||

776 | ((expr * bool) list * (ident * expr) list ) list = |
||

777 | d75eb6f1 | ploc | Format.eprintf "Build_switch with %a@." |

778 | (Utils.fprintf_list ~sep:",@ " |
||

779 | (fun fmt (id, gel) -> Format.fprintf fmt "%s -> [@[<v 0>%a@ ]@]" |
||

780 | id |
||

781 | pp_mdefs gel)) |
||

782 | mem_defs; |
||

783 | 0d79d0f3 | ploc | (* if all mem_defs have empty guards, we are done, return prefix, |

784 | mem_defs expr. |
||

785 | |||

786 | otherwise pick a guard in one of the mem, eg (g, b) then for each |
||

787 | 47851ec2 | ploc | other mem, one need to select the same guard g with the same |

788 | status b, *) |
||

789 | 0d79d0f3 | ploc | if List.for_all (fun (m,mdefs) -> |

790 | (* All defs are unguarded *) |
||

791 | match mdefs with |
||

792 | | [[], _] -> true |
||

793 | 8c934ccd | ploc | | _ -> false |

794 | ) mem_defs |
||

795 | 0d79d0f3 | ploc | then |

796 | [prefix , |
||

797 | List.map (fun (m,gel) -> |
||

798 | match gel with |
||

799 | | [_,e] -> |
||

800 | let e = |
||

801 | match e with |
||

802 | | Expr e -> e |
||

803 | | _ -> assert false (* No IsInit expression *) |
||

804 | in |
||

805 | m,e |
||

806 | | _ -> assert false |
||

807 | ) mem_defs] |
||

808 | else |
||

809 | (* Picking a guard *) |
||

810 | 8c934ccd | ploc | let elem_opt : expr option = pick_guard mem_defs in |

811 | match elem_opt with |
||

812 | None -> [] |
||

813 | | Some elem -> ( |
||

814 | let pos, neg = |
||

815 | split_mem_defs |
||

816 | (Expr elem) |
||

817 | mem_defs |
||

818 | in |
||

819 | (* Special cases to avoid useless computations: true, false conditions *) |
||

820 | match elem.expr_desc with |
||

821 | | Expr_ident "true" -> build_switch_sys pos prefix |
||

822 | | Expr_const (Const_tag tag) when tag = Corelang.tag_true |
||

823 | -> build_switch_sys pos prefix |
||

824 | | Expr_ident "false" -> build_switch_sys neg prefix |
||

825 | | Expr_const (Const_tag tag) when tag = Corelang.tag_false |
||

826 | -> build_switch_sys neg prefix |
||

827 | | _ -> (* Regular case *) |
||

828 | (* let _ = ( |
||

829 | * Format.eprintf "Expr is %a@." Printers.pp_expr elem; |
||

830 | * match elem.expr_desc with |
||

831 | * | Expr_const _ -> Format.eprintf "a const@." |
||

832 | * |
||

833 | * | Expr_ident _ -> Format.eprintf "an ident@." |
||

834 | * | _ -> Format.eprintf "something else@." |
||

835 | * ) |
||

836 | * in *) |
||

837 | 47851ec2 | ploc | let clean l = |

838 | let l = List.map (fun (e,b) -> (Expr e), b) l in |
||

839 | let ok, l = check_sat l in |
||

840 | let l = List.map (fun (e,b) -> deelem e, b) l in |
||

841 | ok, l |
||

842 | in |
||

843 | let pos_prefix = (elem, true)::prefix in |
||

844 | let neg_prefix = (elem, false)::prefix in |
||

845 | 3b7f916b | ploc | let ok_pos, pos_prefix = clean pos_prefix in |

846 | 47851ec2 | ploc | let ok_neg, neg_prefix = clean neg_prefix in |

847 | (if ok_pos then build_switch_sys pos pos_prefix else []) |
||

848 | 8c934ccd | ploc | @ |

849 | 47851ec2 | ploc | (if ok_neg then build_switch_sys neg neg_prefix else []) |

850 | 8c934ccd | ploc | ) |

851 | 0d79d0f3 | ploc | |

852 | |||

853 | |||

854 | (* Take a normalized node and extract a list of switches: (cond, |
||

855 | update) meaning "if cond then update" where update shall define all |
||

856 | node memories. Everything as to be expressed over inputs or memories, intermediate variables are removed through inlining *) |
||

857 | 8c934ccd | ploc | let node_as_switched_sys consts (mems:var_decl list) nd = |

858 | 0d79d0f3 | ploc | (* rescheduling node: has been scheduled already, no need to protect |

859 | the call to schedule_node *) |
||

860 | let nd_report = Scheduling.schedule_node nd in |
||

861 | let schedule = nd_report.Scheduling_type.schedule in |
||

862 | 5de4dde4 | ploc | let eqs, auts = Corelang.get_node_eqs nd in |

863 | assert (auts = []); (* Automata should be expanded by now *) |
||

864 | let sorted_eqs = Scheduling.sort_equations_from_schedule eqs schedule in |
||

865 | 0d79d0f3 | ploc | let defs : (ident, guarded_expr list) Hashtbl.t = Hashtbl.create 13 in |

866 | let add_def = add_def defs in |
||

867 | 8c934ccd | ploc | |

868 | let vars = Corelang.get_node_vars nd in |
||

869 | (* Registering all locals variables as Z3 predicates. Will be use to |
||

870 | simplify the expansion *) |
||

871 | let _ = |
||

872 | List.iter (fun v -> |
||

873 | let fdecl = Z3.FuncDecl.mk_func_decl_s |
||

874 | !ctx |
||

875 | v.var_id |
||

876 | [] |
||

877 | (Zustre_common.type_to_sort v.var_type) |
||

878 | in |
||

879 | ignore (Zustre_common.register_fdecl v.var_id fdecl) |
||

880 | ) vars |
||

881 | in |
||

882 | let _ = |
||

883 | List.iter (fun c -> Hashtbl.add const_defs c.const_id c.const_value) consts |
||

884 | in |
||

885 | 7aaacbc9 | ploc | |

886 | 8c934ccd | ploc | |

887 | (* Registering node equations: identifying mem definitions and |
||

888 | 3b7f916b | ploc | storing others in the "defs" hashtbl. |

889 | |||

890 | Each assign is stored in a hash tbl as list of guarded |
||

891 | expressions. The memory definition is also "rewritten" as such a |
||

892 | list of guarded assigns. *) |
||

893 | d75eb6f1 | ploc | let mem_defs, output_defs = |

894 | List.fold_left (fun (accu_mems, accu_outputs) eq -> |
||

895 | 0d79d0f3 | ploc | match eq.eq_lhs with |

896 | | [vid] -> |
||

897 | d75eb6f1 | ploc | (* Only focus on memory definitions *) |

898 | if List.exists (fun v -> v.var_id = vid) mems then |
||

899 | 0d79d0f3 | ploc | ( |

900 | match eq.eq_rhs.expr_desc with |
||

901 | | Expr_pre def_m -> |
||

902 | 8c934ccd | ploc | report ~level:3 (fun fmt -> |

903 | Format.fprintf fmt "Preparing mem %s@." vid); |
||

904 | d75eb6f1 | ploc | (vid, rewrite defs def_m)::accu_mems, accu_outputs |

905 | 0d79d0f3 | ploc | | _ -> assert false |

906 | d75eb6f1 | ploc | ) |

907 | else if List.exists (fun v -> v.var_id = vid) nd.node_outputs then ( |
||

908 | report ~level:3 (fun fmt -> |
||

909 | Format.fprintf fmt "Output variable %s@." vid); |
||

910 | add_def vid eq.eq_rhs; |
||

911 | accu_mems, (vid, rewrite defs eq.eq_rhs)::accu_outputs |
||

912 | |||

913 | ) |
||

914 | else |
||

915 | ( |
||

916 | report ~level:3 (fun fmt -> |
||

917 | Format.fprintf fmt "Registering variable %s@." vid); |
||

918 | add_def vid eq.eq_rhs; |
||

919 | accu_mems, accu_outputs |
||

920 | ) |
||

921 | 0d79d0f3 | ploc | | _ -> assert false (* should have been removed by normalization *) |

922 | d75eb6f1 | ploc | ) ([], []) sorted_eqs |

923 | 0d79d0f3 | ploc | in |

924 | 8c934ccd | ploc | |

925 | |||

926 | d5ec9f63 | ploc | report ~level:2 (fun fmt -> Format.fprintf fmt "Printing out (guarded) memories definitions (may takes time)@."); |

927 | 0d79d0f3 | ploc | (* Printing memories definitions *) |

928 | report ~level:3 |
||

929 | (fun fmt -> |
||

930 | Format.fprintf fmt |
||

931 | d5ec9f63 | ploc | "@[<v 0>%a@]@ " |

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

933 | 0d79d0f3 | ploc | (fun fmt (m,mdefs) -> |

934 | Format.fprintf fmt |
||

935 | d5ec9f63 | ploc | "%s -> [@[<v 0>%a@] ]@ " |

936 | 0d79d0f3 | ploc | m |

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

938 | pp_guard_expr) mdefs |
||

939 | )) |
||

940 | mem_defs); |
||

941 | 47851ec2 | ploc | (* Format.eprintf "Split init@."; *) |

942 | 0d79d0f3 | ploc | let init_defs, update_defs = |

943 | 8c934ccd | ploc | split_init mem_defs |

944 | 0d79d0f3 | ploc | in |

945 | d75eb6f1 | ploc | let init_out, update_out = |

946 | split_init output_defs |
||

947 | in |
||

948 | 0d79d0f3 | ploc | report ~level:3 |

949 | (fun fmt -> |
||

950 | Format.fprintf fmt |
||

951 | d5ec9f63 | ploc | "@[<v 0>Init:@ %a@ Step@ %a@]@ " |

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

953 | 0d79d0f3 | ploc | (fun fmt (m,mdefs) -> |

954 | Format.fprintf fmt |
||

955 | d5ec9f63 | ploc | "%s -> @[<v 0>[%a@] ]@ " |

956 | 0d79d0f3 | ploc | m |

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

958 | pp_guard_expr) mdefs |
||

959 | )) |
||

960 | init_defs |
||

961 | d5ec9f63 | ploc | (Utils.fprintf_list ~sep:"@ " |

962 | 0d79d0f3 | ploc | (fun fmt (m,mdefs) -> |

963 | Format.fprintf fmt |
||

964 | d5ec9f63 | ploc | "%s -> @[<v 0>[%a@] ]@ " |

965 | 0d79d0f3 | ploc | m |

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

967 | pp_guard_expr) mdefs |
||

968 | )) |
||

969 | update_defs); |
||

970 | 47851ec2 | ploc | (* Format.eprintf "Build init@."; *) |

971 | 8c934ccd | ploc | |

972 | 0d79d0f3 | ploc | let sw_init= |

973 | build_switch_sys init_defs [] |
||

974 | in |
||

975 | 47851ec2 | ploc | (* Format.eprintf "Build step@."; *) |

976 | 0d79d0f3 | ploc | let sw_sys = |

977 | build_switch_sys update_defs [] |
||

978 | in |
||

979 | 81229f63 | ploc | |

980 | d75eb6f1 | ploc | let init_out = |

981 | build_switch_sys init_out [] |
||

982 | in |
||

983 | let update_out = |
||

984 | build_switch_sys update_out [] |
||

985 | in |
||

986 | |||

987 | let sw_init = clean_sys sw_init in |
||

988 | let sw_sys = clean_sys sw_sys in |
||

989 | let init_out = clean_sys init_out in |
||

990 | let update_out = clean_sys update_out in |
||

991 | 81229f63 | ploc | |

992 | (* Some additional checks *) |
||

993 | let pp_gl pp_expr = |
||

994 | fprintf_list ~sep:", " (fun fmt (e,b) -> Format.fprintf fmt "%s%a" (if b then "" else "NOT ") pp_expr e) |
||

995 | in |
||

996 | let pp_gl_short = pp_gl (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag) in |
||

997 | let pp_up fmt up = List.iter (fun (id,e) -> Format.fprintf fmt "%s->%i; " id e.expr_tag) up in |
||

998 | |||

999 | if false then |
||

1000 | begin |
||

1001 | Format.eprintf "@.@.CHECKING!!!!!!!!!!!@."; |
||

1002 | Format.eprintf "Any duplicate expression in guards?@."; |
||

1003 | |||

1004 | let sw_sys = |
||

1005 | List.map (fun (gl, up) -> |
||

1006 | let gl = List.sort (fun (e,b) (e',b') -> |
||

1007 | let res = compare e.expr_tag e'.expr_tag in |
||

1008 | if res = 0 then (Format.eprintf "Same exprs?@.%a@.%a@.@." |
||

1009 | Printers.pp_expr e |
||

1010 | Printers.pp_expr e' |
||

1011 | ); |
||

1012 | res |
||

1013 | ) gl in |
||

1014 | gl, up |
||

1015 | ) sw_sys |
||

1016 | in |
||

1017 | Format.eprintf "Another check for duplicates in guard list@."; |
||

1018 | List.iter (fun (gl, _) -> |
||

1019 | let rec aux hd l = |
||

1020 | match l with |
||

1021 | [] -> () |
||

1022 | | (e,b)::tl -> let others = hd@tl in |
||

1023 | List.iter (fun (e',_) -> if Corelang.is_eq_expr e e' then |
||

1024 | (Format.eprintf "Same exprs?@.%a@.%a@.@." |
||

1025 | Printers.pp_expr e |
||

1026 | Printers.pp_expr e' |
||

1027 | )) others; |
||

1028 | aux ((e,b)::hd) tl |
||

1029 | in |
||

1030 | aux [] gl |
||

1031 | ) sw_sys; |
||

1032 | Format.eprintf "Checking duplicates in updates@."; |
||

1033 | let rec check_dup_up accu l = |
||

1034 | match l with |
||

1035 | | [] -> () |
||

1036 | | ((gl, up) as hd)::tl -> |
||

1037 | let others = accu@tl in |
||

1038 | List.iter (fun (gl',up') -> if up = up' then |
||

1039 | Format.eprintf "Same updates?@.%a@.%a@.%a@.%a@.@." |
||

1040 | |||

1041 | pp_gl_short gl |
||

1042 | pp_up up |
||

1043 | pp_gl_short gl' |
||

1044 | pp_up up' |
||

1045 | |||

1046 | ) others; |
||

1047 | |||

1048 | |||

1049 | |||

1050 | check_dup_up (hd::accu) tl |
||

1051 | |||

1052 | in |
||

1053 | check_dup_up [] sw_sys; |
||

1054 | let sw_sys = |
||

1055 | List.sort (fun (gl1, _) (gl2, _) -> |
||

1056 | let glid gl = List.map (fun (e,_) -> e.expr_tag) gl in |
||

1057 | |||

1058 | let res = compare (glid gl1) (glid gl2) in |
||

1059 | if res = 0 then Format.eprintf "Same guards?@.%a@.%a@.@." |
||

1060 | pp_gl_short gl1 pp_gl_short gl2 |
||

1061 | ; |
||

1062 | res |
||

1063 | |||

1064 | ) sw_sys |
||

1065 | |||

1066 | in |
||

1067 | () |
||

1068 | end; |
||

1069 | |||

1070 | |||

1071 | (* Iter through the elements and gather them by updates *) |
||

1072 | let module UpMap = |
||

1073 | struct |
||

1074 | include Map.Make ( |
||

1075 | struct |
||

1076 | type t = (ident * expr) list |
||

1077 | let compare l1 l2 = |
||

1078 | let proj l = List.map (fun (s,e) -> s, e.expr_tag) l in |
||

1079 | compare (proj l1) (proj l2) |
||

1080 | end) |
||

1081 | let pp = pp_up |
||

1082 | end |
||

1083 | in |
||

1084 | let module Guards = struct |
||

1085 | include Set.Make ( |
||

1086 | struct |
||

1087 | type t = (expr * bool) |
||

1088 | let compare l1 l2 = |
||

1089 | let proj (e,b) = e.expr_tag, b in |
||

1090 | compare (proj l1) (proj l2) |
||

1091 | end) |
||

1092 | let pp_short fmt s = pp_gl_short fmt (elements s) |
||

1093 | let pp_long fmt s = pp_gl Printers.pp_expr fmt (elements s) |
||

1094 | end |
||

1095 | in |
||

1096 | let process sys = |
||

1097 | (* The map will associate to each update up the pair (set, set |
||

1098 | list) where set is the share guards and set list a list of |
||

1099 | disjunctive guards. Each set represents a conjunction of |
||

1100 | expressions. *) |
||

1101 | let map = |
||

1102 | List.fold_left (fun map (gl,up) -> |
||

1103 | (* creating a new set to describe gl *) |
||

1104 | let new_set = |
||

1105 | List.fold_left |
||

1106 | (fun set g -> Guards.add g set) |
||

1107 | Guards.empty |
||

1108 | gl |
||

1109 | in |
||

1110 | (* updating the map with up -> new_set *) |
||

1111 | if UpMap.mem up map then |
||

1112 | let (shared, disj) = UpMap.find up map in |
||

1113 | let new_shared = Guards.inter shared new_set in |
||

1114 | let remaining_shared = Guards.diff shared new_shared in |
||

1115 | let remaining_new_set = Guards.diff new_set new_shared in |
||

1116 | (* Adding remaining_shared to all elements of disj *) |
||

1117 | let disj' = List.map (fun gs -> Guards.union remaining_shared gs) disj in |
||

1118 | UpMap.add up (new_shared, remaining_new_set::disj') map |
||

1119 | else |
||

1120 | UpMap.add up (new_set, []) map |
||

1121 | ) UpMap.empty sys |
||

1122 | in |
||

1123 | let rec mk_binop op l = match l with |
||

1124 | [] -> assert false |
||

1125 | | [e] -> e |
||

1126 | | hd::tl -> Corelang.mkpredef_call hd.expr_loc op [hd; mk_binop op tl] |
||

1127 | in |
||

1128 | let gl_as_expr gl = |
||

1129 | let gl = Guards.elements gl in |
||

1130 | let export (e,b) = if b then e else Corelang.push_negations ~neg:true e in |
||

1131 | match gl with |
||

1132 | [] -> [] |
||

1133 | | [e] -> [export e] |
||

1134 | | _ -> |
||

1135 | [mk_binop "&&" |
||

1136 | (List.map export gl)] |
||

1137 | in |
||

1138 | let rec clean_disj disj = |
||

1139 | match disj with |
||

1140 | | [] | [_] -> [] |
||

1141 | | _::_::_ -> ( |
||

1142 | (* First basic version: producing a DNF One can later, (1) |
||

1143 | simplify it with z3, or (2) build the compact tree with |
||

1144 | maximum shared subexpression (and simplify it with z3) *) |
||

1145 | let elems = List.fold_left (fun accu gl -> (gl_as_expr gl) @ accu) [] disj in |
||

1146 | let or_expr = mk_binop "||" elems in |
||

1147 | [or_expr] |
||

1148 | |||

1149 | |||

1150 | (* TODO disj*) |
||

1151 | (* get the item that occurs in most case *) |
||

1152 | (* List.fold_left (fun accu s -> |
||

1153 | * List.fold_left (fun accu (e,b) -> |
||

1154 | * if List.mem_assoc (e.expr_tag, b) |
||

1155 | * ) accu (Guards.elements s) |
||

1156 | * ) [] disj *) |
||

1157 | |||

1158 | ) |
||

1159 | in |
||

1160 | Format.eprintf "Map: %i elements@." (UpMap.cardinal map); |
||

1161 | UpMap.fold (fun up (common, disj) accu -> |
||

1162 | Format.eprintf |
||

1163 | "Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@." |
||

1164 | Guards.pp_short common |
||

1165 | (fprintf_list ~sep:";@ " Guards.pp_long) disj |
||

1166 | UpMap.pp up; |
||

1167 | let disj = clean_disj disj in |
||

1168 | let guard_expr = (gl_as_expr common)@disj in |
||

1169 | |||

1170 | ((match guard_expr with |
||

1171 | | [] -> None |
||

1172 | | _ -> Some (mk_binop "&&" guard_expr)), up)::accu |
||

1173 | ) map [] |
||

1174 | |||

1175 | in |
||

1176 | d75eb6f1 | ploc | process sw_init, process sw_sys, process init_out, process update_out |