Revision 57d61d67
Added by Pierre-Loïc Garoche over 6 years ago
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
New option to select github version of Z3
Added Yojson dependency in lustrev
Some progress on Cex generation