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