equal
deleted
inserted
replaced
572 else |
572 else |
573 let |
573 let |
574 (* use the first ML solver (to avoid startup overhead) *) |
574 (* use the first ML solver (to avoid startup overhead) *) |
575 val (ml_solvers, nonml_solvers) = |
575 val (ml_solvers, nonml_solvers) = |
576 SatSolver.get_solvers () |
576 SatSolver.get_solvers () |
577 |> List.partition (member (op =) ["dptsat", "dpll_p", "dpll"] o fst) |
577 |> List.partition (member (op =) ["dptsat", "dpll_p"] o fst) |
578 val res = |
578 val res = |
579 if null nonml_solvers then |
579 if null nonml_solvers then |
580 TimeLimit.timeLimit tac_timeout (snd (hd ml_solvers)) prop |
580 TimeLimit.timeLimit tac_timeout (snd (hd ml_solvers)) prop |
581 else |
581 else |
582 TimeLimit.timeLimit ml_solver_timeout (snd (hd ml_solvers)) prop |
582 TimeLimit.timeLimit ml_solver_timeout (snd (hd ml_solvers)) prop |