105 val lines_for_atp_problem : atp_format -> string problem -> string list |
105 val lines_for_atp_problem : atp_format -> string problem -> string list |
106 val ensure_cnf_problem : |
106 val ensure_cnf_problem : |
107 (string * string) problem -> (string * string) problem |
107 (string * string) problem -> (string * string) problem |
108 val filter_cnf_ueq_problem : |
108 val filter_cnf_ueq_problem : |
109 (string * string) problem -> (string * string) problem |
109 (string * string) problem -> (string * string) problem |
110 val declare_undeclared_syms_in_atp_problem : |
110 val declared_syms_in_problem : (string * ''a) problem -> (string * ''a) list |
111 string -> string -> (string * string) problem -> (string * string) problem |
|
112 val nice_atp_problem : |
111 val nice_atp_problem : |
113 bool -> ('a * (string * string) problem_line list) list |
112 bool -> ('a * (string * string) problem_line list) list |
114 -> ('a * string problem_line list) list |
113 -> ('a * string problem_line list) list |
115 * (string Symtab.table * string Symtab.table) option |
114 * (string Symtab.table * string Symtab.table) option |
116 end; |
115 end; |
611 in if length conjs = 1 andalso conjs <> lines then problem else [] end) |
610 in if length conjs = 1 andalso conjs <> lines then problem else [] end) |
612 |
611 |
613 |
612 |
614 (** Symbol declarations **) |
613 (** Symbol declarations **) |
615 |
614 |
616 (* TFF allows implicit declarations of types, function symbols, and predicate |
|
617 symbols (with "$i" as the type of individuals), but some provers (e.g., |
|
618 SNARK) require explicit declarations. The situation is similar for THF. *) |
|
619 fun default_type pred_sym = |
|
620 let |
|
621 fun typ 0 = if pred_sym then bool_atype else individual_atype |
|
622 | typ ary = AFun (individual_atype, typ (ary - 1)) |
|
623 in typ end |
|
624 |
|
625 fun add_declared_syms_in_problem_line (Decl (_, sym, _)) = insert (op =) sym |
615 fun add_declared_syms_in_problem_line (Decl (_, sym, _)) = insert (op =) sym |
626 | add_declared_syms_in_problem_line _ = I |
616 | add_declared_syms_in_problem_line _ = I |
627 fun declared_syms_in_problem problem = |
617 fun declared_syms_in_problem problem = |
628 fold (fold add_declared_syms_in_problem_line o snd) problem [] |
618 fold (fold add_declared_syms_in_problem_line o snd) problem [] |
629 |
|
630 fun nary_type_constr_type n = |
|
631 funpow n (curry AFun atype_of_types) atype_of_types |
|
632 |
|
633 fun undeclared_syms_in_problem declared problem = |
|
634 let |
|
635 fun do_sym name ty = |
|
636 if member (op =) declared name then I else AList.default (op =) (name, ty) |
|
637 fun do_type (AType (name as (s, _), tys)) = |
|
638 is_tptp_user_symbol s |
|
639 ? do_sym name (fn _ => nary_type_constr_type (length tys)) |
|
640 #> fold do_type tys |
|
641 | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2 |
|
642 | do_type (ATyAbs (_, ty)) = do_type ty |
|
643 fun do_term pred_sym (ATerm (name as (s, _), tms)) = |
|
644 is_tptp_user_symbol s |
|
645 ? do_sym name (fn _ => default_type pred_sym (length tms)) |
|
646 #> fold (do_term false) tms |
|
647 | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm |
|
648 fun do_formula (AQuant (_, xs, phi)) = |
|
649 fold do_type (map_filter snd xs) #> do_formula phi |
|
650 | do_formula (AConn (_, phis)) = fold do_formula phis |
|
651 | do_formula (AAtom tm) = do_term true tm |
|
652 fun do_problem_line (Decl (_, _, ty)) = do_type ty |
|
653 | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi |
|
654 in |
|
655 fold (fold do_problem_line o snd) problem [] |
|
656 |> filter_out (is_built_in_tptp_symbol o fst o fst) |
|
657 end |
|
658 |
|
659 fun declare_undeclared_syms_in_atp_problem prefix heading problem = |
|
660 let |
|
661 fun decl_line (x as (s, _), ty) = Decl (prefix ^ s, x, ty ()) |
|
662 val declared = problem |> declared_syms_in_problem |
|
663 val decls = |
|
664 problem |> undeclared_syms_in_problem declared |
|
665 |> sort_wrt (fst o fst) |
|
666 |> map decl_line |
|
667 in (heading, decls) :: problem end |
|
668 |
619 |
669 (** Nice names **) |
620 (** Nice names **) |
670 |
621 |
671 fun empty_name_pool readable_names = |
622 fun empty_name_pool readable_names = |
672 if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE |
623 if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE |