src/Pure/search.ML
author wenzelm
Mon Feb 26 23:18:24 2007 +0100 (2007-02-26)
changeset 22360 26ead7ed4f4b
parent 22025 7c5896919eb8
child 23178 07ba6b58b3d2
permissions -rw-r--r--
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
     1 (*  Title: 	Pure/search.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson and Norbert Voelker
     4 
     5 Search tacticals.
     6 *)
     7 
     8 infix 1 THEN_MAYBE THEN_MAYBE';
     9 
    10 signature SEARCH =
    11   sig
    12   val DEEPEN  	        : int*int -> (int->int->tactic) -> int -> int -> tactic
    13 
    14   val THEN_MAYBE	: tactic * tactic -> tactic
    15   val THEN_MAYBE'	: ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
    16 
    17   val trace_DEPTH_FIRST	: bool ref
    18   val DEPTH_FIRST	: (thm -> bool) -> tactic -> tactic
    19   val DEPTH_SOLVE	: tactic -> tactic
    20   val DEPTH_SOLVE_1	: tactic -> tactic
    21   val ITER_DEEPEN	: (thm->bool) -> (int->tactic) -> tactic
    22   val THEN_ITER_DEEPEN	: tactic -> (thm->bool) -> (int->tactic) -> tactic
    23   val iter_deepen_limit : int ref
    24 
    25   val has_fewer_prems	: int -> thm -> bool   
    26   val IF_UNSOLVED	: tactic -> tactic
    27   val SOLVE		: tactic -> tactic
    28   val DETERM_UNTIL_SOLVED: tactic -> tactic
    29   val trace_BEST_FIRST	: bool ref
    30   val BEST_FIRST	: (thm -> bool) * (thm -> int) -> tactic -> tactic
    31   val THEN_BEST_FIRST	: tactic -> (thm->bool) * (thm->int) -> tactic
    32 			  -> tactic
    33   val trace_ASTAR	: bool ref
    34   val ASTAR	        : (thm -> bool) * (int->thm->int) -> tactic -> tactic
    35   val THEN_ASTAR	: tactic -> (thm->bool) * (int->thm->int) -> tactic
    36 			  -> tactic
    37   val BREADTH_FIRST	: (thm -> bool) -> tactic -> tactic
    38   val QUIET_BREADTH_FIRST	: (thm -> bool) -> tactic -> tactic
    39   end;
    40 
    41 
    42 (** Instantiation of heaps for best-first search **)
    43 
    44 (*total ordering on theorems, allowing duplicates to be found*)
    45 structure ThmHeap =
    46   HeapFun (type elem = int * thm
    47     val ord = Library.prod_ord Library.int_ord
    48       (Term.term_ord o Library.pairself (#prop o Thm.rep_thm)));
    49 
    50 
    51 structure Search : SEARCH = 
    52 struct
    53 
    54 (**** Depth-first search ****)
    55 
    56 val trace_DEPTH_FIRST = ref false;
    57 
    58 (*Searches until "satp" reports proof tree as satisfied.
    59   Suppresses duplicate solutions to minimize search space.*)
    60 fun DEPTH_FIRST satp tac = 
    61  let val tac = tracify trace_DEPTH_FIRST tac
    62      fun depth used [] = NONE
    63        | depth used (q::qs) =
    64 	  case Seq.pull q of
    65 	      NONE         => depth used qs
    66 	    | SOME(st,stq) => 
    67 		if satp st andalso not (member Thm.eq_thm used st)
    68 		then SOME(st, Seq.make
    69 			         (fn()=> depth (st::used) (stq::qs)))
    70 		else depth used (tac st :: stq :: qs)
    71   in  traced_tac (fn st => depth [] [Seq.single st])  end;
    72 
    73 
    74 
    75 (*Predicate: Does the rule have fewer than n premises?*)
    76 fun has_fewer_prems n rule = (nprems_of rule < n);
    77 
    78 (*Apply a tactic if subgoals remain, else do nothing.*)
    79 val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac;
    80 
    81 (*Force a tactic to solve its goal completely, otherwise fail *)
    82 fun SOLVE tac = tac THEN COND (has_fewer_prems 1) all_tac no_tac;
    83 
    84 (*Force repeated application of tactic until goal is solved completely *)
    85 val DETERM_UNTIL_SOLVED = DETERM_UNTIL (has_fewer_prems 1);
    86 
    87 (*Execute tac1, but only execute tac2 if there are at least as many subgoals
    88   as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
    89 fun (tac1 THEN_MAYBE tac2) st = 
    90     (tac1  THEN  COND (has_fewer_prems (nprems_of st)) all_tac tac2)  st;
    91 
    92 fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x;
    93 
    94 (*Tactical to reduce the number of premises by 1.
    95   If no subgoals then it must fail! *)
    96 fun DEPTH_SOLVE_1 tac st = st |>
    97     (case nprems_of st of
    98 	0 => no_tac
    99       | n => DEPTH_FIRST (has_fewer_prems n) tac);
   100 
   101 (*Uses depth-first search to solve ALL subgoals*)
   102 val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1);
   103 
   104 
   105 
   106 (**** Iterative deepening with pruning ****)
   107 
   108 fun has_vars (Var _) = true
   109   | has_vars (Abs (_,_,t)) = has_vars t
   110   | has_vars (f$t) = has_vars f orelse has_vars t
   111   | has_vars _ = false;
   112 
   113 (*Counting of primitive inferences is APPROXIMATE, as the step tactic
   114   may perform >1 inference*)
   115 
   116 (*Pruning of rigid ancestor to prevent backtracking*)
   117 fun prune (new as (k', np':int, rgd', stq), qs) = 
   118     let fun prune_aux (qs, []) = new::qs
   119           | prune_aux (qs, (k,np,rgd,q)::rqs) =
   120 	      if np'+1 = np andalso rgd then
   121 		  (if !trace_DEPTH_FIRST then
   122 		       tracing ("Pruning " ^ 
   123 				string_of_int (1+length rqs) ^ " levels")
   124 		   else ();
   125 		   (*Use OLD k: zero-cost solution; see Stickel, p 365*)
   126 		   (k, np', rgd', stq) :: qs)
   127 	      else prune_aux ((k,np,rgd,q)::qs, rqs)
   128         fun take ([], rqs) = ([], rqs)
   129 	  | take (arg as ((k,np,rgd,stq)::qs, rqs)) = 
   130 	        if np' < np then take (qs, (k,np,rgd,stq)::rqs)
   131 		            else arg
   132     in  prune_aux (take (qs, []))  end;
   133 
   134 
   135 (*No known example (on 1-5-2007) needs even thirty*)
   136 val iter_deepen_limit = ref 50;
   137 
   138 (*Depth-first iterative deepening search for a state that satisfies satp
   139   tactic tac0 sets up the initial goal queue, while tac1 searches it.
   140   The solution sequence is redundant: the cutoff heuristic makes it impossible
   141   to suppress solutions arising from earlier searches, as the accumulated cost
   142   (k) can be wrong.*)
   143 fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st => 
   144  let val countr = ref 0
   145      and tf = tracify trace_DEPTH_FIRST (tac1 1)
   146      and qs0 = tac0 st
   147      (*bnd = depth bound; inc = estimate of increment required next*)
   148      fun depth (bnd,inc) [] = 
   149           if bnd > !iter_deepen_limit then
   150 	     (tracing (string_of_int (!countr) ^ 
   151 		       " inferences so far.  Giving up at " ^ string_of_int bnd);
   152 	      NONE)
   153           else
   154 	     (tracing (string_of_int (!countr) ^ 
   155 		       " inferences so far.  Searching to depth " ^ 
   156 		       string_of_int bnd);
   157 	      (*larger increments make it run slower for the hard problems*)
   158 	      depth (bnd+inc, 10)) [(0, 1, false, qs0)]
   159        | depth (bnd,inc) ((k,np,rgd,q)::qs) =
   160 	  if k>=bnd then depth (bnd,inc) qs
   161           else
   162 	  case (countr := !countr+1;
   163 		if !trace_DEPTH_FIRST then
   164 		    tracing (string_of_int np ^ implode (map (fn _ => "*") qs))
   165 		else ();
   166 		Seq.pull q) of
   167 	     NONE         => depth (bnd,inc) qs
   168 	   | SOME(st,stq) => 
   169 	       if satp st	(*solution!*)
   170 	       then SOME(st, Seq.make
   171 			 (fn()=> depth (bnd,inc) ((k,np,rgd,stq)::qs)))
   172 
   173 	       else 
   174                let val np' = nprems_of st
   175 		     (*rgd' calculation assumes tactic operates on subgoal 1*)
   176                    val rgd' = not (has_vars (hd (prems_of st)))
   177                    val k' = k+np'-np+1  (*difference in # of subgoals, +1*)
   178                in  if k'+np' >= bnd 
   179 		   then depth (bnd, Int.min(inc, k'+np'+1-bnd)) qs
   180 		   else if np' < np (*solved a subgoal; prune rigid ancestors*)
   181                    then depth (bnd,inc) 
   182 		         (prune ((k', np', rgd', tf st), (k,np,rgd,stq) :: qs))
   183 	           else depth (bnd,inc) ((k', np', rgd', tf st) :: 
   184 					 (k,np,rgd,stq) :: qs)
   185 	       end
   186   in depth (0,5) [] end);
   187 
   188 val ITER_DEEPEN = THEN_ITER_DEEPEN all_tac;
   189 
   190 
   191 (*Simple iterative deepening tactical.  It merely "deepens" any search tactic
   192   using increment "inc" up to limit "lim". *)
   193 fun DEEPEN (inc,lim) tacf m i = 
   194   let fun dpn m st = 
   195        st |> (if has_fewer_prems i st then no_tac
   196 	      else if m>lim then 
   197 		       (warning "Search depth limit exceeded: giving up"; 
   198 			no_tac)
   199 	      else (warning ("Search depth = " ^ string_of_int m);
   200 			     tacf m i  ORELSE  dpn (m+inc)))
   201   in  dpn m  end;
   202  
   203 (*** Best-first search ***)
   204 
   205 val trace_BEST_FIRST = ref false;
   206 
   207 (*For creating output sequence*)
   208 fun some_of_list []     = NONE
   209   | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
   210 
   211 (*Check for and delete duplicate proof states*)
   212 fun deleteAllMin prf heap = 
   213       if ThmHeap.is_empty heap then heap
   214       else if Thm.eq_thm (prf, #2 (ThmHeap.min heap))
   215       then deleteAllMin prf (ThmHeap.delete_min heap)
   216       else heap;
   217 
   218 (*Best-first search for a state that satisfies satp (incl initial state)
   219   Function sizef estimates size of problem remaining (smaller means better).
   220   tactic tac0 sets up the initial priority queue, while tac1 searches it. *)
   221 fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 = 
   222   let val tac = tracify trace_BEST_FIRST tac1
   223       fun pairsize th = (sizef th, th);
   224       fun bfs (news,nprf_heap) =
   225 	   (case  List.partition satp news  of
   226 		([],nonsats) => next(foldr ThmHeap.insert
   227 					nprf_heap (map pairsize nonsats))
   228 	      | (sats,_)  => some_of_list sats)
   229       and next nprf_heap =
   230             if ThmHeap.is_empty nprf_heap then NONE
   231 	    else 
   232 	    let val (n,prf) = ThmHeap.min nprf_heap
   233 	    in if !trace_BEST_FIRST 
   234 	       then tracing("state size = " ^ string_of_int n)  
   235                else ();
   236 	       bfs (Seq.list_of (tac prf), 
   237 		    deleteAllMin prf (ThmHeap.delete_min nprf_heap))
   238             end
   239       fun btac st = bfs (Seq.list_of (tac0 st), ThmHeap.empty)
   240   in traced_tac btac end;
   241 
   242 (*Ordinary best-first search, with no initial tactic*)
   243 val BEST_FIRST = THEN_BEST_FIRST all_tac;
   244 
   245 (*Breadth-first search to satisfy satpred (including initial state) 
   246   SLOW -- SHOULD NOT USE APPEND!*)
   247 fun gen_BREADTH_FIRST message satpred (tac:tactic) = 
   248   let val tacf = Seq.list_of o tac;
   249       fun bfs prfs =
   250 	 (case  List.partition satpred prfs  of
   251 	      ([],[]) => []
   252 	    | ([],nonsats) => 
   253 		  (message("breadth=" ^ string_of_int(length nonsats));
   254 		   bfs (maps tacf nonsats))
   255 	    | (sats,_)  => sats)
   256   in (fn st => Seq.of_list (bfs [st])) end;
   257 
   258 val BREADTH_FIRST = gen_BREADTH_FIRST tracing;
   259 val QUIET_BREADTH_FIRST = gen_BREADTH_FIRST (K ());
   260 
   261 
   262 (*  Author: 	Norbert Voelker, FernUniversitaet Hagen
   263     Remarks:    Implementation of A*-like proof procedure by modification
   264 		of the existing code for BEST_FIRST and best_tac so that the 
   265 		current level of search is taken into account.
   266 *)		
   267 
   268 (*Insertion into priority queue of states, marked with level *)
   269 fun insert_with_level (lnth: int*int*thm, []) = [lnth]
   270   | insert_with_level ((l,m,th), (l',n,th')::nths) = 
   271       if  n<m then (l',n,th') :: insert_with_level ((l,m,th), nths)
   272       else if  n=m andalso Thm.eq_thm(th,th')
   273               then (l',n,th')::nths
   274               else (l,m,th)::(l',n,th')::nths;
   275 
   276 (*For creating output sequence*)
   277 fun some_of_list []     = NONE
   278   | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
   279 
   280 val trace_ASTAR = ref false; 
   281 
   282 fun THEN_ASTAR tac0 (satp, costf) tac1 = 
   283   let val tf = tracify trace_ASTAR tac1;   
   284       fun bfs (news,nprfs,level) =
   285       let fun cost thm = (level, costf level thm, thm)
   286       in (case  List.partition satp news  of
   287             ([],nonsats) 
   288 		 => next (foldr insert_with_level nprfs (map cost nonsats))
   289           | (sats,_)  => some_of_list sats)
   290       end and    
   291       next []  = NONE
   292         | next ((level,n,prf)::nprfs)  =
   293             (if !trace_ASTAR 
   294                then tracing("level = " ^ string_of_int level ^
   295 			 "  cost = " ^ string_of_int n ^ 
   296                          "  queue length =" ^ string_of_int (length nprfs))  
   297                else ();
   298              bfs (Seq.list_of (tf prf), nprfs,level+1))
   299       fun tf st = bfs (Seq.list_of (tac0 st), [], 0)
   300   in traced_tac tf end;
   301 
   302 (*Ordinary ASTAR, with no initial tactic*)
   303 val ASTAR = THEN_ASTAR all_tac;
   304 
   305 end;
   306 
   307 open Search;