* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
authorpaulson
Mon Apr 07 15:37:27 2008 +0200 (2008-04-07)
changeset 265629d25ef112cf6
parent 26561 394cd765643d
child 26563 420567ad8125
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
NEWS
src/HOL/Hilbert_Choice.thy
src/HOL/Tools/meson.ML
src/HOL/Tools/res_axioms.ML
     1.1 --- a/NEWS	Mon Apr 07 15:37:04 2008 +0200
     1.2 +++ b/NEWS	Mon Apr 07 15:37:27 2008 +0200
     1.3 @@ -173,6 +173,8 @@
     1.4  * Metis prover is now an order of magnitude faster, and also works
     1.5  with multithreading.
     1.6  
     1.7 +* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
     1.8 +
     1.9  * Sledgehammer no longer produces structured proofs by default. To enable, 
    1.10  declare [[sledgehammer_full = true]]. Attributes reconstruction_modulus,  
    1.11  reconstruction_sorts renamed sledgehammer_modulus, sledgehammer_sorts. 
     2.1 --- a/src/HOL/Hilbert_Choice.thy	Mon Apr 07 15:37:04 2008 +0200
     2.2 +++ b/src/HOL/Hilbert_Choice.thy	Mon Apr 07 15:37:27 2008 +0200
     2.3 @@ -635,6 +635,8 @@
     2.4  
     2.5  use "Tools/meson.ML"
     2.6  
     2.7 +setup Meson.setup
     2.8 +
     2.9  
    2.10  subsection {* Specification package -- Hilbertized version *}
    2.11  
     3.1 --- a/src/HOL/Tools/meson.ML	Mon Apr 07 15:37:04 2008 +0200
     3.2 +++ b/src/HOL/Tools/meson.ML	Mon Apr 07 15:37:27 2008 +0200
     3.3 @@ -14,7 +14,7 @@
     3.4    val first_order_resolve: thm -> thm -> thm
     3.5    val flexflex_first_order: thm -> thm
     3.6    val size_of_subgoals: thm -> int
     3.7 -  val too_many_clauses: term -> bool
     3.8 +  val too_many_clauses: Proof.context option -> term -> bool
     3.9    val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
    3.10    val finish_cnf: thm list -> thm list
    3.11    val make_nnf: thm -> thm
    3.12 @@ -41,11 +41,15 @@
    3.13    val negate_head: thm -> thm
    3.14    val select_literal: int -> thm -> thm
    3.15    val skolemize_tac: int -> tactic
    3.16 +  val setup: Context.theory -> Context.theory
    3.17  end
    3.18  
    3.19  structure Meson: MESON =
    3.20  struct
    3.21  
    3.22 +val max_clauses_default = 60;
    3.23 +val (max_clauses, setup) = Attrib.config_int "max_clauses" max_clauses_default;
    3.24 +
    3.25  val not_conjD = thm "meson_not_conjD";
    3.26  val not_disjD = thm "meson_not_disjD";
    3.27  val not_notD = thm "meson_not_notD";
    3.28 @@ -237,37 +241,39 @@
    3.29  
    3.30  (*** The basic CNF transformation ***)
    3.31  
    3.32 -val max_clauses = 40;
    3.33 -
    3.34 -fun sum x y = if x < max_clauses andalso y < max_clauses then x+y else max_clauses;
    3.35 -fun prod x y = if x < max_clauses andalso y < max_clauses then x*y else max_clauses;
    3.36 -
    3.37 -(*Estimate the number of clauses in order to detect infeasible theorems*)
    3.38 -fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
    3.39 -  | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t
    3.40 -  | signed_nclauses b (Const("op &",_) $ t $ u) =
    3.41 -      if b then sum (signed_nclauses b t) (signed_nclauses b u)
    3.42 -           else prod (signed_nclauses b t) (signed_nclauses b u)
    3.43 -  | signed_nclauses b (Const("op |",_) $ t $ u) =
    3.44 -      if b then prod (signed_nclauses b t) (signed_nclauses b u)
    3.45 -           else sum (signed_nclauses b t) (signed_nclauses b u)
    3.46 -  | signed_nclauses b (Const("op -->",_) $ t $ u) =
    3.47 -      if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
    3.48 -           else sum (signed_nclauses (not b) t) (signed_nclauses b u)
    3.49 -  | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) =
    3.50 -      if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
    3.51 -          if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
    3.52 -                        (prod (signed_nclauses (not b) u) (signed_nclauses b t))
    3.53 -               else sum (prod (signed_nclauses b t) (signed_nclauses b u))
    3.54 -                        (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
    3.55 -      else 1
    3.56 -  | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
    3.57 -  | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
    3.58 -  | signed_nclauses _ _ = 1; (* literal *)
    3.59 -
    3.60 -val nclauses = signed_nclauses true;
    3.61 -
    3.62 -fun too_many_clauses t = nclauses t >= max_clauses;
    3.63 +fun too_many_clauses ctxto t = 
    3.64 + let
    3.65 +  val max_cl = case ctxto of SOME ctxt => Config.get ctxt max_clauses
    3.66 +                           | NONE => max_clauses_default
    3.67 +  
    3.68 +  fun sum x y = if x < max_cl andalso y < max_cl then x+y else max_cl;
    3.69 +  fun prod x y = if x < max_cl andalso y < max_cl then x*y else max_cl;
    3.70 +  
    3.71 +  (*Estimate the number of clauses in order to detect infeasible theorems*)
    3.72 +  fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
    3.73 +    | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t
    3.74 +    | signed_nclauses b (Const("op &",_) $ t $ u) =
    3.75 +	if b then sum (signed_nclauses b t) (signed_nclauses b u)
    3.76 +	     else prod (signed_nclauses b t) (signed_nclauses b u)
    3.77 +    | signed_nclauses b (Const("op |",_) $ t $ u) =
    3.78 +	if b then prod (signed_nclauses b t) (signed_nclauses b u)
    3.79 +	     else sum (signed_nclauses b t) (signed_nclauses b u)
    3.80 +    | signed_nclauses b (Const("op -->",_) $ t $ u) =
    3.81 +	if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
    3.82 +	     else sum (signed_nclauses (not b) t) (signed_nclauses b u)
    3.83 +    | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) =
    3.84 +	if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
    3.85 +	    if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
    3.86 +			  (prod (signed_nclauses (not b) u) (signed_nclauses b t))
    3.87 +		 else sum (prod (signed_nclauses b t) (signed_nclauses b u))
    3.88 +			  (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
    3.89 +	else 1
    3.90 +    | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
    3.91 +    | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
    3.92 +    | signed_nclauses _ _ = 1; (* literal *)
    3.93 + in 
    3.94 +  signed_nclauses true t >= max_cl
    3.95 + end;
    3.96  
    3.97  (*Replaces universally quantified variables by FREE variables -- because
    3.98    assumptions may not contain scheme variables.  Later, generalize using Variable.export. *)
    3.99 @@ -328,8 +334,8 @@
   3.100            | _ => nodups th :: ths  (*no work to do*)
   3.101        and cnf_nil th = cnf_aux (th,[])
   3.102        val cls = 
   3.103 -	    if too_many_clauses (concl_of th)
   3.104 -	    then (Output.debug (fn () => ("cnf is ignoring: " ^ string_of_thm th)); ths)
   3.105 +	    if too_many_clauses (SOME ctxt) (concl_of th)
   3.106 +	    then (warning ("cnf is ignoring: " ^ string_of_thm th); ths)
   3.107  	    else cnf_aux (th,ths)
   3.108    in  (cls, !ctxtr)  end;
   3.109  
     4.1 --- a/src/HOL/Tools/res_axioms.ML	Mon Apr 07 15:37:04 2008 +0200
     4.2 +++ b/src/HOL/Tools/res_axioms.ML	Mon Apr 07 15:37:27 2008 +0200
     4.3 @@ -339,7 +339,7 @@
     4.4  
     4.5  fun too_complex t = 
     4.6    apply_depth t > max_apply_depth orelse 
     4.7 -  Meson.too_many_clauses t orelse
     4.8 +  Meson.too_many_clauses NONE t orelse
     4.9    excessive_lambdas_fm [] t;
    4.10    
    4.11  fun is_strange_thm th =