src/Pure/search.ML
author paulson
Fri Nov 01 15:15:39 1996 +0100 (1996-11-01)
changeset 2143 093bbe6d333b
parent 1588 fff3738830f5
child 2672 85d7e800d754
permissions -rw-r--r--
Replaced min by Int.min
     1 (*  Title: 	search
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson and Norbert Voelker
     4 
     5 Search tacticals
     6 *)
     7 
     8 signature SEARCH =
     9   sig
    10   val trace_DEPTH_FIRST	: bool ref
    11   val DEPTH_FIRST	: (thm -> bool) -> tactic -> tactic
    12   val DEPTH_SOLVE	: tactic -> tactic
    13   val DEPTH_SOLVE_1	: tactic -> tactic
    14   val ITER_DEEPEN	: (thm->bool) -> (int->tactic) -> tactic
    15   val THEN_ITER_DEEPEN	: tactic -> (thm->bool) -> (int->tactic) -> tactic
    16 
    17   val has_fewer_prems	: int -> thm -> bool   
    18   val IF_UNSOLVED	: tactic -> tactic
    19   val trace_BEST_FIRST	: bool ref
    20   val BEST_FIRST	: (thm -> bool) * (thm -> int) -> tactic -> tactic
    21   val THEN_BEST_FIRST	: tactic -> (thm->bool) * (thm->int) -> tactic
    22 			  -> tactic
    23   val trace_ASTAR	: bool ref
    24   val ASTAR	        : (thm -> bool) * (int->thm->int) -> tactic -> tactic
    25   val THEN_ASTAR	: tactic -> (thm->bool) * (int->thm->int) -> tactic
    26 			  -> tactic
    27   val BREADTH_FIRST	: (thm -> bool) -> tactic -> tactic
    28   end;
    29 
    30 structure Search : SEARCH = 
    31 struct
    32 
    33 (**** Depth-first search ****)
    34 
    35 val trace_DEPTH_FIRST = ref false;
    36 
    37 (*Searches until "satp" reports proof tree as satisfied.
    38   Suppresses duplicate solutions to minimize search space.*)
    39 fun DEPTH_FIRST satp tac = 
    40  let val tac = tracify trace_DEPTH_FIRST tac
    41      fun depth used [] = None
    42        | depth used (q::qs) =
    43 	  case Sequence.pull q of
    44 	      None         => depth used qs
    45 	    | Some(st,stq) => 
    46 		if satp st andalso not (gen_mem eq_thm (st, used))
    47 		then Some(st, Sequence.seqof
    48 			         (fn()=> depth (st::used) (stq::qs)))
    49 		else depth used (tac st :: stq :: qs)
    50   in  traced_tac (fn st => depth [] ([Sequence.single st]))  end;
    51 
    52 
    53 
    54 (*Predicate: Does the rule have fewer than n premises?*)
    55 fun has_fewer_prems n rule = (nprems_of rule < n);
    56 
    57 (*Apply a tactic if subgoals remain, else do nothing.*)
    58 val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac;
    59 
    60 (*Tactical to reduce the number of premises by 1.
    61   If no subgoals then it must fail! *)
    62 fun DEPTH_SOLVE_1 tac = STATE
    63  (fn st => 
    64     (case nprems_of st of
    65 	0 => no_tac
    66       | n => DEPTH_FIRST (has_fewer_prems n) tac));
    67 
    68 (*Uses depth-first search to solve ALL subgoals*)
    69 val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1);
    70 
    71 
    72 
    73 (**** Iterative deepening ****)
    74 
    75 fun has_vars (Var _) = true
    76   | has_vars (Abs (_,_,t)) = has_vars t
    77   | has_vars (f$t) = has_vars f orelse has_vars t
    78   | has_vars _ = false;
    79 
    80 (*Counting of primitive inferences is APPROXIMATE, as the step tactic
    81   may perform >1 inference*)
    82 
    83 (*Pruning of rigid ancestor to prevent backtracking*)
    84 fun prune (new as (k', np':int, rgd', stq), qs) = 
    85     let fun prune_aux (qs, []) = new::qs
    86           | prune_aux (qs, (k,np,rgd,q)::rqs) =
    87 	      if np'+1 = np andalso rgd then
    88 		  (if !trace_DEPTH_FIRST then
    89 		       writeln ("Pruning " ^ 
    90 				string_of_int (1+length rqs) ^ " levels")
    91 		   else ();
    92 		   (*Use OLD k: zero-cost solution; see Stickel, p 365*)
    93 		   (k, np', rgd', stq) :: qs)
    94 	      else prune_aux ((k,np,rgd,q)::qs, rqs)
    95         fun take ([], rqs) = ([], rqs)
    96 	  | take (arg as ((k,np,rgd,stq)::qs, rqs)) = 
    97 	        if np' < np then take (qs, (k,np,rgd,stq)::rqs)
    98 		            else arg
    99     in  prune_aux (take (qs, []))  end;
   100 
   101 
   102 (*Depth-first iterative deepening search for a state that satisfies satp
   103   tactic tac0 sets up the initial goal queue, while tac1 searches it.
   104   The solution sequence is redundant: the cutoff heuristic makes it impossible
   105   to suppress solutions arising from earlier searches, as the accumulated cost
   106   (k) can be wrong.*)
   107 fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st => 
   108  let val countr = ref 0
   109      and tf = tracify trace_DEPTH_FIRST (tac1 1)
   110      and qs0 = tac0 st
   111      (*bnd = depth bound; inc = estimate of increment required next*)
   112      fun depth (bnd,inc) [] = 
   113 	     (writeln (string_of_int (!countr) ^ 
   114 		       " inferences so far.  Searching to depth " ^ 
   115 		       string_of_int bnd);
   116 	      (*larger increments make it run slower for the hard problems*)
   117 	      depth (bnd+inc, 10)) [(0, 1, false, qs0)]
   118        | depth (bnd,inc) ((k,np,rgd,q)::qs) =
   119 	  if k>=bnd then depth (bnd,inc) qs
   120           else
   121 	  case (countr := !countr+1;
   122 		if !trace_DEPTH_FIRST then
   123 		    writeln (string_of_int np ^ 
   124 			     implode (map (fn _ => "*") qs))
   125 		else ();
   126 		Sequence.pull q) of
   127 	     None         => depth (bnd,inc) qs
   128 	   | Some(st,stq) => 
   129 	       if satp st	(*solution!*)
   130 	       then Some(st, Sequence.seqof
   131 			 (fn()=> depth (bnd,inc) ((k,np,rgd,stq)::qs)))
   132 
   133 	       else 
   134                let val np' = nprems_of st
   135 		     (*rgd' calculation assumes tactic operates on subgoal 1*)
   136                    val rgd' = not (has_vars (hd (prems_of st)))
   137                    val k' = k+np'-np+1  (*difference in # of subgoals, +1*)
   138                in  if k'+np' >= bnd 
   139 		   then depth (bnd, Int.min(inc, k'+np'+1-bnd)) qs
   140 		   else if np' < np (*solved a subgoal; prune rigid ancestors*)
   141                    then depth (bnd,inc) 
   142 		         (prune ((k', np', rgd', tf st), (k,np,rgd,stq) :: qs))
   143 	           else depth (bnd,inc) ((k', np', rgd', tf st) :: 
   144 					 (k,np,rgd,stq) :: qs)
   145 	       end
   146   in depth (0,5) [] end);
   147 
   148 val ITER_DEEPEN = THEN_ITER_DEEPEN all_tac;
   149 
   150 
   151 (*** Best-first search ***)
   152 
   153 val trace_BEST_FIRST = ref false;
   154 
   155 (*Insertion into priority queue of states *)
   156 fun insert (nth: int*thm, []) = [nth]
   157   | insert ((m,th), (n,th')::nths) = 
   158       if  n<m then (n,th') :: insert ((m,th), nths)
   159       else if  n=m andalso eq_thm(th,th')
   160               then (n,th')::nths
   161               else (m,th)::(n,th')::nths;
   162 
   163 (*For creating output sequence*)
   164 fun some_of_list []     = None
   165   | some_of_list (x::l) = Some (x, Sequence.seqof (fn () => some_of_list l));
   166 
   167 
   168 (*Best-first search for a state that satisfies satp (incl initial state)
   169   Function sizef estimates size of problem remaining (smaller means better).
   170   tactic tac0 sets up the initial priority queue, while tac1 searches it. *)
   171 fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 = 
   172   let val tac = tracify trace_BEST_FIRST tac1
   173       fun pairsize th = (sizef th, th);
   174       fun bfs (news,nprfs) =
   175 	   (case  partition satp news  of
   176 		([],nonsats) => next(foldr insert
   177 					(map pairsize nonsats, nprfs)) 
   178 	      | (sats,_)  => some_of_list sats)
   179       and next [] = None
   180         | next ((n,prf)::nprfs) =
   181 	    (if !trace_BEST_FIRST 
   182 	       then writeln("state size = " ^ string_of_int n ^ 
   183 		         "  queue length =" ^ string_of_int (length nprfs))  
   184                else ();
   185 	     bfs (Sequence.list_of_s (tac prf), nprfs))
   186       fun btac st = bfs (Sequence.list_of_s (tac0 st),  [])
   187   in traced_tac btac end;
   188 
   189 (*Ordinary best-first search, with no initial tactic*)
   190 val BEST_FIRST = THEN_BEST_FIRST all_tac;
   191 
   192 (*Breadth-first search to satisfy satpred (including initial state) 
   193   SLOW -- SHOULD NOT USE APPEND!*)
   194 fun BREADTH_FIRST satpred tac = 
   195   let val tacf = Sequence.list_of_s o tac;
   196       fun bfs prfs =
   197 	 (case  partition satpred prfs  of
   198 	      ([],[]) => []
   199 	    | ([],nonsats) => 
   200 		  (prs("breadth=" ^ string_of_int(length nonsats) ^ "\n");
   201 		   bfs (flat (map tacf nonsats)))
   202 	    | (sats,_)  => sats)
   203   in (fn st => Sequence.s_of_list (bfs [st])) end;
   204 
   205 
   206 (*  Author: 	Norbert Voelker, FernUniversitaet Hagen
   207     Remarks:    Implementation of A*-like proof procedure by modification
   208 		of the existing code for BEST_FIRST and best_tac so that the 
   209 		current level of search is taken into account.
   210 *)		
   211 
   212 (*Insertion into priority queue of states, marked with level *)
   213 fun insert_with_level (lnth: int*int*thm, []) = [lnth]
   214   | insert_with_level ((l,m,th), (l',n,th')::nths) = 
   215       if  n<m then (l',n,th') :: insert_with_level ((l,m,th), nths)
   216       else if  n=m andalso eq_thm(th,th')
   217               then (l',n,th')::nths
   218               else (l,m,th)::(l',n,th')::nths;
   219 
   220 (*For creating output sequence*)
   221 fun some_of_list []     = None
   222   | some_of_list (x::l) = Some (x, Sequence.seqof (fn () => some_of_list l));
   223 
   224 val trace_ASTAR = ref false; 
   225 
   226 fun THEN_ASTAR tac0 (satp, costf) tac1 = 
   227   let val tf = tracify trace_ASTAR tac1;   
   228       fun bfs (news,nprfs,level) =
   229       let fun cost thm = (level, costf level thm, thm)
   230       in (case  partition satp news  of
   231             ([],nonsats) 
   232 		 => next (foldr insert_with_level (map cost nonsats, nprfs))
   233           | (sats,_)  => some_of_list sats)
   234       end and    
   235       next []  = None
   236         | next ((level,n,prf)::nprfs)  =
   237             (if !trace_ASTAR 
   238                then writeln("level = " ^ string_of_int level ^
   239 			 "  cost = " ^ string_of_int n ^ 
   240                          "  queue length =" ^ string_of_int (length nprfs))  
   241                else ();
   242              bfs (Sequence.list_of_s (tf prf), nprfs,level+1))
   243       fun tf st = bfs (Sequence.list_of_s (tac0 st), [], 0)
   244   in traced_tac tf end;
   245 
   246 (*Ordinary ASTAR, with no initial tactic*)
   247 val ASTAR = THEN_ASTAR all_tac;
   248 
   249 end;
   250 
   251 open Search;