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