Project

General

Profile

Revision 7d77632f src/tools/zustre/zustre_cex.ml

View differences:

src/tools/zustre/zustre_cex.ml
46 46
  let nb_outputs = List.length inputs in
47 47
  let nb_mems = List.length (full_memory_vars machines machine) in
48 48
  
49
  let main =
50
    List.fold_left (fun accu conj ->
49
  let main, funs =
50
    List.fold_left (fun (main, funs) conj ->
51 51
    (* Filtering out non MAIN decls *)
52 52
    let func_decl = Z3.Expr.get_func_decl conj in
53 53
    let node_name = Z3.Symbol.get_string (Z3.FuncDecl.get_name func_decl) in
54 54
    (* Focusing only on MAIN_nodeid predicates *)
55 55
    if node_name = "MAIN_" ^ node_id then
56 56
      (* Extracting info *)
57
      (* Recall that MAIN args are 
58
	 main_input @ 
59
	 (full_memory_vars machines machine) @
60
	 main_output   *)
57
      (* Recall that MAIN args are in@mems@out *)
61 58
      let args = Z3.Expr.get_args conj in
62 59
      if List.length args = 1 + nb_inputs + nb_mems + nb_outputs then
63 60
	let id = Z3.Arithmetic.Integer.get_int (List.hd args) in
64 61
	let input_values = Utils.List.extract args 1 (1 + nb_inputs) in
65 62
	let output_values = Utils.List.extract args (1+nb_inputs+nb_mems) (1 + nb_inputs + nb_mems + nb_outputs) in
66
	(id, (input_values, output_values))::accu
63
	(id, (input_values, output_values))::main, funs
67 64
      else
68 65
	assert false
69 66
    else
70
      accu 
71
  ) [] conjuncts
67
      let reg = Str.regexp_string "[a-z]*_step" in
68
      if Str.string_match reg node_name 0 then (
69
	let actual_name = Str.matched_group 0 node_name in
70
	Format.eprintf "Name %s@." actual_name;
71
	main, funs
72
      )
73
      else (
74
	Format.eprintf "pas matché %s@." node_name;
75
	main, funs
76
      )
77
    ) ((* main*) [],(* other functions *) []) conjuncts
72 78
  in
73 79
  let main = List.sort (fun (id1, _) (id2, _) -> compare id1 id2) main in
74 80
  List.iter (
......
147 153
  (*     Format.eprintf "FP help: %s@." (Z3.Fixedpoint.get_help !fp); *)
148 154

  
149 155
  let stats_entries =   Z3.Statistics.get_entries stats in
150
  List.iter (fun e -> Format.eprintf "%s@.@?"
151
    (Z3.Statistics.Entry.to_string e)
156
  (* List.iter (fun e -> Format.eprintf "%s@.@?" *)
157
  (*   (Z3.Statistics.Entry.to_string e) *)
152 158
    
153
  ) stats_entries;
159
  (* ) stats_entries; *)
154 160
  let json : Yojson.json =
155 161
    `Assoc [
156 162
      "Results",

Also available in: Unified diff