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