136 evals: term list, |
134 evals: term list, |
137 formats: (term option * int list) list, |
135 formats: (term option * int list) list, |
138 atomss: (typ option * string list) list, |
136 atomss: (typ option * string list) list, |
139 max_potential: int, |
137 max_potential: int, |
140 max_genuine: int, |
138 max_genuine: int, |
141 check_potential: bool, |
|
142 check_genuine: bool, |
|
143 batch_size: int, |
139 batch_size: int, |
144 expect: string} |
140 expect: string} |
145 |
141 |
146 val genuineN = "genuine" |
142 val genuineN = "genuine" |
147 val quasi_genuineN = "quasi_genuine" |
143 val quasi_genuineN = "quasi_genuine" |
232 overlord, spy, user_axioms, assms, whacks, merge_type_vars, |
228 overlord, spy, user_axioms, assms, whacks, merge_type_vars, |
233 binary_ints, destroy_constrs, specialize, star_linear_preds, |
229 binary_ints, destroy_constrs, specialize, star_linear_preds, |
234 total_consts, needs, peephole_optim, datatype_sym_break, |
230 total_consts, needs, peephole_optim, datatype_sym_break, |
235 kodkod_sym_break, tac_timeout, max_threads, show_types, show_skolems, |
231 kodkod_sym_break, tac_timeout, max_threads, show_types, show_skolems, |
236 show_consts, evals, formats, atomss, max_potential, max_genuine, |
232 show_consts, evals, formats, atomss, max_potential, max_genuine, |
237 check_potential, check_genuine, batch_size, ...} = params |
233 batch_size, ...} = params |
238 val outcome = Synchronized.var "Nitpick.outcome" (Queue.empty: string Queue.T) |
234 val outcome = Synchronized.var "Nitpick.outcome" (Queue.empty: string Queue.T) |
239 fun pprint print prt = |
235 fun pprint print prt = |
240 if mode = Auto_Try then |
236 if mode = Auto_Try then |
241 Synchronized.change outcome (Queue.enqueue (Pretty.string_of prt)) |
237 Synchronized.change outcome (Queue.enqueue (Pretty.string_of prt)) |
242 else |
238 else |
667 | pretties => [Pretty.brk 1, Pretty.str "for", Pretty.brk 1] @ pretties) @ |
663 | pretties => [Pretty.brk 1, Pretty.str "for", Pretty.brk 1] @ pretties) @ |
668 [Pretty.str ":", Pretty.fbrk])), |
664 [Pretty.str ":", Pretty.fbrk])), |
669 Pretty.indent indent_size reconstructed_model]); |
665 Pretty.indent indent_size reconstructed_model]); |
670 print_t (K "% SZS output end FiniteModel"); |
666 print_t (K "% SZS output end FiniteModel"); |
671 if genuine then |
667 if genuine then |
672 (if check_genuine then |
668 (if has_lonely_bool_var orig_t then |
673 case prove_hol_model scope tac_timeout free_names sel_names |
|
674 rel_table bounds (assms_prop ()) of |
|
675 SOME true => |
|
676 print ("Confirmation by \"auto\": The above " ^ |
|
677 das_wort_model ^ " is really genuine.") |
|
678 | SOME false => |
|
679 if genuine_means_genuine then |
|
680 error ("A supposedly genuine " ^ das_wort_model ^ " was \ |
|
681 \shown to be spurious by \"auto\".\nThis should never \ |
|
682 \happen.\nPlease send a bug report to blanchet\ |
|
683 \te@in.tum.de.") |
|
684 else |
|
685 print ("Refutation by \"auto\": The above " ^ |
|
686 das_wort_model ^ " is spurious.") |
|
687 | NONE => print "No confirmation by \"auto\"." |
|
688 else |
|
689 (); |
|
690 if has_lonely_bool_var orig_t then |
|
691 print "Hint: Maybe you forgot a colon after the lemma's name?" |
669 print "Hint: Maybe you forgot a colon after the lemma's name?" |
692 else if has_syntactic_sorts orig_t then |
670 else if has_syntactic_sorts orig_t then |
693 print "Hint: Maybe you forgot a type constraint?" |
671 print "Hint: Maybe you forgot a type constraint?" |
694 else |
672 else |
695 (); |
673 (); |
723 else |
701 else |
724 (); |
702 (); |
725 NONE) |
703 NONE) |
726 else |
704 else |
727 if not genuine then |
705 if not genuine then |
728 (Unsynchronized.inc met_potential; |
706 (Unsynchronized.inc met_potential; NONE) |
729 if check_potential then |
|
730 let |
|
731 val status = prove_hol_model scope tac_timeout free_names |
|
732 sel_names rel_table bounds |
|
733 (assms_prop ()) |
|
734 in |
|
735 (case status of |
|
736 SOME true => print ("Confirmation by \"auto\": The \ |
|
737 \above " ^ das_wort_model ^ |
|
738 " is genuine.") |
|
739 | SOME false => print ("Refutation by \"auto\": The above " ^ |
|
740 das_wort_model ^ " is spurious.") |
|
741 | NONE => print "No confirmation by \"auto\"."); |
|
742 status |
|
743 end |
|
744 else |
|
745 NONE) |
|
746 else |
707 else |
747 NONE) |
708 NONE) |
748 |> pair genuine_means_genuine |
709 |> pair genuine_means_genuine |
749 end |
710 end |
750 fun solve_any_problem (found_really_genuine, max_potential, max_genuine, |
711 fun solve_any_problem (found_really_genuine, max_potential, max_genuine, |