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