src/HOL/Tools/res_atp.ML
changeset 22865 da52c2bd66ae
parent 22824 51bb2f6ecc4a
child 22989 3bcbe6187027
equal deleted inserted replaced
22864:e2511e6e5cbb 22865:da52c2bd66ae
     3     Copyright 2004 University of Cambridge
     3     Copyright 2004 University of Cambridge
     4 
     4 
     5 ATPs with TPTP format input.
     5 ATPs with TPTP format input.
     6 *)
     6 *)
     7 
     7 
     8 (*Currently unused, during debugging*)
       
     9 signature RES_ATP =
     8 signature RES_ATP =
    10 sig
     9 sig
    11   val prover: string ref
    10   val prover: string ref
    12   val custom_spass: string list ref
    11   val custom_spass: string list ref
    13   val destdir: string ref
    12   val destdir: string ref
    46   val rm_atpset : unit -> unit
    45   val rm_atpset : unit -> unit
    47   val rm_clasimp : unit -> unit
    46   val rm_clasimp : unit -> unit
    48   val is_fol_thms : thm list -> bool
    47   val is_fol_thms : thm list -> bool
    49 end;
    48 end;
    50 
    49 
    51 structure ResAtp =
    50 structure ResAtp: RES_ATP =
    52 struct
    51 struct
    53 
    52 
    54 fun timestamp s = Output.debug (fn () => ("At " ^ Time.toString (Time.now()) ^ ": " ^ s));
    53 fun timestamp s = Output.debug (fn () => ("At " ^ Time.toString (Time.now()) ^ ": " ^ s));
    55 
    54 
    56 (********************************************************************)
    55 (********************************************************************)
   506 fun get_relevant_clauses thy cls_thms white_cls goals =
   505 fun get_relevant_clauses thy cls_thms white_cls goals =
   507   white_cls @ (ReduceAxiomsN.relevance_filter thy cls_thms goals);
   506   white_cls @ (ReduceAxiomsN.relevance_filter thy cls_thms goals);
   508 
   507 
   509 fun all_valid_thms ctxt =
   508 fun all_valid_thms ctxt =
   510   let
   509   let
   511     val banned_tab = foldl setinsert Symtab.empty (!blacklist) 
   510     val banned_tab = foldl setinsert Symtab.empty (!blacklist)
   512     fun blacklisted s = !run_blacklist_filter andalso
   511     fun blacklisted s = !run_blacklist_filter andalso
   513                         (isSome (Symtab.lookup banned_tab s) orelse is_package_def s)
   512                         (isSome (Symtab.lookup banned_tab s) orelse is_package_def s)
   514 
   513 
   515     fun extern_valid space (name, ths) =
   514     fun extern_valid space (name, ths) =
   516       let
   515       let
   710         val logic = case mode of
   709         val logic = case mode of
   711                             Auto => problem_logic_goals [goal_tms]
   710                             Auto => problem_logic_goals [goal_tms]
   712                           | Fol => FOL
   711                           | Fol => FOL
   713                           | Hol => HOL
   712                           | Hol => HOL
   714         val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
   713         val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
   715         val cla_simp_atp_clauses = included_thms 
   714         val cla_simp_atp_clauses = included_thms
   716                                      |> ResAxioms.cnf_rules_pairs |> make_unique
   715                                      |> ResAxioms.cnf_rules_pairs |> make_unique
   717                                      |> restrict_to_logic thy logic
   716                                      |> restrict_to_logic thy logic
   718                                      |> remove_unwanted_clauses
   717                                      |> remove_unwanted_clauses
   719         val user_cls = ResAxioms.cnf_rules_pairs user_rules
   718         val user_cls = ResAxioms.cnf_rules_pairs user_rules
   720         val axclauses = make_unique (get_relevant_clauses thy cla_simp_atp_clauses user_cls goal_tms)
   719         val axclauses = make_unique (get_relevant_clauses thy cla_simp_atp_clauses user_cls goal_tms)
   811 fun write_problem_files probfile (ctxt,th)  =
   810 fun write_problem_files probfile (ctxt,th)  =
   812   let val goals = Thm.prems_of th
   811   let val goals = Thm.prems_of th
   813       val _ = Output.debug (fn () => "number of subgoals = " ^ Int.toString (length goals))
   812       val _ = Output.debug (fn () => "number of subgoals = " ^ Int.toString (length goals))
   814       val thy = ProofContext.theory_of ctxt
   813       val thy = ProofContext.theory_of ctxt
   815       fun get_neg_subgoals [] _ = []
   814       fun get_neg_subgoals [] _ = []
   816         | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) :: 
   815         | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) ::
   817                                          get_neg_subgoals gls (n+1)
   816                                          get_neg_subgoals gls (n+1)
   818       val goal_cls = get_neg_subgoals goals 1
   817       val goal_cls = get_neg_subgoals goals 1
   819       val logic = case !linkup_logic_mode of
   818       val logic = case !linkup_logic_mode of
   820                 Auto => problem_logic_goals (map ((map prop_of)) goal_cls)
   819                 Auto => problem_logic_goals (map ((map prop_of)) goal_cls)
   821               | Fol => FOL
   820               | Fol => FOL
   900          let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix
   899          let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix
   901                             else prob_pathname
   900                             else prob_pathname
   902          in ignore (write_problem_files probfile (ctxt,th)) end);
   901          in ignore (write_problem_files probfile (ctxt,th)) end);
   903 
   902 
   904 
   903 
   905 (** the Isar toplevel hook **)
   904 (** the Isar toplevel command **)
   906 
   905 
   907 fun invoke_atp_ml (ctxt, goal) =
   906 fun sledgehammer state =
   908   let val thy = ProofContext.theory_of ctxt;
   907   let
       
   908     val (ctxt, (_, goal)) = Proof.get_goal (Toplevel.proof_of state);
       
   909     val thy = ProofContext.theory_of ctxt;
   909   in
   910   in
   910     Output.debug (fn () => "subgoals in isar_atp:\n" ^
   911     Output.debug (fn () => "subgoals in isar_atp:\n" ^
   911                   Pretty.string_of (ProofContext.pretty_term ctxt
   912                   Pretty.string_of (ProofContext.pretty_term ctxt
   912                     (Logic.mk_conjunction_list (Thm.prems_of goal))));
   913                     (Logic.mk_conjunction_list (Thm.prems_of goal))));
   913     Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
   914     Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
   914     inc hook_count;
   915     inc hook_count;
   915     Output.debug (fn () => "in hook for time: " ^ Int.toString (!hook_count));
   916     Output.debug (fn () => "in hook for time: " ^ Int.toString (!hook_count));
   916     ResClause.init thy;
   917     ResClause.init thy;
   917     ResHolClause.init thy;
   918     ResHolClause.init thy;
   918     if !time_limit > 0 then isar_atp (ctxt, goal)
   919     if !time_limit > 0 then isar_atp (ctxt, goal)
   919     else (warning ("Writing problem file only: " ^ !problem_name); 
   920     else (warning ("Writing problem file only: " ^ !problem_name);
   920           isar_atp_writeonly (ctxt, goal))
   921           isar_atp_writeonly (ctxt, goal))
   921   end;
   922   end;
   922 
   923 
   923 val invoke_atp = Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep
   924 val _ = OuterSyntax.add_parsers
   924  (fn state =>
   925   [OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag
   925   let val (ctxt, (_, goal)) = Proof.get_goal (Toplevel.proof_of state)
   926     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer))];
   926   in  invoke_atp_ml (ctxt, goal)  end);
       
   927 
       
   928 val call_atpP =
       
   929   OuterSyntax.command
       
   930     "ProofGeneral.call_atp"
       
   931     "call automatic theorem provers"
       
   932     OuterKeyword.diag
       
   933     (Scan.succeed invoke_atp);
       
   934 
       
   935 val _ = OuterSyntax.add_parsers [call_atpP];
       
   936 
   927 
   937 end;
   928 end;