334 prem_role = Conjecture, |
334 prem_role = Conjecture, |
335 best_slices = fn ctxt => |
335 best_slices = fn ctxt => |
336 let val heuristic = effective_e_selection_heuristic ctxt in |
336 let val heuristic = effective_e_selection_heuristic ctxt in |
337 (* FUDGE *) |
337 (* FUDGE *) |
338 if heuristic = e_smartN then |
338 if heuristic = e_smartN then |
339 [(0.1667, (((128, meshN), FOF, "mono_tags??", combsN, false), e_fun_weightN)), |
339 [(0.15, (((128, meshN), FOF, "mono_tags??", combsN, false), e_fun_weightN)), |
340 (0.1667, (((128, mashN), FOF, "mono_guards??", combsN, false), e_sym_offset_weightN)), |
340 (0.15, (((128, mashN), FOF, "mono_guards??", combsN, false), e_sym_offset_weightN)), |
341 (0.1666, (((91, mepoN), FOF, "mono_tags??", combsN, false), e_autoN)), |
341 (0.15, (((91, mepoN), FOF, "mono_tags??", combsN, false), e_autoN)), |
342 (0.1667, (((64, mashN), FOF, "mono_guards??", combsN, false), e_fun_weightN)), |
342 (0.15, (((64, mashN), FOF, "mono_guards??", combsN, false), e_fun_weightN)), |
343 (0.1667, (((1000, meshN), FOF, "poly_guards??", combsN, false), e_sym_offset_weightN)), |
343 (0.15, (((1000, meshN), FOF, "poly_guards??", combsN, false), e_sym_offset_weightN)), |
344 (0.1666, (((256, mepoN), FOF, "mono_tags??", liftingN, false), e_fun_weightN))] |
344 (0.25, (((256, mepoN), FOF, "mono_tags??", liftingN, false), e_fun_weightN))] |
345 else |
345 else |
346 [(1.0, (((500, ""), FOF, "mono_tags??", combsN, false), heuristic))] |
346 [(1.0, (((500, ""), FOF, "mono_tags??", combsN, false), heuristic))] |
347 end, |
347 end, |
348 best_max_mono_iters = default_max_mono_iters, |
348 best_max_mono_iters = default_max_mono_iters, |
349 best_max_new_mono_instances = default_max_new_mono_instances} |
349 best_max_new_mono_instances = default_max_new_mono_instances} |
505 (InternalError, "Please report this error")] @ |
505 (InternalError, "Please report this error")] @ |
506 known_perl_failures, |
506 known_perl_failures, |
507 prem_role = Conjecture, |
507 prem_role = Conjecture, |
508 best_slices = fn ctxt => |
508 best_slices = fn ctxt => |
509 (* FUDGE *) |
509 (* FUDGE *) |
510 [(0.1667, (((150, meshN), DFG Monomorphic, "mono_native", combsN, true), "")), |
510 [(0.15, (((150, meshN), DFG Monomorphic, "mono_native", combsN, true), "")), |
511 (0.1667, (((500, mepoN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)), |
511 (0.15, (((500, mepoN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)), |
512 (0.1666, (((50, mashN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2LR0LT0)), |
512 (0.15, (((50, mashN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2LR0LT0)), |
513 (0.1000, (((250, mepoN), DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0)), |
513 (0.10, (((250, mepoN), DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0)), |
514 (0.1000, (((1000, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS)), |
514 (0.10, (((1000, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS)), |
515 (0.1000, (((150, mashN), DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)), |
515 (0.10, (((150, mashN), DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)), |
516 (0.1000, (((300, mepoN), DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS)), |
516 (0.10, (((300, mepoN), DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS)), |
517 (0.1000, (((100, meshN), DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))] |
517 (0.15, (((100, meshN), DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))] |
518 |> (case Config.get ctxt spass_extra_options of |
518 |> (case Config.get ctxt spass_extra_options of |
519 "" => I |
519 "" => I |
520 | opts => map (apsnd (apsnd (K opts)))), |
520 | opts => map (apsnd (apsnd (K opts)))), |
521 best_max_mono_iters = default_max_mono_iters, |
521 best_max_mono_iters = default_max_mono_iters, |
522 best_max_new_mono_instances = default_max_new_mono_instances} |
522 best_max_new_mono_instances = default_max_new_mono_instances} |
559 known_szs_status_failures, |
559 known_szs_status_failures, |
560 prem_role = Conjecture, |
560 prem_role = Conjecture, |
561 best_slices = fn ctxt => |
561 best_slices = fn ctxt => |
562 (* FUDGE *) |
562 (* FUDGE *) |
563 (if is_vampire_beyond_1_8 () then |
563 (if is_vampire_beyond_1_8 () then |
564 [(0.1667, (((128, meshN), vampire_tff0, "mono_guards??", combs_or_liftingN, false), e_fun_weightN)), |
564 [(0.20, (((128, meshN), vampire_tff0, "mono_guards??", combs_or_liftingN, false), e_fun_weightN)), |
565 (0.1667, (((128, mashN), vampire_tff0, "poly_tags??", combs_or_liftingN, false), e_sym_offset_weightN)), |
565 (0.15, (((128, mashN), vampire_tff0, "poly_tags??", combs_or_liftingN, false), e_sym_offset_weightN)), |
566 (0.1666, (((91, mepoN), vampire_tff0, "mono_native", combsN, false), e_autoN)), |
566 (0.15, (((91, mepoN), vampire_tff0, "mono_native", combsN, false), e_autoN)), |
567 (0.1667, (((64, mashN), vampire_tff0, "mono_tags??", liftingN, false), e_fun_weightN)), |
567 (0.15, (((64, mashN), vampire_tff0, "mono_tags??", liftingN, false), e_fun_weightN)), |
568 (0.1667, (((1000, meshN), vampire_tff0, "poly_guards??", combs_or_liftingN, false), e_sym_offset_weightN)), |
568 (0.15, (((1000, meshN), vampire_tff0, "poly_guards??", combs_or_liftingN, false), e_sym_offset_weightN)), |
569 (0.1666, (((256, mepoN), vampire_tff0, "mono_native", combs_or_liftingN, false), e_fun_weightN))] |
569 (0.20, (((256, mepoN), vampire_tff0, "mono_native", combs_or_liftingN, false), e_fun_weightN))] |
570 else |
570 else |
571 [(0.333, (((150, mepoN), FOF, "poly_guards??", combs_or_liftingN, false), sosN)), |
571 [(0.333, (((150, mepoN), FOF, "poly_guards??", combs_or_liftingN, false), sosN)), |
572 (0.333, (((500, meshN), FOF, "mono_tags??", combs_or_liftingN, false), sosN)), |
572 (0.333, (((500, meshN), FOF, "mono_tags??", combs_or_liftingN, false), sosN)), |
573 (0.334, (((50, mashN), FOF, "mono_guards??", combs_or_liftingN, false), no_sosN))]) |
573 (0.334, (((50, mashN), FOF, "mono_guards??", combs_or_liftingN, false), no_sosN))]) |
574 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single |
574 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single |