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