now uses the heap data structure for BEST_FIRST
authorpaulson
Tue Jun 20 11:54:07 2000 +0200 (2000-06-20)
changeset 9094530e7a33b3dd
parent 9093 2e608fa6c404
child 9095 3b26cc949016
now uses the heap data structure for BEST_FIRST
src/Pure/search.ML
     1.1 --- a/src/Pure/search.ML	Tue Jun 20 11:53:35 2000 +0200
     1.2 +++ b/src/Pure/search.ML	Tue Jun 20 11:54:07 2000 +0200
     1.3 @@ -37,6 +37,23 @@
     1.4    val QUIET_BREADTH_FIRST	: (thm -> bool) -> tactic -> tactic
     1.5    end;
     1.6  
     1.7 +
     1.8 +(** Instantiation of leftist heaps for best-first search **)
     1.9 +
    1.10 +(*Termless makes the ordering total, allowing duplicates to be found*)
    1.11 +structure MeasureThm : ORDERED =
    1.12 +struct
    1.13 +  type T = int * thm
    1.14 +  fun eq ((m,th):T, (m',th')) = (m=m' andalso eq_thm(th,th'))
    1.15 +  fun lt ((m,th):T, (m',th')) = 
    1.16 +          (m<m' orelse 
    1.17 +	   m=m' andalso Term.termless (#prop(rep_thm th), #prop(rep_thm th')))
    1.18 +  fun leq (mth, mth') = not (lt (mth',mth))
    1.19 +end;
    1.20 +
    1.21 +structure MeasureThmHeap = LeftistHeap(MeasureThm);
    1.22 +
    1.23 +
    1.24  structure Search : SEARCH = 
    1.25  struct
    1.26  
    1.27 @@ -184,18 +201,16 @@
    1.28  
    1.29  val trace_BEST_FIRST = ref false;
    1.30  
    1.31 -(*Insertion into priority queue of states *)
    1.32 -fun insert (nth: int*thm, []) = [nth]
    1.33 -  | insert ((m,th), (n,th')::nths) = 
    1.34 -      if  n<m then (n,th') :: insert ((m,th), nths)
    1.35 -      else if  n=m andalso eq_thm(th,th')
    1.36 -              then (n,th')::nths
    1.37 -              else (m,th)::(n,th')::nths;
    1.38 -
    1.39  (*For creating output sequence*)
    1.40  fun some_of_list []     = None
    1.41    | some_of_list (x::l) = Some (x, Seq.make (fn () => some_of_list l));
    1.42  
    1.43 +(*Check for and delete duplicate proof states*)
    1.44 +fun deleteAllMin prf heap = 
    1.45 +      if MeasureThmHeap.isEmpty heap then heap
    1.46 +      else if eq_thm (prf, #2 (MeasureThmHeap.findMin heap))
    1.47 +      then deleteAllMin prf (MeasureThmHeap.deleteMin heap)
    1.48 +      else heap;
    1.49  
    1.50  (*Best-first search for a state that satisfies satp (incl initial state)
    1.51    Function sizef estimates size of problem remaining (smaller means better).
    1.52 @@ -203,19 +218,22 @@
    1.53  fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 = 
    1.54    let val tac = tracify trace_BEST_FIRST tac1
    1.55        fun pairsize th = (sizef th, th);
    1.56 -      fun bfs (news,nprfs) =
    1.57 +      fun bfs (news,nprf_heap) =
    1.58  	   (case  partition satp news  of
    1.59 -		([],nonsats) => next(foldr insert
    1.60 -					(map pairsize nonsats, nprfs)) 
    1.61 +		([],nonsats) => next(foldr MeasureThmHeap.insert
    1.62 +					(map pairsize nonsats, nprf_heap)) 
    1.63  	      | (sats,_)  => some_of_list sats)
    1.64 -      and next [] = None
    1.65 -        | next ((n,prf)::nprfs) =
    1.66 -	    (if !trace_BEST_FIRST 
    1.67 -	       then writeln("state size = " ^ string_of_int n ^ 
    1.68 -		         "  queue length =" ^ string_of_int (length nprfs))  
    1.69 +      and next nprf_heap =
    1.70 +            if MeasureThmHeap.isEmpty nprf_heap then None
    1.71 +	    else 
    1.72 +	    let val (n,prf) = MeasureThmHeap.findMin nprf_heap
    1.73 +	    in if !trace_BEST_FIRST 
    1.74 +	       then writeln("state size = " ^ string_of_int n)  
    1.75                 else ();
    1.76 -	     bfs (Seq.list_of (tac prf), nprfs))
    1.77 -      fun btac st = bfs (Seq.list_of (tac0 st),  [])
    1.78 +	       bfs (Seq.list_of (tac prf), 
    1.79 +		    deleteAllMin prf (MeasureThmHeap.deleteMin nprf_heap))
    1.80 +            end
    1.81 +      fun btac st = bfs (Seq.list_of (tac0 st),  MeasureThmHeap.empty)
    1.82    in traced_tac btac end;
    1.83  
    1.84  (*Ordinary best-first search, with no initial tactic*)