24 datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm, |
24 datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm, |
25 kind: ResClause.kind,literals: literal list, ctypes_sorts: typ list} |
25 kind: ResClause.kind,literals: literal list, ctypes_sorts: typ list} |
26 val strip_comb: combterm -> combterm * combterm list |
26 val strip_comb: combterm -> combterm * combterm list |
27 val literals_of_term: theory -> term -> literal list * typ list |
27 val literals_of_term: theory -> term -> literal list * typ list |
28 exception TOO_TRIVIAL |
28 exception TOO_TRIVIAL |
29 val make_conjecture_clauses: bool -> theory -> thm list -> clause list (* dfg thy ccls *) |
29 val make_conjecture_clauses: bool -> theory -> thm list -> clause list |
30 val make_axiom_clauses: bool -> |
30 val make_axiom_clauses: bool -> |
31 theory -> |
31 theory -> |
32 (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list (* dfg thy axcls *) |
32 (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list |
33 val get_helper_clauses: bool -> |
33 val get_helper_clauses: bool -> |
34 theory -> |
34 theory -> |
35 bool -> |
35 bool -> |
36 clause list * (thm * (axiom_name * clause_id)) list * string list -> |
36 clause list * (thm * (axiom_name * clause_id)) list * string list -> |
37 clause list |
37 clause list |
38 val tptp_write_file: bool -> string -> |
38 val tptp_write_file: bool -> Path.T -> |
39 clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit |
39 clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit |
40 val dfg_write_file: bool -> string -> |
40 val dfg_write_file: bool -> Path.T -> |
41 clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit |
41 clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit |
42 end |
42 end |
43 |
43 |
44 structure ResHolClause: RES_HOL_CLAUSE = |
44 structure ResHolClause: RES_HOL_CLAUSE = |
45 struct |
45 struct |
467 in (const_min_arity, const_needs_hBOOL) end |
467 in (const_min_arity, const_needs_hBOOL) end |
468 else (Symtab.empty, Symtab.empty); |
468 else (Symtab.empty, Symtab.empty); |
469 |
469 |
470 (* tptp format *) |
470 (* tptp format *) |
471 |
471 |
472 fun tptp_write_file t_full filename clauses = |
472 fun tptp_write_file t_full file clauses = |
473 let |
473 let |
474 val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses |
474 val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses |
475 val (cma, cnh) = count_constants clauses |
475 val (cma, cnh) = count_constants clauses |
476 val params = (t_full, cma, cnh) |
476 val params = (t_full, cma, cnh) |
477 val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures) |
477 val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures) |
478 val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss) |
478 val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss) |
479 val out = TextIO.openOut filename |
479 in |
480 in |
480 File.write_list file ( |
481 List.app (curry TextIO.output out o #1 o (clause2tptp params)) axclauses; |
481 map (#1 o (clause2tptp params)) axclauses @ |
482 RC.writeln_strs out tfree_clss; |
482 tfree_clss @ |
483 RC.writeln_strs out tptp_clss; |
483 tptp_clss @ |
484 List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses; |
484 map RC.tptp_classrelClause classrel_clauses @ |
485 List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses; |
485 map RC.tptp_arity_clause arity_clauses @ |
486 List.app (curry TextIO.output out o #1 o (clause2tptp params)) helper_clauses; |
486 map (#1 o (clause2tptp params)) helper_clauses) |
487 TextIO.closeOut out |
|
488 end; |
487 end; |
489 |
488 |
490 |
489 |
491 (* dfg format *) |
490 (* dfg format *) |
492 |
491 |
493 fun dfg_write_file t_full filename clauses = |
492 fun dfg_write_file t_full file clauses = |
494 let |
493 let |
495 val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses |
494 val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses |
496 val (cma, cnh) = count_constants clauses |
495 val (cma, cnh) = count_constants clauses |
497 val params = (t_full, cma, cnh) |
496 val params = (t_full, cma, cnh) |
498 val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures) |
497 val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures) |
499 and probname = Path.implode (Path.base (Path.explode filename)) |
498 and probname = Path.implode (Path.base file) |
500 val axstrs = map (#1 o (clause2dfg params)) axclauses |
499 val axstrs = map (#1 o (clause2dfg params)) axclauses |
501 val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss) |
500 val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss) |
502 val out = TextIO.openOut filename |
|
503 val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses |
501 val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses |
504 val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses |
502 val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses |
505 and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses |
503 and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses |
506 in |
504 in |
507 TextIO.output (out, RC.string_of_start probname); |
505 File.write_list file ( |
508 TextIO.output (out, RC.string_of_descrip probname); |
506 RC.string_of_start probname :: |
509 TextIO.output (out, RC.string_of_symbols |
507 RC.string_of_descrip probname :: |
510 (RC.string_of_funcs funcs) |
508 RC.string_of_symbols (RC.string_of_funcs funcs) |
511 (RC.string_of_preds (cl_preds @ ty_preds))); |
509 (RC.string_of_preds (cl_preds @ ty_preds)) :: |
512 TextIO.output (out, "list_of_clauses(axioms,cnf).\n"); |
510 "list_of_clauses(axioms,cnf).\n" :: |
513 RC.writeln_strs out axstrs; |
511 axstrs @ |
514 List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses; |
512 map RC.dfg_classrelClause classrel_clauses @ |
515 List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses; |
513 map RC.dfg_arity_clause arity_clauses @ |
516 RC.writeln_strs out helper_clauses_strs; |
514 helper_clauses_strs @ |
517 TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"); |
515 ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @ |
518 RC.writeln_strs out tfree_clss; |
516 tfree_clss @ |
519 RC.writeln_strs out dfg_clss; |
517 dfg_clss @ |
520 TextIO.output (out, "end_of_list.\n\n"); |
518 ["end_of_list.\n\n", |
521 (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*) |
519 (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*) |
522 TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n"); |
520 "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n", |
523 TextIO.output (out, "end_problem.\n"); |
521 "end_problem.\n"]) |
524 TextIO.closeOut out |
|
525 end; |
522 end; |
526 |
523 |
527 end |
524 end |