# HG changeset patch
# User webertj
# Date 1127541470 -7200
# Node ID ae4af66b30720b6849ab329e3fd7890f4c4d839f
# Parent  5d03a69481b6fcd7f9c76a58459bac9255ee088e
replay_proof optimized: now performs backwards proof search

diff -r 5d03a69481b6 -r ae4af66b3072 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Sat Sep 24 07:21:46 2005 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Sat Sep 24 07:57:50 2005 +0200
@@ -124,7 +124,7 @@
 
 fun replay_chain sg clauses idx (c::cs) =
 let
-	val (SOME fc) = Array.sub (clauses, c)
+	val fc = (valOf o Array.sub) (clauses, c)
 
 	fun strip_neg (Const ("Trueprop", _) $ x) = strip_neg x
 	  | strip_neg (Const ("Not", _) $ x)      = x
@@ -175,25 +175,22 @@
 
 fun replay_proof sg clauses (clause_table, empty_id) =
 let
-	fun complete []      =
-		true
-	  | complete (x::xs) =
-		(isSome o Array.sub) (clauses, x) andalso complete xs
+	(* int -> unit *)
+	fun prove_clause id =
+		case Array.sub (clauses, id) of
+		  SOME _ =>
+			()
+		| NONE   =>
+			let
+				val ids = valOf (Inttab.lookup clause_table id)
+				val _   = map prove_clause ids
+			in
+				replay_chain sg clauses id ids
+			end
 
-	fun do_chains []        =
-		()
-	  | do_chains (ch::chs) =
-		let
-			val (idx, cls) = ch
-		in
-			if complete cls then (
-				replay_chain sg clauses idx cls;
-				do_chains chs
-			) else
-				do_chains (chs @ [ch])
-		end
+	val _ = counter := 0
 
-	val _ = do_chains (Inttab.dest clause_table)
+	val _ = prove_clause empty_id
 
 	val _ = if !trace_sat then
 			tracing (string_of_int (!counter) ^ " resolution steps total.")