Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 9ef97dbb authored by Sylvain Dailler's avatar Sylvain Dailler

Q316-004 Remove get-info

Do not print (get-info :reason-unknown) on smt2 output. Previously,
detection of end of model and beginning of statistics was done by using
the reason. We now detect a single parenthesis on a line: every cvc4 model
ends with this (we assume statistics does not contain a line beginning
with a closing parenthesis). As a side effect, we also find
more counterexamples.

* src/driver/parse_smtv2_model.ml
(parse): Revert changes that were detecting Abort trap.

* src/driver/parse_smtv2_model_parser.mly
(output): Revert changes to allow absence of parenthesis at the end. Also
removed parsing on results given by the reason. Now match on ).

* src/printer/smtv2_cvc_ce.ml
(print_prop_decl): Remove (get-info :reason-unknown).

* src/printer/smtv2.ml
(print_prop_decl): Remove get-info for coherence.

Change-Id: Ifbd7b2b9ce499f8aaa020f58375d784793990965
parent 4e94e8dc
......@@ -62,15 +62,9 @@ let parse : raw_model_parser = function input ->
let r = Str.regexp "unknown\\|sat\\|\\(I don't know.*\\)" in
ignore (Str.search_forward r input 0);
let match_end = Str.match_end () in
let nr1 = Str.regexp "(:reason-unknown" in
let nr2 = Str.regexp "(error \"Can" in
let nr3 = Str.regexp "Abort trap" in (* TODO bug on mac *)
let res1 = try Str.search_forward nr1 input 0 with Not_found -> 0 in
let res2 = try Str.search_forward nr2 input 0 with Not_found -> 0 in
let res3 = try Str.search_forward nr3 input 0 with Not_found -> 0 in
let res = max (max res1 res2) res3 in
let model_string =
if res = 0 then "" else String.sub input match_end (res - match_end) in
let nr = Str.regexp "^)" in
let res = Str.search_backward nr input (String.length input) in
let model_string = String.sub input match_end (res + 1 - match_end) in
do_parsing model_string
with
| Not_found -> []
......
......@@ -50,13 +50,12 @@
output:
| EOF { Stdlib.Mstr.empty }
| LPAREN ps MODEL ps list_decls (* RPAREN *) { $5 } (* TODO cvc4 bug mac *)
| LPAREN ps MODEL ps list_decls RPAREN { $5 }
list_decls:
| LPAREN decl RPAREN ps EOF { Smt2_model_defs.add_element $2 Stdlib.Mstr.empty false}
| LPAREN decl RPAREN ps { Smt2_model_defs.add_element $2 Stdlib.Mstr.empty false}
| LPAREN decl RPAREN ps list_decls { Smt2_model_defs.add_element $2 $5 false }
| RPAREN EOF { Stdlib.Mstr.empty }
| COMMENT ps list_decls EOF { $3 } (* Lines beginning with ';' are ignored *)
| COMMENT ps list_decls { $3 } (* Lines beginning with ';' are ignored *)
(* Examples:
"(define-fun to_rep ((_ufmt_1 enum_t)) Int 0)"
......
......@@ -466,10 +466,6 @@ let print_prop_decl vc_loc cntexample args info fmt k pr f = match k with
(*if cntexample then fprintf fmt "@[(push)@]@\n"; (* z3 specific stuff *)*)
fprintf fmt "@[(check-sat)@]@\n";
let model_list = print_info_model cntexample fmt info in
if cntexample then begin
(* (get-info :reason-unknown) *)
fprintf fmt "@[(get-info :reason-unknown)@]@\n";
end;
args.printer_mapping <- { lsymbol_m = args.printer_mapping.lsymbol_m;
vc_term_loc = vc_loc;
......
......@@ -486,10 +486,6 @@ let print_prop_decl vc_loc cntexample args info fmt k pr f = match k with
(*if cntexample then fprintf fmt "@[(push)@]@\n"; (* z3 specific stuff *)*)
fprintf fmt "@[(check-sat)@]@\n";
let model_list = print_info_model cntexample fmt info in
if cntexample then begin
(* (get-info :reason-unknown) *)
fprintf fmt "@[(get-info :reason-unknown)@]@\n";
end;
args.printer_mapping <- { lsymbol_m = args.printer_mapping.lsymbol_m;
vc_term_loc = vc_loc;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment