19 |
19 |
20 open Sledgehammer_Proof |
20 open Sledgehammer_Proof |
21 open Sledgehammer_Preplay |
21 open Sledgehammer_Preplay |
22 |
22 |
23 fun variants (Let _) = raise Fail "Sledgehammer_Try0: variants" |
23 fun variants (Let _) = raise Fail "Sledgehammer_Try0: variants" |
24 | variants (Prove (qs, xs, l, t, subproofs, By (facts, _))) = |
24 | variants (Prove (qs, xs, l, t, subproofs, (facts, _))) = |
25 let |
25 let |
26 val methods = [SimpM, FastforceM, AutoM, ArithM, ForceM, BlastM] |
26 val methods = [SimpM, FastforceM, AutoM, ArithM, ForceM, BlastM] |
27 fun step method = Prove (qs, xs, l, t, subproofs, By (facts, method)) |
27 fun step method = Prove (qs, xs, l, t, subproofs, (facts, method)) |
28 (*fun step_without_facts method = |
28 (*fun step_without_facts method = |
29 Prove (qs, xs, l, t, subproofs, By (no_facts, method))*) |
29 Prove (qs, xs, l, t, subproofs, (no_facts, method))*) |
30 in |
30 in |
31 (* FIXME *) |
31 (* FIXME *) |
32 (* There seems to be a bias for methods earlier in the list, so we put |
32 (* There seems to be a bias for methods earlier in the list, so we put |
33 the variants using no facts first. *) |
33 the variants using no facts first. *) |
34 (*map step_without_facts methods @*) map step methods |
34 (*map step_without_facts methods @*) map step methods |