Project

General

Profile

« Previous | Next » 

Revision 57d61d67

Added by Pierre-Loïc Garoche over 6 years ago

New option to select github version of Z3
Added Yojson dependency in lustrev
Some progress on Cex generation

View differences:

src/tools/zustre/zustre_verifier.ml
64 64
        active := true;
65 65
        Options.output := "horn";
66 66
      )
67

  
67 68
    let is_active () = !active
68 69

  
69 70
    let get_normalization_params () =
......
136 137
       *        self.fp.set ('xform.slice', False)
137 138
       *        self.fp.set ('xform.inline_linear',False)
138 139
       *        self.fp.set ('xform.inline_eager',False) *\) *)
139
      if !param_pp then (
140
      if not !param_pp then (
141
	(* Mandatory to print all steps and recover cex *)
140 142
        P.add_bool fp_params (mks "xform.slice") false;
141 143
        P.add_bool fp_params (mks "xform.inline_linear") false;
142 144
        P.add_bool fp_params (mks "xform.inline_eager") false
......
145 147

  
146 148
      (* Ploc's options. Do not seem to have any effect yet *)
147 149
      P.add_bool fp_params (mks "print_answer") true;
148
      P.add_bool fp_params (mks "print_certificate") true;
149
      P.add_bool fp_params (mks "xform.slice") false;
150
      (* P.add_bool fp_params (mks "print_certificate") true; *)
151
      P.add_bool fp_params (mks "xform.slice") false ; (* required to preserve signatures *)
152

  
153
      (* P.add_bool fp_params (mks "print_statistics") true; *)
154
      (* P.add_bool fp_params (mks "print_certificate") true;  *)
150 155

  
151 156
      (* Adding a timeout *)
152 157
      P.add_int fp_params (mks "timeout") !timeout;
......
165 170
      *)
166 171
      if false then (
167 172
	
168
	let queries = Z3.Fixedpoint.parse_file !fp "mini.smt2" in
173
	let queries = Z3.Fixedpoint.parse_file !fp "nstep.smt2" in
169 174

  
170 175
	(* Debug instructions *)
171 176
	
......
183 188
	
184 189
	let _ = List.map extract_expr_fds rules_expr in
185 190
	Format.eprintf "%t" pp_fdecls;
191

  
192
	let decl_err = List.hd queries in
193
      	let res_status = Z3.Fixedpoint.query !fp decl_err in
186 194
	
187
      	let res_status = Z3.Fixedpoint.query !fp (List.hd queries )in
188
	
189
	Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status)
195
	Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);
196
	(* let _ =  *)
197
	(*   match res_status with *)
198
	(*   | Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex machine machines decl_err *)
199
	(*   | _ -> () *)
200
	(* in *)
201
	exit 0
190 202
      )
191 203
      else if false then (
192 204

  
......
250 262
	    end: VerifierType.S)
251 263
    
252 264
(* Local Variables: *)
253
(* compile-command:"make -C ../.." *)
265
(* compile-command:"make -C ../.. lustrev" *)
254 266
(* End: *)

Also available in: Unified diff