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