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