--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/astar.ML Wed Sep 07 13:04:28 1994 +0200
@@ -0,0 +1,59 @@
+(* Title: astar
+ ID: $Id$
+ Author: Norbert Voelker, FernUniversitaet Hagen
+ Remarks: Implementation of A*-like proof procedure by modification
+ of the existing code for BEST_FIRST and best_tac so that the
+ current level of search is taken into account.
+*)
+
+(*Insertion into priority queue of states, marked with level *)
+fun insert_with_level (lnth: int*int*thm, []) = [lnth]
+ | insert_with_level ((l,m,th), (l',n,th')::nths) =
+ if n<m then (l',n,th') :: insert_with_level ((l,m,th), nths)
+ else if n=m andalso eq_thm(th,th')
+ then (l',n,th')::nths
+ else (l,m,th)::(l',n,th')::nths;
+
+(*For creating output sequence*)
+fun some_of_list [] = None
+ | some_of_list (x::l) = Some (x, Sequence.seqof (fn () => some_of_list l));
+
+infix THEN_ASTAR;
+val trace_ASTAR = ref false;
+
+fun (Tactic tf0) THEN_ASTAR (satp, costf, tac) =
+ let val tf = tracify trace_ASTAR tac;
+ fun bfs (news,nprfs,level) =
+ let fun cost thm = (level,costf level thm,thm)
+ in (case partition satp news of
+ ([],nonsats)
+ => next (foldr insert_with_level (map cost nonsats, nprfs))
+ | (sats,_) => some_of_list sats)
+ end and
+ next [] = None
+ | next ((level,n,prf)::nprfs) =
+ (if !trace_ASTAR
+ then writeln("level = " ^ string_of_int level ^
+ " cost = " ^ string_of_int n ^
+ " queue length =" ^ string_of_int (length nprfs))
+ else ();
+ bfs (Sequence.list_of_s (tf prf), nprfs,level+1))
+ fun tf st = bfs (Sequence.list_of_s (tf0 st), [], 0)
+ in traced_tac tf end;
+
+(*Ordinary ASTAR, with no initial tactic*)
+fun ASTAR (satp,costf) tac = all_tac THEN_ASTAR (satp,costf,tac);
+
+(* ASTAR with weight weight_ASTAR as a classical prover *)
+val weight_ASTAR = ref 5;
+
+fun astar_tac cs =
+ SELECT_GOAL ( ASTAR (has_fewer_prems 1
+ , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level))
+ (step_tac cs 1));
+
+fun slow_astar_tac cs =
+ SELECT_GOAL ( ASTAR (has_fewer_prems 1
+ , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level))
+ (slow_step_tac cs 1));
+