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