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