Commit 4e94e8dc authored by Sylvain Dailler's avatar Sylvain Dailler

Q316-004 Parse cvc4 output on mac

This patch allows parsing model including the error message raised by cvc4
on mac.

* src/driver/parse_smtv2_model.ml
(parse): Allow parsing of specific error message "Abort trap".
(output): Allow parsing when last parenthesis is missing which is the case
when the bug is occuring.

Change-Id: I80d7276d37916e09ba4bb28478ac9a7427789771
parent cffa3177
......@@ -64,9 +64,11 @@ let parse : raw_model_parser = function input ->
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 res = max (res1) (res2) 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
do_parsing model_string
......
......@@ -50,12 +50,13 @@
output:
| EOF { Stdlib.Mstr.empty }
| LPAREN ps MODEL ps list_decls RPAREN { $5 }
| LPAREN ps MODEL ps list_decls (* RPAREN *) { $5 } (* TODO cvc4 bug mac *)
list_decls:
| LPAREN decl RPAREN ps { Smt2_model_defs.add_element $2 Stdlib.Mstr.empty false}
| LPAREN decl RPAREN ps EOF { Smt2_model_defs.add_element $2 Stdlib.Mstr.empty false}
| LPAREN decl RPAREN ps list_decls { Smt2_model_defs.add_element $2 $5 false }
| COMMENT ps list_decls { $3 } (* Lines beginning with ';' are ignored *)
| RPAREN EOF { Stdlib.Mstr.empty }
| COMMENT ps list_decls EOF { $3 } (* Lines beginning with ';' are ignored *)
(* Examples:
"(define-fun to_rep ((_ufmt_1 enum_t)) Int 0)"
......
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