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