Commit bd8b6aca authored by MARCHE Claude's avatar MARCHE Claude

suppress the ad-hoc interpretation of SMTLIB's (get-info :unknown-reason) command

parent 36b42d5e
......@@ -17,7 +17,8 @@ prelude "(set-logic AUFNIRA)"
*)
filename "%f-%t-%g.smt2"
unknown "^\\(unknown\\|sat\\|Fail\\)$" ""
unknown "^\\(unknown\\|sat\\|Fail\\)$" "\\1"
unknown "^(:reason-unknown \\([^)]*\\))$" "\\1"
time "why3cpulimit time : %s s"
valid "^unsat$"
......
......@@ -19,10 +19,6 @@ let debug = Debug.register_info_flag "call_prover"
let debug_attrs = Debug.register_info_flag "print_attrs"
~desc:"Print@ attrs@ of@ identifiers@ and@ expressions."
type reason_unknown =
| Resourceout
| Other
(* BEGIN{proveranswer} anchor for automatic documentation, do not remove *)
type prover_answer =
| Valid
......@@ -30,7 +26,7 @@ type prover_answer =
| Timeout
| OutOfMemory
| StepLimitExceeded
| Unknown of (string * reason_unknown option)
| Unknown of string
| Failure of string
| HighFailure
(* END{proveranswer} anchor for automatic documentation, do not remove *)
......@@ -127,6 +123,7 @@ let rec grep_steps out = function
Some(int_of_string v)
with _ -> grep_steps out l end
(*
let grep_reason_unknown out =
try
(* TODO: this is SMTLIB specific, should be done in drivers instead *)
......@@ -137,6 +134,7 @@ let grep_reason_unknown out =
| _ -> Other
with Not_found ->
Other
*)
type prover_result_parser = {
prp_regexps : (string * prover_answer) list;
......@@ -146,20 +144,13 @@ type prover_result_parser = {
prp_model_parser : Model_parser.model_parser;
}
let print_unknown_reason fmt = function
| Some Resourceout -> fprintf fmt "resource limit reached"
| Some Other -> fprintf fmt "other"
| None -> fprintf fmt "none"
let print_prover_answer fmt = function
| Valid -> fprintf fmt "Valid"
| Invalid -> fprintf fmt "Invalid"
| Timeout -> fprintf fmt "Timeout"
| OutOfMemory -> fprintf fmt "Ouf Of Memory"
| StepLimitExceeded -> fprintf fmt "Step limit exceeded"
| Unknown ("", r) -> fprintf fmt "Unknown (%a)" print_unknown_reason r
| Failure "" -> fprintf fmt "Failure"
| Unknown (s, r) -> fprintf fmt "Unknown %a(%s)" print_unknown_reason r s
| Unknown s -> fprintf fmt "Unknown (%s)" s
| Failure s -> fprintf fmt "Failure (%s)" s
| HighFailure -> fprintf fmt "HighFailure"
......@@ -192,7 +183,7 @@ let rec grep out l = match l with
ignore (Str.search_forward re out 0);
match pa with
| Valid | Invalid | Timeout | OutOfMemory | StepLimitExceeded -> pa
| Unknown (s, ru) -> Unknown ((Str.replace_matched s out), ru)
| Unknown s -> Unknown (Str.replace_matched s out)
| Failure s -> Failure (Str.replace_matched s out)
| HighFailure -> assert false
with Not_found -> grep out l end
......@@ -233,11 +224,20 @@ let debug_print_model ~print_attrs model =
let model_str = Model_parser.model_to_string ~print_attrs model in
Debug.dprintf debug "Call_provers: %s@." model_str
type answer_or_model = Answer of prover_answer | Model of string
let analyse_result res_parser printer_mapping out =
let list_re = res_parser.prp_regexps in
let re = craft_efficient_re list_re in
let list_re = List.map (fun (a, b) -> Str.regexp a, b) list_re in
let result_list = Str.full_split re out in
let result_list =
List.map
(function
| Str.Delim r -> Answer (grep r list_re)
| Str.Text t -> Model t)
result_list
in
(* Format.eprintf "[incremental model parsing] results list is @[[%a]@]@."
(Pp.print_list Pp.semi print_delim) result_list;
*)
......@@ -248,9 +248,25 @@ let analyse_result res_parser printer_mapping out =
(HighFailure, saved_model)
else
(Opt.get saved_res, saved_model)
| Str.Delim res :: Str.Text model :: tl ->
(* Parse the text of the result *)
let res = grep res list_re in
| Answer res1 :: (Answer res2 :: tl as tl1) ->
Debug.dprintf debug "Call_provers: two consecutive answers: %a %a@."
print_prover_answer res1 print_prover_answer res2;
begin
match res1,res2 with
| Unknown _, Unknown "resourceout" ->
analyse saved_model saved_res (Answer StepLimitExceeded :: tl)
| Unknown _, Unknown "timeout" ->
analyse saved_model saved_res (Answer Timeout :: tl)
| Unknown "", Unknown _ ->
analyse saved_model saved_res tl1
| Unknown s1, Unknown "" ->
analyse saved_model saved_res (Answer (Unknown s1) :: tl)
| Unknown s1, Unknown s2 ->
analyse saved_model saved_res (Answer (Unknown (s1 ^ " + " ^ s2)) :: tl)
| _,_ ->
analyse saved_model saved_res tl1
end
| Answer res :: Model model :: tl ->
if res = Valid then
(Valid, None)
else
......@@ -260,13 +276,12 @@ let analyse_result res_parser printer_mapping out =
debug_print_model ~print_attrs:false m;
let m = if is_model_empty m then saved_model else (Some m) in
analyse m (Some res) tl
| Str.Delim res :: tl ->
let res = grep res list_re in
| Answer res :: tl ->
if res = Valid then
(Valid, None)
else
analyse saved_model (Some res) tl
| Str.Text _fail :: tl -> analyse saved_model saved_res tl
| Model _fail :: tl -> analyse saved_model saved_res tl
in
analyse None None result_list
......@@ -288,17 +303,10 @@ let parse_prover_run res_parser signaled time out exitcode limit ~printer_mappin
(* TODO let (n, m, t) = greps out res_parser.prp_regexps in
t, None *)
in
let model = match model with | Some s -> s | None -> default_model in
let model = match model with Some s -> s | None -> default_model in
Debug.dprintf debug "Call_provers: prover output:@\n%s@." out;
let time = Opt.get_def (time) (grep_time out res_parser.prp_timeregexps) in
let steps = Opt.get_def (-1) (grep_steps out res_parser.prp_stepregexps) in
(* add info for unknown if possible. FIXME: this is too SMTLIB specific *)
let ans = match ans with
| Unknown (s, _) ->
let reason_unknown = grep_reason_unknown out in
Unknown (s, Some reason_unknown)
| _ -> ans
in
(* HighFailure or Unknown close to time limit are assumed to be timeouts *)
let tlimit = float limit.limit_time in
let ans, time =
......@@ -488,7 +496,7 @@ let query_result_buffer id =
with Not_found -> NoUpdates
let editor_result ret = {
pr_answer = Unknown ("", None);
pr_answer = Unknown "not yet edited";
pr_status = ret;
pr_output = "";
pr_time = 0.0;
......
......@@ -15,13 +15,6 @@ open Model_parser
(** {2 data types for prover answers} *)
(** The reason why unknown was reported *)
type reason_unknown =
| Resourceout
(** Out of resources *)
| Other
(** Other reason *)
type prover_answer =
| Valid
(** The task is valid according to the prover *)
......@@ -33,7 +26,7 @@ type prover_answer =
(** the task runs out of memory *)
| StepLimitExceeded
(** the task required more steps than the limit provided *)
| Unknown of (string * reason_unknown option)
| Unknown of string
(** The prover can't determine if the task is valid *)
| Failure of string
(** The prover reports a failure *)
......
......@@ -93,7 +93,7 @@ let load_driver_absolute = let driver_tag = ref (-1) in fun env file extra_files
| RegexpOutOfMemory s -> add_to_list regexps (s, OutOfMemory)
| RegexpStepLimitExceeded s ->
add_to_list regexps (s, StepLimitExceeded)
| RegexpUnknown (s,t) -> add_to_list regexps (s, Unknown (t, None))
| RegexpUnknown (s,t) -> add_to_list regexps (s, Unknown t)
| RegexpFailure (s,t) -> add_to_list regexps (s, Failure t)
| TimeRegexp r -> add_to_list timeregexps (Call_provers.timeregexp r)
| StepRegexp (r,ns) ->
......@@ -104,7 +104,7 @@ let load_driver_absolute = let driver_tag = ref (-1) in fun env file extra_files
| ExitCodeOutOfMemory s -> add_to_list exitcodes (s, OutOfMemory)
| ExitCodeStepLimitExceeded s ->
add_to_list exitcodes (s, StepLimitExceeded)
| ExitCodeUnknown (s,t) -> add_to_list exitcodes (s, Unknown (t, None))
| ExitCodeUnknown (s,t) -> add_to_list exitcodes (s, Unknown t)
| ExitCodeFailure (s,t) -> add_to_list exitcodes (s, Failure t)
| Filename s -> set_or_raise loc filename s "filename"
| Printer s -> set_or_raise loc printer s "printer"
......
......@@ -521,6 +521,9 @@ let add_check_sat info fmt =
if info.info_cntexample && info.info_cntexample_need_push then
fprintf fmt "@[(push)@]@\n";
fprintf fmt "@[(check-sat)@]@\n";
(* unfortunately we can't do that unconditionally, since it will make
CVC4 fail and immediately exit if last answer was not 'unknown' *)
(* fprintf fmt "@[(get-info :reason-unknown)@]@\n"; *)
if info.info_cntexample then
fprintf fmt "@[(get-model)@]@\n"
......
......@@ -51,7 +51,7 @@ let convert_prover_answer (pa: prover_answer) =
| Timeout -> "Timeout",""
| OutOfMemory -> "OutOfMemory",""
| StepLimitExceeded -> "StepLimitExceeded",""
| Unknown(s,_) -> "Unknown",s
| Unknown s -> "Unknown",s
| Failure s -> "Failure",s
| HighFailure -> "HighFailure",""
......@@ -533,7 +533,7 @@ let parse_prover_answer a d =
| "Timeout" -> Timeout
| "OutOfMemory" -> OutOfMemory
| "StepLimitExceeded" -> StepLimitExceeded
| "Unknown" -> Unknown (d,None)
| "Unknown" -> Unknown d
| "Failure" -> Failure d
| "HighFailure" -> HighFailure
| _ -> HighFailure
......
......@@ -930,7 +930,7 @@ let load_result r =
match status with
| "valid" -> Call_provers.Valid
| "invalid" -> Call_provers.Invalid
| "unknown" -> Call_provers.Unknown ("", None)
| "unknown" -> Call_provers.Unknown ""
| "timeout" -> Call_provers.Timeout
| "outofmemory" -> Call_provers.OutOfMemory
| "failure" -> Call_provers.Failure ""
......
......@@ -164,7 +164,7 @@ the proof containing this prover are selected";
Arg.Unit (fun () -> opt_status := Call_provers.Invalid::!opt_status),
" filter the invalid goals";
"--filter-unknown",
Arg.String (fun s -> opt_status := Call_provers.Unknown (s, None)::!opt_status),
Arg.String (fun s -> opt_status := Call_provers.Unknown s::!opt_status),
" filter when the prover reports it can't determine if the task is valid";
"--filter-failure",
Arg.String (fun s -> opt_status := Call_provers.Failure s::!opt_status),
......
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