|
1
|
open Zustre_data
|
|
2
|
|
|
3
|
let get_conjuncts e =
|
|
4
|
assert (Z3.Boolean.is_bool e);
|
|
5
|
if Z3.Boolean.is_and e then
|
|
6
|
Z3.Expr.get_args e
|
|
7
|
else
|
|
8
|
[e]
|
|
9
|
|
|
10
|
let build_cex decl_err =
|
|
11
|
|
|
12
|
let cex = match Z3.Fixedpoint.get_answer !fp with Some e -> e | None -> raise Not_found in
|
|
13
|
(* Original code used the function Z3.Fixedpoint.get_ground_sat_answer !fp *)
|
|
14
|
let conjuncts = List.rev (get_conjuncts cex) in
|
|
15
|
(* Predicates are renamed according to the naming scheme of LustreC*)
|
|
16
|
(* pred_dict = {}
|
|
17
|
cex_dict = {} #store the cex in order
|
|
18
|
for p in self.preds:
|
|
19
|
lus_pred = z3.substitute(p, *self.coco.z3MapVar)
|
|
20
|
lus_arg = [str(x) for x in lus_pred.children()]
|
|
21
|
pred_dict.update({str(lus_pred.decl()):lus_arg})
|
|
22
|
*)
|
|
23
|
(* Building a cex_dict, a map of maps ! node name -> (k -> value) *)
|
|
24
|
let _ = List.mapi (fun k conj ->
|
|
25
|
(* k-iterate *)
|
|
26
|
let ground_val = List.map (fun e -> Z3.Expr.to_string e) (Z3.Expr.get_args conj) in
|
|
27
|
let func_decl = Z3.Expr.get_func_decl conj in
|
|
28
|
if !debug then Format.eprintf "FuncDecl %s@." (Z3.FuncDecl.to_string func_decl);
|
|
29
|
let node_name = Z3.Symbol.get_string (Z3.FuncDecl.get_name func_decl) in
|
|
30
|
|
|
31
|
if !debug then Format.eprintf "Node %s, args %a@." node_name (Utils.fprintf_list ~sep:", " (Format.pp_print_string)) ground_val;
|
|
32
|
|
|
33
|
()
|
|
34
|
(* ground_pair = []
|
|
35
|
try:
|
|
36
|
ground_vars = pred_dict[node_name]
|
|
37
|
ground_pair = zip(ground_vars,ground_val)
|
|
38
|
if "_reset" in node_name:
|
|
39
|
# this condition is to remove the node nodename_reset added by lustrec
|
|
40
|
continue
|
|
41
|
# node = node_name.split("_reset")[0]
|
|
42
|
# cex_dict.update({node:{k:ground_pair}})
|
|
43
|
elif "_step" in node_name:
|
|
44
|
node = node_name.split("_step")[0]
|
|
45
|
try:
|
|
46
|
# case in which we already have the node in dict
|
|
47
|
d = cex_dict[node]
|
|
48
|
max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key value and add 1
|
|
49
|
d.update({(max_key+1):ground_pair})
|
|
50
|
except Exception as e:
|
|
51
|
self._log.warning("Adding a new node cex " + str(e))
|
|
52
|
cex_dict.update({node:{k:ground_pair}})
|
|
53
|
else:
|
|
54
|
node = node_name
|
|
55
|
try:
|
|
56
|
d = cex_dict[node]
|
|
57
|
max_key = max(k for k, v in d.iteritems() if v != 0) #get the maximum key value and add 1
|
|
58
|
d.update({(max_key+1):ground_pair})
|
|
59
|
except Exception as e:
|
|
60
|
if node not in ["MAIN", "ERR"]:
|
|
61
|
self._log.warning("Adding a new node cex " + str(e))
|
|
62
|
cex_dict.update({node:{k:ground_pair}})
|
|
63
|
except Exception as e:
|
|
64
|
self._log.warning("Problem with getting a node name: " + str(e))
|
|
65
|
*)
|
|
66
|
) conjuncts in
|
|
67
|
let rules_expr = Z3.Fixedpoint.get_rules !fp in
|
|
68
|
if !debug then
|
|
69
|
Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
|
|
70
|
(Utils.fprintf_list ~sep:"@ "
|
|
71
|
(fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) )
|
|
72
|
rules_expr;
|
|
73
|
if !debug then
|
|
74
|
Format.eprintf "FP help: %s@." (Z3.Fixedpoint.get_help !fp);
|
|
75
|
|
|
76
|
()
|
|
77
|
(* ordered_by_signal = self.reorder(cex_dict) *)
|
|
78
|
(* return self.mk_cex_xml(ordered_by_signal) *)
|
|
79
|
|
|
80
|
|
|
81
|
|