73 val facts = |
73 val facts = |
74 facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) |
74 facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) |
75 val problem = |
75 val problem = |
76 {state = state, goal = goal, subgoal = i, subgoal_count = n, |
76 {state = state, goal = goal, subgoal = i, subgoal_count = n, |
77 facts = facts, smt_filter = NONE} |
77 facts = facts, smt_filter = NONE} |
78 val result as {outcome, used_facts, ...} = prover params (K "") problem |
78 val result as {outcome, used_facts, run_time_in_msecs, ...} = |
|
79 prover params (K "") problem |
79 in |
80 in |
80 print silent (fn () => |
81 print silent (fn () => |
81 case outcome of |
82 case outcome of |
82 SOME failure => string_for_failure failure |
83 SOME failure => string_for_failure failure |
83 | NONE => if length used_facts = length facts then "Found proof." |
84 | NONE => "Found proof" ^ |
84 else "Found proof with " ^ n_facts used_facts ^ "."); |
85 (if length used_facts = length facts then "" |
|
86 else " with " ^ n_facts used_facts) ^ |
|
87 (case run_time_in_msecs of |
|
88 SOME ms => |
|
89 " (" ^ string_from_time (Time.fromMilliseconds ms) ^ ")" |
|
90 | NONE => "") ^ "."); |
85 result |
91 result |
86 end |
92 end |
87 |
93 |
88 (* minimalization of facts *) |
94 (* minimalization of facts *) |
89 |
95 |