Commit 5c3038bf authored by David Hauzar's avatar David Hauzar

Query cvc4 for reason of answer unknown and use it for counterexamples.

When resource limit is hit, cvc4 outputs useless counterexample. Query
cvc4 for the reason of answer unknown and use the answer to decide
whether resource limit was hit. If it was hit, do not display the
counterexample.

* src/driver/call_provers.{ml|mli}
(parse_prover_run): If the prover answers unknown, get the information
about the reason of this answer.

* src/printer/smtv2.ml
(print_prop_decl): Query solver for the reason of answer unknown.

* src/driver/driver.ml
(load_driver): Initialize Unknown with no information about the reason
of answer unknown.

* src/session/session.ml
(load_result): Initialize Unknown with no information about the reason
of answer unknown.

* src/session/session_scheduler.ml
(schedule_proof_attempt)
(edit_proof): Initialize Unknown with no information about the reason
of answer unknown.

* src/why3session/why3session_lib.ml
(filter_spec): Initialize Unknown with no information about the reason
of answer unknown.
parent 4dfa48b8
......@@ -16,6 +16,29 @@ let debug = Debug.register_info_flag "call_prover"
~desc:"Print@ debugging@ messages@ about@ prover@ calls@ \
and@ keep@ temporary@ files."
type reason_unknown =
| Resourceout
| Other
type prover_answer =
| Valid
| Invalid
| Timeout
| OutOfMemory
| StepLimitExceeded
| Unknown of (string * reason_unknown option)
| Failure of string
| HighFailure
type prover_result = {
pr_answer : prover_answer;
pr_status : Unix.process_status;
pr_output : string;
pr_time : float;
pr_steps : int; (* -1 if unknown *)
pr_model : model;
}
(** time regexp "%h:%m:%s" *)
type timeunit =
| Hour
......@@ -83,26 +106,15 @@ let rec grep_steps out = function
with _ -> grep_steps out l
end
(** *)
type prover_answer =
| Valid
| Invalid
| Timeout
| OutOfMemory
| StepLimitExceeded
| Unknown of string
| Failure of string
| HighFailure
type prover_result = {
pr_answer : prover_answer;
pr_status : Unix.process_status;
pr_output : string;
pr_time : float;
pr_steps : int; (* -1 if unknown *)
pr_model : model;
}
let grep_reason_unknown out =
try
let re = Str.regexp "^(:reason-unknown \\([^)]*\\)" in
ignore (Str.search_forward re out 0);
match (Str.matched_group 1 out) with
| "resourceout" -> Resourceout
| _ -> Other
with Not_found ->
Other
type prover_result_parser = {
prp_regexps : (Str.regexp * prover_answer) list;
......@@ -118,9 +130,9 @@ let print_prover_answer fmt = function
| Timeout -> fprintf fmt "Timeout"
| OutOfMemory -> fprintf fmt "Ouf Of Memory"
| StepLimitExceeded -> fprintf fmt "Step limit exceeded"
| Unknown "" -> fprintf fmt "Unknown"
| Unknown ("", _) -> fprintf fmt "Unknown"
| Failure "" -> fprintf fmt "Failure"
| Unknown s -> fprintf fmt "Unknown (%s)" s
| Unknown (s, _) -> fprintf fmt "Unknown (%s)" s
| Failure s -> fprintf fmt "Failure (%s)" s
| HighFailure -> fprintf fmt "HighFailure"
......@@ -151,7 +163,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 -> Unknown (Str.replace_matched s out)
| Unknown (s, ru) -> Unknown ((Str.replace_matched s out), ru)
| Failure s -> Failure (Str.replace_matched s out)
| HighFailure -> assert false
with Not_found -> grep out l end
......@@ -188,6 +200,10 @@ let parse_prover_run res_parser time out ret on_timelimit timelimit ~printer_map
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
let reason_unknown = grep_reason_unknown out in
let ans = match ans with
| Unknown (s, _) -> Unknown (s, Some reason_unknown)
| _ -> ans in
let ans = match ans with
| Unknown _ | HighFailure when on_timelimit && timelimit > 0
&& time >= (0.9 *. float timelimit) -> Timeout
......
......@@ -15,6 +15,13 @@ 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 *)
......@@ -26,7 +33,7 @@ type prover_answer =
(** the task runs out of memory *)
| StepLimitExceeded
(** the task required more steps than the limit provided *)
| Unknown of string
| Unknown of (string * reason_unknown option)
(** The prover can't determine if the task is valid *)
| Failure of string
(** The prover reports a failure *)
......@@ -45,8 +52,8 @@ type prover_result = {
(** The time taken by the prover *)
pr_steps : int;
(** The number of steps taken by the prover (-1 if not available) *)
(** The model produced by a the solver *)
pr_model : model;
(** The model produced by a the solver *)
}
val print_prover_answer : Format.formatter -> prover_answer -> unit
......
......@@ -92,7 +92,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
| RegexpOutOfMemory s -> add_to_list regexps (Str.regexp s, OutOfMemory)
| RegexpStepLimitExceeded s ->
add_to_list regexps (Str.regexp s, StepLimitExceeded)
| RegexpUnknown (s,t) -> add_to_list regexps (Str.regexp s, Unknown t)
| RegexpUnknown (s,t) -> add_to_list regexps (Str.regexp s, Unknown (t, None))
| RegexpFailure (s,t) -> add_to_list regexps (Str.regexp s, Failure t)
| TimeRegexp r -> add_to_list timeregexps (Call_provers.timeregexp r)
| StepRegexp (r,ns) ->
......@@ -103,7 +103,7 @@ let load_driver = 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)
| ExitCodeUnknown (s,t) -> add_to_list exitcodes (s, Unknown (t, None))
| 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"
......
......@@ -582,6 +582,8 @@ let print_prop_decl vc_loc cntexample args info fmt k pr f = match k with
let model_list = S.elements info.info_model in
fprintf fmt "@[(check-sat)@]@\n";
print_info_model cntexample fmt model_list info;
(* (get-info :reason-unknown) *)
fprintf fmt "@[(get-info :reason-unknown)@]@\n";
args.printer_mapping <- { lsymbol_m = args.printer_mapping.lsymbol_m;
vc_term_loc = vc_loc;
......
......@@ -1168,7 +1168,7 @@ let load_result r =
match status with
| "valid" -> Call_provers.Valid
| "invalid" -> Call_provers.Invalid
| "unknown" -> Call_provers.Unknown ""
| "unknown" -> Call_provers.Unknown ("", None)
| "timeout" -> Call_provers.Timeout
| "outofmemory" -> Call_provers.OutOfMemory
| "failure" -> Call_provers.Failure ""
......@@ -1194,7 +1194,7 @@ let load_result r =
Call_provers.pr_output = "";
Call_provers.pr_status = Unix.WEXITED 0;
Call_provers.pr_steps = steps;
Call_provers.pr_model = Model_parser.default_model
Call_provers.pr_model = Model_parser.default_model;
}
| "undone" -> Interrupted
| "unedited" -> Unedited
......
......@@ -290,7 +290,7 @@ let schedule_proof_attempt ~cntexample ~timelimit ~memlimit ~steplimit ?old ~inp
let schedule_edition t command filename callback =
Debug.dprintf debug "[Sched] Scheduling an edition@.";
let res_parser =
{ Call_provers.prp_exitcodes = [(0,Call_provers.Unknown "")];
{ Call_provers.prp_exitcodes = [(0,Call_provers.Unknown ("", None))];
Call_provers.prp_regexps = [];
Call_provers.prp_timeregexps = [];
Call_provers.prp_stepregexps = [];
......@@ -861,7 +861,7 @@ let edit_proof ~cntexample eS sched ~default_editor a =
else
let callback a res =
match res with
| Done {Call_provers.pr_answer = Call_provers.Unknown ""} ->
| Done {Call_provers.pr_answer = Call_provers.Unknown ("", None)} ->
set_proof_state ~notify ~obsolete:true ~archived:false
JustEdited a
| _ ->
......@@ -873,7 +873,7 @@ let edit_proof ~cntexample eS sched ~default_editor a =
let edit_proof_v3 ~cntexample eS sched ~default_editor ~callback a =
let callback a res =
match res with
| Done {Call_provers.pr_answer = Call_provers.Unknown ""} ->
| Done {Call_provers.pr_answer = Call_provers.Unknown ("", None)} ->
callback a
| _ -> ()
in
......
......@@ -148,7 +148,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::!opt_status),
Arg.String (fun s -> opt_status := Call_provers.Unknown (s, None)::!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