|
1 (* Title: astar |
|
2 ID: $Id$ |
|
3 Author: Norbert Voelker, FernUniversitaet Hagen |
|
4 Remarks: Implementation of A*-like proof procedure by modification |
|
5 of the existing code for BEST_FIRST and best_tac so that the |
|
6 current level of search is taken into account. |
|
7 *) |
|
8 |
|
9 (*Insertion into priority queue of states, marked with level *) |
|
10 fun insert_with_level (lnth: int*int*thm, []) = [lnth] |
|
11 | insert_with_level ((l,m,th), (l',n,th')::nths) = |
|
12 if n<m then (l',n,th') :: insert_with_level ((l,m,th), nths) |
|
13 else if n=m andalso eq_thm(th,th') |
|
14 then (l',n,th')::nths |
|
15 else (l,m,th)::(l',n,th')::nths; |
|
16 |
|
17 (*For creating output sequence*) |
|
18 fun some_of_list [] = None |
|
19 | some_of_list (x::l) = Some (x, Sequence.seqof (fn () => some_of_list l)); |
|
20 |
|
21 infix THEN_ASTAR; |
|
22 val trace_ASTAR = ref false; |
|
23 |
|
24 fun (Tactic tf0) THEN_ASTAR (satp, costf, tac) = |
|
25 let val tf = tracify trace_ASTAR tac; |
|
26 fun bfs (news,nprfs,level) = |
|
27 let fun cost thm = (level,costf level thm,thm) |
|
28 in (case partition satp news of |
|
29 ([],nonsats) |
|
30 => next (foldr insert_with_level (map cost nonsats, nprfs)) |
|
31 | (sats,_) => some_of_list sats) |
|
32 end and |
|
33 next [] = None |
|
34 | next ((level,n,prf)::nprfs) = |
|
35 (if !trace_ASTAR |
|
36 then writeln("level = " ^ string_of_int level ^ |
|
37 " cost = " ^ string_of_int n ^ |
|
38 " queue length =" ^ string_of_int (length nprfs)) |
|
39 else (); |
|
40 bfs (Sequence.list_of_s (tf prf), nprfs,level+1)) |
|
41 fun tf st = bfs (Sequence.list_of_s (tf0 st), [], 0) |
|
42 in traced_tac tf end; |
|
43 |
|
44 (*Ordinary ASTAR, with no initial tactic*) |
|
45 fun ASTAR (satp,costf) tac = all_tac THEN_ASTAR (satp,costf,tac); |
|
46 |
|
47 (* ASTAR with weight weight_ASTAR as a classical prover *) |
|
48 val weight_ASTAR = ref 5; |
|
49 |
|
50 fun astar_tac cs = |
|
51 SELECT_GOAL ( ASTAR (has_fewer_prems 1 |
|
52 , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) |
|
53 (step_tac cs 1)); |
|
54 |
|
55 fun slow_astar_tac cs = |
|
56 SELECT_GOAL ( ASTAR (has_fewer_prems 1 |
|
57 , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) |
|
58 (slow_step_tac cs 1)); |
|
59 |