use results of relevance-filter to determine additional clauses;
authorimmler@in.tum.de
Mon Jun 22 17:07:09 2009 +0200 (2009-06-22)
changeset 3175219a5f1c8a844
parent 31751 fda2cf4fef58
child 31753 a61475260e47
use results of relevance-filter to determine additional clauses;
(needed for minimize to be able to prove the same problems as sledgehammer)
src/HOL/Tools/atp_manager.ML
src/HOL/Tools/atp_minimal.ML
src/HOL/Tools/atp_wrapper.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/atp_manager.ML	Mon Jun 22 17:07:08 2009 +0200
     1.2 +++ b/src/HOL/Tools/atp_manager.ML	Mon Jun 22 17:07:09 2009 +0200
     1.3 @@ -20,9 +20,9 @@
     1.4    val info: unit -> unit
     1.5    val messages: int option -> unit
     1.6    type prover = int -> (thm * (string * int)) list option ->
     1.7 -    (int Symtab.table * bool Symtab.table) option -> string -> int ->
     1.8 +    (thm * (string * int)) list option -> string -> int ->
     1.9      Proof.context * (thm list * thm) ->
    1.10 -    bool * string * string * string vector * (int Symtab.table * bool Symtab.table)
    1.11 +    bool * string * string * string vector * (thm * (string * int)) list
    1.12    val add_prover: string -> prover -> theory -> theory
    1.13    val print_provers: theory -> unit
    1.14    val get_prover: string -> theory -> prover option
    1.15 @@ -292,9 +292,9 @@
    1.16  (* named provers *)
    1.17  
    1.18  type prover = int -> (thm * (string * int)) list option ->
    1.19 -  (int Symtab.table * bool Symtab.table) option -> string -> int ->
    1.20 +  (thm * (string * int)) list option -> string -> int ->
    1.21    Proof.context * (thm list * thm) ->
    1.22 -  bool * string * string * string vector * (int Symtab.table * bool Symtab.table)
    1.23 +  bool * string * string * string vector * (thm * (string * int)) list
    1.24  
    1.25  fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
    1.26  
     2.1 --- a/src/HOL/Tools/atp_minimal.ML	Mon Jun 22 17:07:08 2009 +0200
     2.2 +++ b/src/HOL/Tools/atp_minimal.ML	Mon Jun 22 17:07:09 2009 +0200
     2.3 @@ -83,9 +83,9 @@
     2.4     ("# Cannot determine problem status within resource limit", Timeout),
     2.5     ("Error", Error)]
     2.6  
     2.7 -fun produce_answer (success, message, result_string, thm_name_vec, const_counts) =
     2.8 +fun produce_answer (success, message, result_string, thm_name_vec, filtered) =
     2.9    if success then
    2.10 -    (Success (Vector.foldr op:: [] thm_name_vec, const_counts), result_string)
    2.11 +    (Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string)
    2.12    else
    2.13      let
    2.14        val failure = failure_strings |> get_first (fn (s, t) =>
    2.15 @@ -100,7 +100,7 @@
    2.16  
    2.17  (* wrapper for calling external prover *)
    2.18  
    2.19 -fun sh_test_thms prover prover_name time_limit subgoalno state counts name_thms_pairs =
    2.20 +fun sh_test_thms prover prover_name time_limit subgoalno state filtered name_thms_pairs =
    2.21    let
    2.22      val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ")
    2.23      val name_thm_pairs =
    2.24 @@ -109,7 +109,7 @@
    2.25      val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
    2.26      val (result, proof) =
    2.27        produce_answer
    2.28 -        (prover time_limit (SOME axclauses) counts prover_name subgoalno (Proof.get_goal state))
    2.29 +        (prover time_limit (SOME axclauses) filtered prover_name subgoalno (Proof.get_goal state))
    2.30      val _ = println (string_of_result result)
    2.31      val _ = debug proof
    2.32    in
    2.33 @@ -127,11 +127,12 @@
    2.34      val _ = debug_fn (fn () => app (fn (n, tl) =>
    2.35          (debug n; app (fn t => debug ("  " ^ Display.string_of_thm t)) tl)) name_thms_pairs)
    2.36      val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state
    2.37 -    fun test_thms counts thms = case test_thms_fun counts thms of (Success _, _) => true | _ => false
    2.38 +    fun test_thms filtered thms =
    2.39 +      case test_thms_fun filtered thms of (Success _, _) => true | _ => false
    2.40    in
    2.41      (* try prove first to check result and get used theorems *)
    2.42      (case test_thms_fun NONE name_thms_pairs of
    2.43 -      (Success (used, const_counts), _) =>
    2.44 +      (Success (used, filtered), _) =>
    2.45          let
    2.46            val ordered_used = order_unique used
    2.47            val to_use =
    2.48 @@ -139,7 +140,7 @@
    2.49                filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
    2.50              else
    2.51                name_thms_pairs
    2.52 -          val min_thms = (minimal (test_thms (SOME const_counts)) to_use)
    2.53 +          val min_thms = (minimal (test_thms (SOME filtered)) to_use)
    2.54            val min_names = order_unique (map fst min_thms)
    2.55            val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems")
    2.56            val _ = debug_fn (fn () => print_names min_thms)
     3.1 --- a/src/HOL/Tools/atp_wrapper.ML	Mon Jun 22 17:07:08 2009 +0200
     3.2 +++ b/src/HOL/Tools/atp_wrapper.ML	Mon Jun 22 17:07:09 2009 +0200
     3.3 @@ -41,7 +41,7 @@
     3.4  (* basic template *)
     3.5  
     3.6  fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer
     3.7 -  timeout axiom_clauses const_counts name subgoalno goal =
     3.8 +  timeout axiom_clauses filtered_clauses name subgoalno goal =
     3.9    let
    3.10      (* path to unique problem file *)
    3.11      val destdir' = ! destdir
    3.12 @@ -62,24 +62,20 @@
    3.13        handle THM ("assume: variables", _, _) =>
    3.14          error "Sledgehammer: Goal contains type variables (TVars)"
    3.15      val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) goal_cls
    3.16 +    val the_filtered_clauses =
    3.17 +      case filtered_clauses of
    3.18 +          NONE => relevance_filter goal goal_cls
    3.19 +        | SOME fcls => fcls
    3.20      val the_axiom_clauses =
    3.21        case axiom_clauses of
    3.22 -          NONE => relevance_filter goal goal_cls
    3.23 +          NONE => the_filtered_clauses
    3.24          | SOME axcls => axcls
    3.25 -    val (thm_names, clauses) = preparer goal_cls chain_ths the_axiom_clauses thy
    3.26 -    val the_const_counts = case const_counts of
    3.27 -      NONE =>
    3.28 -        ResHolClause.count_constants(
    3.29 -          case axiom_clauses of
    3.30 -            NONE => clauses
    3.31 -            | SOME axcls => #2(preparer goal_cls chain_ths (relevance_filter goal goal_cls) thy)
    3.32 -          )
    3.33 -      | SOME ccs => ccs
    3.34 +    val (thm_names, clauses) = preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
    3.35  
    3.36      (* write out problem file and call prover *)
    3.37      val probfile = prob_pathname subgoalno
    3.38      val fname = File.platform_path probfile
    3.39 -    val _ = writer fname the_const_counts clauses
    3.40 +    val _ = writer fname clauses
    3.41      val cmdline =
    3.42        if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args
    3.43        else error ("Bad executable: " ^ Path.implode cmd)
    3.44 @@ -101,7 +97,7 @@
    3.45        else if rc <> 0 then "External prover failed: " ^ proof
    3.46        else "Try this command: " ^ produce_answer name (proof, thm_names, ctxt, th, subgoalno)
    3.47      val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
    3.48 -  in (success, message, proof, thm_names, the_const_counts) end;
    3.49 +  in (success, message, proof, thm_names, the_filtered_clauses) end;
    3.50  
    3.51  
    3.52  
    3.53 @@ -109,7 +105,7 @@
    3.54  
    3.55  (* generic TPTP-based provers *)
    3.56  
    3.57 -fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses ccs name n goal =
    3.58 +fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses fcls name n goal =
    3.59    external_prover
    3.60    (ResAtp.get_relevant max_new theory_const)
    3.61    (ResAtp.prepare_clauses false)
    3.62 @@ -117,7 +113,7 @@
    3.63    command
    3.64    ResReconstruct.find_failure
    3.65    (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
    3.66 -  timeout ax_clauses ccs name n goal;
    3.67 +  timeout ax_clauses fcls name n goal;
    3.68  
    3.69  (*arbitrary ATP with TPTP input/output and problemfile as last argument*)
    3.70  fun tptp_prover_opts max_new theory_const =
    3.71 @@ -174,7 +170,7 @@
    3.72  
    3.73  (* SPASS *)
    3.74  
    3.75 -fun spass_opts max_new theory_const timeout ax_clauses ccs name n goal = external_prover
    3.76 +fun spass_opts max_new theory_const timeout ax_clauses fcls name n goal = external_prover
    3.77    (ResAtp.get_relevant max_new theory_const)
    3.78    (ResAtp.prepare_clauses true)
    3.79    ResHolClause.dfg_write_file
    3.80 @@ -182,7 +178,7 @@
    3.81      "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout)
    3.82    ResReconstruct.find_failure
    3.83    ResReconstruct.lemma_list_dfg
    3.84 -  timeout ax_clauses ccs name n goal;
    3.85 +  timeout ax_clauses fcls name n goal;
    3.86  
    3.87  val spass = spass_opts 40 true;
    3.88  
     4.1 --- a/src/HOL/Tools/res_atp.ML	Mon Jun 22 17:07:08 2009 +0200
     4.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Jun 22 17:07:09 2009 +0200
     4.3 @@ -9,6 +9,7 @@
     4.4    val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
     4.5      (thm * (string * int)) list
     4.6    val prepare_clauses : bool -> thm list -> thm list ->
     4.7 +    (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list ->
     4.8      (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list -> theory ->
     4.9      ResHolClause.axiom_name vector * (ResHolClause.clause list * ResHolClause.clause list *
    4.10      ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list)
    4.11 @@ -526,26 +527,30 @@
    4.12      relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
    4.13    end;
    4.14  
    4.15 -(* prepare for passing to writer *)
    4.16 -fun prepare_clauses dfg goal_cls chain_ths axcls thy =
    4.17 +(* prepare for passing to writer,
    4.18 +   create additional clauses based on the information from extra_cls *)
    4.19 +fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
    4.20    let
    4.21 -    val white_thms = filter check_named (map ResAxioms.pairname (if null chain_ths then whitelist else chain_ths))
    4.22 +    val white_thms =
    4.23 +      filter check_named (map ResAxioms.pairname (if null chain_ths then whitelist else chain_ths))
    4.24      val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
    4.25 -    val axcls = white_cls @ axcls
    4.26 -    val ccls = subtract_cls goal_cls axcls
    4.27 +    val extra_cls = white_cls @ extra_cls
    4.28 +    val ccls = subtract_cls goal_cls extra_cls
    4.29      val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
    4.30      val ccltms = map prop_of ccls
    4.31 -    and axtms = map (prop_of o #1) axcls
    4.32 +    and axtms = map (prop_of o #1) extra_cls
    4.33      val subs = tfree_classes_of_terms ccltms
    4.34      and supers = tvar_classes_of_terms axtms
    4.35      and tycons = type_consts_of_terms thy (ccltms@axtms)
    4.36      (*TFrees in conjecture clauses; TVars in axiom clauses*)
    4.37 -    val (clnames, (conjectures, axiom_clauses, helper_clauses)) =
    4.38 -      ResHolClause.prepare_clauses dfg thy (isFO thy goal_cls) ccls axcls []
    4.39 +    val conjectures = ResHolClause.make_conjecture_clauses dfg thy ccls
    4.40 +    val (clnames,axiom_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy axcls)
    4.41 +    val helper_clauses = ResHolClause.get_helper_clauses dfg thy (isFO thy goal_cls) (conjectures, extra_cls, [])
    4.42      val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
    4.43      val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
    4.44    in
    4.45 -    (Vector.fromList clnames, (conjectures, axiom_clauses, helper_clauses, classrel_clauses, arity_clauses))
    4.46 +    (Vector.fromList clnames,
    4.47 +      (conjectures, axiom_clauses, helper_clauses, classrel_clauses, arity_clauses))
    4.48    end
    4.49  
    4.50  end;
     5.1 --- a/src/HOL/Tools/res_hol_clause.ML	Mon Jun 22 17:07:08 2009 +0200
     5.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Mon Jun 22 17:07:09 2009 +0200
     5.3 @@ -28,13 +28,18 @@
     5.4    val strip_comb: combterm -> combterm * combterm list
     5.5    val literals_of_term: theory -> term -> literal list * typ list
     5.6    exception TOO_TRIVIAL
     5.7 -  val count_constants: clause list * clause list * clause list * 'a * 'b ->
     5.8 -    int Symtab.table * bool Symtab.table
     5.9 -  val prepare_clauses: bool -> theory -> bool -> thm list -> (thm * (axiom_name * clause_id)) list ->
    5.10 -    string list -> axiom_name list * (clause list * clause list * clause list)
    5.11 -  val tptp_write_file: string -> int Symtab.table * bool Symtab.table ->
    5.12 +  val make_conjecture_clauses:  bool -> theory -> thm list -> clause list (* dfg thy ccls *)
    5.13 +  val make_axiom_clauses: bool ->
    5.14 +       theory ->
    5.15 +       (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list (* dfg thy axcls *)
    5.16 +  val get_helper_clauses: bool ->
    5.17 +       theory ->
    5.18 +       bool ->
    5.19 +       clause list * (thm * (axiom_name * clause_id)) list * string list ->
    5.20 +       clause list
    5.21 +  val tptp_write_file: string ->
    5.22      clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
    5.23 -  val dfg_write_file: string -> int Symtab.table * bool Symtab.table ->
    5.24 +  val dfg_write_file: string -> 
    5.25      clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
    5.26  end
    5.27  
    5.28 @@ -403,10 +408,12 @@
    5.29  fun cnf_helper_thms thy =
    5.30    ResAxioms.cnf_rules_pairs thy o map ResAxioms.pairname
    5.31  
    5.32 -fun get_helper_clauses dfg thy isFO (conjectures, axclauses, user_lemmas) =
    5.33 +fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
    5.34    if isFO then []  (*first-order*)
    5.35    else
    5.36 -    let val ct0 = List.foldl count_clause init_counters conjectures
    5.37 +    let
    5.38 +        val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
    5.39 +        val ct0 = List.foldl count_clause init_counters conjectures
    5.40          val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
    5.41          fun needed c = valOf (Symtab.lookup ct c) > 0
    5.42          val IK = if needed "c_COMBI" orelse needed "c_COMBK"
    5.43 @@ -462,20 +469,12 @@
    5.44       in (const_min_arity, const_needs_hBOOL) end
    5.45    else (Symtab.empty, Symtab.empty);
    5.46  
    5.47 -
    5.48 -fun prepare_clauses dfg thy isFO thms ax_tuples user_lemmas =
    5.49 -  let
    5.50 -    val conjectures = make_conjecture_clauses dfg thy thms
    5.51 -    val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses dfg thy ax_tuples)
    5.52 -    val helper_clauses = get_helper_clauses dfg thy isFO (conjectures, axclauses, user_lemmas)
    5.53 -  in
    5.54 -    (clnames, (conjectures, axclauses, helper_clauses))
    5.55 -  end
    5.56 -
    5.57  (* tptp format *)
    5.58  
    5.59 -fun tptp_write_file filename const_counts (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) =
    5.60 +fun tptp_write_file filename clauses =
    5.61    let
    5.62 +    val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
    5.63 +    val const_counts = count_constants clauses
    5.64      val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp const_counts) conjectures)
    5.65      val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss)
    5.66      val out = TextIO.openOut filename
    5.67 @@ -492,8 +491,10 @@
    5.68  
    5.69  (* dfg format *)
    5.70  
    5.71 -fun dfg_write_file filename const_counts (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) =
    5.72 +fun dfg_write_file filename clauses =
    5.73    let
    5.74 +    val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
    5.75 +    val const_counts = count_constants clauses
    5.76      val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg const_counts) conjectures)
    5.77      and probname = Path.implode (Path.base (Path.explode filename))
    5.78      val axstrs = map (#1 o (clause2dfg const_counts)) axclauses