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