Revision 51ec4e8c
Added by Pierre-Loïc Garoche almost 7 years ago
| src/tools/zustre/zustre_verifier.ml | ||
|---|---|---|
| 83 | 83 |
let mks = S.mk_string !ctx in |
| 84 | 84 |
let params = P.mk_params !ctx in |
| 85 | 85 |
|
| 86 |
(* self.fp.set (engine='spacer') *)
|
|
| 86 |
(* (\* self.fp.set (engine='spacer') *\) *)
|
|
| 87 | 87 |
P.add_symbol params (mks "engine") (mks "spacer"); |
| 88 |
(* P.add_symbol params (mks "engine") (mks "pdr"); *) |
|
| 88 | 89 |
|
| 89 | 90 |
(* #z3.set_option(rational_to_decimal=True) *) |
| 90 | 91 |
(* #self.fp.set('precision',30) *)
|
| ... | ... | |
| 152 | 153 |
|
| 153 | 154 |
let queries = Z3.Fixedpoint.parse_file !fp "mini.smt2" in |
| 154 | 155 |
|
| 155 |
(* Debug instructions *) |
|
| 156 |
let rules_expr = Z3.Fixedpoint.get_rules !fp in |
|
| 157 |
Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." |
|
| 158 |
(Utils.fprintf_list ~sep:"@ " |
|
| 159 |
(fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) |
|
| 160 |
rules_expr; |
|
| 156 |
(* Debug instructions *) |
|
| 157 |
|
|
| 161 | 158 |
|
| 162 |
let res_status = Z3.Fixedpoint.query !fp (List.hd queries )in |
|
| 159 |
|
|
| 160 |
let rules_expr = Z3.Fixedpoint.get_rules !fp in |
|
| 161 |
Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." |
|
| 162 |
(Utils.fprintf_list ~sep:"@ " |
|
| 163 |
(fun fmt e -> |
|
| 164 |
(* let e2 = Z3.Quantifier.get_body eq in *) |
|
| 165 |
(* let fd = Z3.Expr.get_func_decl e in *) |
|
| 166 |
Format.fprintf fmt "Rule: %s@." |
|
| 167 |
(Z3.Expr.to_string e); |
|
| 168 |
)) rules_expr; |
|
| 169 |
|
|
| 170 |
let _ = List.map extract_expr_fds rules_expr in |
|
| 171 |
Format.eprintf "%t" pp_fdecls; |
|
| 172 |
|
|
| 173 |
let res_status = Z3.Fixedpoint.query !fp (List.hd queries )in |
|
| 163 | 174 |
|
| 164 | 175 |
Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status) |
| 165 | 176 |
) |
| 177 |
else if false then ( |
|
| 178 |
|
|
| 179 |
(* No queries here *) |
|
| 180 |
let _ = Z3.Fixedpoint.parse_file !fp "mini_decl.smt2" in |
|
| 181 |
|
|
| 182 |
(* Debug instructions *) |
|
| 183 |
|
|
| 184 |
|
|
| 185 |
|
|
| 186 |
let rules_expr = Z3.Fixedpoint.get_rules !fp in |
|
| 187 |
Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." |
|
| 188 |
(Utils.fprintf_list ~sep:"@ " |
|
| 189 |
(fun fmt e -> |
|
| 190 |
(* let e2 = Z3.Quantifier.get_body eq in *) |
|
| 191 |
(* let fd = Z3.Expr.get_func_decl e in *) |
|
| 192 |
Format.fprintf fmt "Rule: %s@." |
|
| 193 |
(Z3.Expr.to_string e); |
|
| 194 |
)) rules_expr; |
|
| 195 |
|
|
| 196 |
let _ = List.map extract_expr_fds rules_expr in |
|
| 197 |
Format.eprintf "%t" pp_fdecls; |
|
| 198 |
|
|
| 199 |
if !Options.main_node <> "" then |
|
| 200 |
begin |
|
| 201 |
Zustre_analyze.check machines !Options.main_node |
|
| 202 |
|
|
| 203 |
end |
|
| 204 |
else |
|
| 205 |
failwith "Require main node"; |
|
| 206 |
|
|
| 207 |
() |
|
| 208 |
) |
|
| 166 | 209 |
else ( |
| 167 | 210 |
|
| 168 | 211 |
|
| 169 |
decl_sorts ();
|
|
| 170 |
|
|
| 171 |
List.iter (decl_machine machines) (List.rev machines);
|
|
| 212 |
decl_sorts ();
|
|
| 213 |
|
|
| 214 |
List.iter (decl_machine machines) (List.rev machines);
|
|
| 172 | 215 |
|
| 173 | 216 |
|
| 174 |
(* (\* Debug instructions *\) *)
|
|
| 175 |
(* let rules_expr = Z3.Fixedpoint.get_rules !fp in *)
|
|
| 176 |
(* Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." *)
|
|
| 177 |
(* (Utils.fprintf_list ~sep:"@ " *)
|
|
| 178 |
(* (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *)
|
|
| 179 |
(* rules_expr; *)
|
|
| 217 |
(* (\* Debug instructions *\) *)
|
|
| 218 |
(* let rules_expr = Z3.Fixedpoint.get_rules !fp in *)
|
|
| 219 |
(* Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." *)
|
|
| 220 |
(* (Utils.fprintf_list ~sep:"@ " *)
|
|
| 221 |
(* (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *)
|
|
| 222 |
(* rules_expr; *)
|
|
| 180 | 223 |
|
| 181 |
if !Options.main_node <> "" then
|
|
| 182 |
begin |
|
| 183 |
Zustre_analyze.check machines !Options.main_node |
|
| 224 |
if !Options.main_node <> "" then
|
|
| 225 |
begin
|
|
| 226 |
Zustre_analyze.check machines !Options.main_node
|
|
| 184 | 227 |
|
| 185 |
end |
|
| 186 |
else
|
|
| 187 |
failwith "Require main node"; |
|
| 188 |
|
|
| 189 |
()
|
|
| 228 |
end
|
|
| 229 |
else
|
|
| 230 |
failwith "Require main node";
|
|
| 231 |
|
|
| 232 |
()
|
|
| 190 | 233 |
) |
| 191 | 234 |
|
| 192 | 235 |
|
| 193 |
end: VerifierType.S) |
|
| 236 |
end: VerifierType.S)
|
|
| 194 | 237 |
|
| 195 | 238 |
(* Local Variables: *) |
| 196 | 239 |
(* compile-command:"make -C ../.." *) |
Also available in: Unified diff
Try to debug the use of Z3 API. Still having troubles