690 |> pair genuine_means_genuine |
690 |> pair genuine_means_genuine |
691 end |
691 end |
692 fun solve_any_problem (found_really_genuine, max_potential, max_genuine, |
692 fun solve_any_problem (found_really_genuine, max_potential, max_genuine, |
693 donno) first_time problems = |
693 donno) first_time problems = |
694 let |
694 let |
|
695 val kodkod_scala = Config.get ctxt KK.kodkod_scala |
695 val max_potential = Int.max (0, max_potential) |
696 val max_potential = Int.max (0, max_potential) |
696 val max_genuine = Int.max (0, max_genuine) |
697 val max_genuine = Int.max (0, max_genuine) |
697 fun print_and_check genuine (j, bounds) = |
698 fun print_and_check genuine (j, bounds) = |
698 print_and_check_model genuine bounds (snd (nth problems j)) |
699 print_and_check_model genuine bounds (snd (nth problems j)) |
699 val max_solutions = max_potential + max_genuine |
700 val max_solutions = max_potential + max_genuine |
700 |> not incremental ? Integer.min 1 |
701 |> not incremental ? Integer.min 1 |
701 in |
702 in |
702 if max_solutions <= 0 then |
703 if max_solutions <= 0 then |
703 (found_really_genuine, 0, 0, donno) |
704 (found_really_genuine, 0, 0, donno) |
704 else |
705 else |
705 case KK.solve_any_problem debug overlord deadline max_threads |
706 case KK.solve_any_problem kodkod_scala debug overlord deadline max_threads |
706 max_solutions (map fst problems) of |
707 max_solutions (map fst problems) of |
707 KK.Normal ([], unsat_js, s) => |
708 KK.Normal ([], unsat_js, s) => |
708 (update_checked_problems problems unsat_js; show_kodkod_warning s; |
709 (update_checked_problems problems unsat_js; show_kodkod_warning s; |
709 (found_really_genuine, max_potential, max_genuine, donno)) |
710 (found_really_genuine, max_potential, max_genuine, donno)) |
710 | KK.Normal (sat_ps, unsat_js, s) => |
711 | KK.Normal (sat_ps, unsat_js, s) => |