--- a/src/HOL/Tools/ATP/atp_problem.ML Fri Mar 25 13:52:23 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Fri Mar 25 13:52:23 2022 +0100
@@ -128,40 +128,31 @@
val bool_atype : (string * string) atp_type
val individual_atype : (string * string) atp_type
val mk_anot : ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'c, 'd) atp_formula
- val mk_aconn :
- atp_connective -> ('a, 'b, 'c, 'd) atp_formula
- -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'c, 'd) atp_formula
+ val mk_aconn : atp_connective -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'c, 'd) atp_formula ->
+ ('a, 'b, 'c, 'd) atp_formula
val mk_app : (string, 'a) atp_term -> (string, 'a) atp_term -> (string, 'a) atp_term
val mk_apps : (string, 'a) atp_term -> (string, 'a) atp_term list -> (string, 'a) atp_term
val mk_simple_aterm: 'a -> ('a, 'b) atp_term
- val aconn_fold :
- bool option -> (bool option -> 'a -> 'b -> 'b) -> atp_connective * 'a list
- -> 'b -> 'b
- val aconn_map :
- bool option -> (bool option -> 'a -> ('b, 'c, 'd, 'e) atp_formula)
- -> atp_connective * 'a list -> ('b, 'c, 'd, 'e) atp_formula
- val formula_fold :
- bool option -> (bool option -> 'c -> 'e -> 'e)
- -> ('a, 'b, 'c, 'd) atp_formula -> 'e -> 'e
- val formula_map :
- ('c -> 'e) -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'e, 'd) atp_formula
+ val aconn_fold : bool option -> (bool option -> 'a -> 'b -> 'b) -> atp_connective * 'a list ->
+ 'b -> 'b
+ val aconn_map : bool option -> (bool option -> 'a -> ('b, 'c, 'd, 'e) atp_formula) ->
+ atp_connective * 'a list -> ('b, 'c, 'd, 'e) atp_formula
+ val formula_fold : bool option -> (bool option -> 'c -> 'e -> 'e) ->
+ ('a, 'b, 'c, 'd) atp_formula -> 'e -> 'e
+ val formula_map : ('c -> 'e) -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'e, 'd) atp_formula
val strip_atype : 'a atp_type -> 'a list * ('a atp_type list * 'a atp_type)
val is_format_higher_order : atp_format -> bool
val tptp_string_of_format : atp_format -> string
val tptp_string_of_role : atp_formula_role -> string
val tptp_string_of_line : atp_format -> string atp_problem_line -> string
- val lines_of_atp_problem :
- atp_format -> term_order -> (unit -> (string * int) list)
- -> string atp_problem -> string list
- val ensure_cnf_problem :
- (string * string) atp_problem -> (string * string) atp_problem
- val filter_cnf_ueq_problem :
- (string * string) atp_problem -> (string * string) atp_problem
+ val lines_of_atp_problem : atp_format -> (unit -> (string * int) list) -> string atp_problem ->
+ string list
+ val ensure_cnf_problem : (string * string) atp_problem -> (string * string) atp_problem
+ val filter_cnf_ueq_problem : (string * string) atp_problem -> (string * string) atp_problem
val declared_in_atp_problem : 'a atp_problem -> ('a list * 'a list) * 'a list
- val nice_atp_problem :
- bool -> atp_format -> ('a * (string * string) atp_problem_line list) list
- -> ('a * string atp_problem_line list) list
- * (string Symtab.table * string Symtab.table) option
+ val nice_atp_problem : bool -> atp_format ->
+ ('a * (string * string) atp_problem_line list) list ->
+ ('a * string atp_problem_line list) list * (string Symtab.table * string Symtab.table) option
end;
structure ATP_Problem : ATP_PROBLEM =
@@ -693,8 +684,14 @@
fun maybe_enclose bef aft "" = "% " ^ bef ^ aft
| maybe_enclose bef aft s = bef ^ s ^ aft
-fun dfg_lines poly {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem =
+fun dfg_lines poly ord_info problem =
let
+ (* hardcoded settings *)
+ val is_lpo = false
+ val gen_weights = true
+ val gen_prec = true
+ val gen_simp = false
+
val typ = string_of_type (DFG poly)
val term = dfg_string_of_term
fun spair (s, s') = "(" ^ s ^ ", " ^ s' ^ ")"
@@ -801,11 +798,11 @@
["end_problem.\n"]
end
-fun lines_of_atp_problem format ord ord_info problem =
+fun lines_of_atp_problem format ord_info problem =
"% This file was generated by Isabelle (most likely Sledgehammer)\n\
\% " ^ timestamp () ^ "\n" ::
(case format of
- DFG poly => dfg_lines poly ord ord_info
+ DFG poly => dfg_lines poly ord_info
| _ => tptp_lines format) problem