src/HOL/Tools/sat_solver.ML
changeset 17621 afffade1697e
parent 17620 49568e5e0450
child 18678 dd0c569fa43d
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Sat Sep 24 02:53:08 2005 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Sat Sep 24 07:10:57 2005 +0200
     1.3 @@ -579,19 +579,19 @@
     1.4  			(* string list -> proof -> proof *)
     1.5  			fun process_tokens [] proof =
     1.6  				proof
     1.7 -			  | process_tokens (tok::toks) (clause_table, conflict_id) =
     1.8 +			  | process_tokens (tok::toks) (clause_table, empty_id) =
     1.9  				if tok="CL:" then (
    1.10  					case toks of
    1.11  					  id::sep::ids =>
    1.12  						let
    1.13  							val _   = if !clause_offset = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"VAR:\".")
    1.14 -							val _   = if conflict_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".")
    1.15 +							val _   = if empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".")
    1.16  							val cid = int_from_string id
    1.17  							val _   = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
    1.18  							val rs  = map int_from_string ids
    1.19  						in
    1.20  							(* update clause table *)
    1.21 -							(Inttab.update_new (cid, rs) clause_table, conflict_id)
    1.22 +							(Inttab.update_new (cid, rs) clause_table, empty_id)
    1.23  								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.")
    1.24  						end
    1.25  					| _ =>
    1.26 @@ -600,7 +600,7 @@
    1.27  					case toks of
    1.28  					  id::levsep::levid::valsep::valid::antesep::anteid::litsep::lits =>
    1.29  						let
    1.30 -							val _   = if conflict_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".")
    1.31 +							val _   = if empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".")
    1.32  							(* set 'clause_offset' to the largest used clause ID *)
    1.33  							val _   = if !clause_offset = ~1 then clause_offset :=
    1.34  								(case Inttab.max_key clause_table of
    1.35 @@ -629,7 +629,7 @@
    1.36  							val rs   = aid :: map (fn v => !clause_offset + v) vids
    1.37  						in
    1.38  							(* update clause table *)
    1.39 -							(Inttab.update_new (cid, rs) clause_table, conflict_id)
    1.40 +							(Inttab.update_new (cid, rs) clause_table, empty_id)
    1.41  								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (derived from antecedent for variable " ^ id ^ ") already defined.")
    1.42  						end
    1.43  					| _ =>
    1.44 @@ -638,19 +638,19 @@
    1.45  					case toks of
    1.46  					  id::sep::ids =>
    1.47  						let
    1.48 -							val _   = if conflict_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified."
    1.49 +							val _   = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified."
    1.50  							val cid = int_from_string id
    1.51  							val _   = if sep = "==" then () else raise INVALID_PROOF ("File format error: \"==\" expected (" ^ quote sep ^ " encountered).")
    1.52  							val ls  = map int_from_string ids
    1.53  							(* the conflict clause must be resolved with the unit clauses *)
    1.54  							(* for its literals to obtain the empty clause                *)
    1.55 -							val vids     = map (fn l => l div 2) ls
    1.56 -							val rs       = cid :: map (fn v => !clause_offset + v) vids
    1.57 -							val empty_id = getOpt (Inttab.max_key clause_table, ~1) + 1
    1.58 +							val vids         = map (fn l => l div 2) ls
    1.59 +							val rs           = cid :: map (fn v => !clause_offset + v) vids
    1.60 +							val new_empty_id = getOpt (Inttab.max_key clause_table, !clause_offset) + 1
    1.61  						in
    1.62  							(* update clause table and conflict id *)
    1.63 -							(Inttab.update_new (empty_id, rs) clause_table, empty_id)
    1.64 -								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined.")
    1.65 +							(Inttab.update_new (new_empty_id, rs) clause_table, new_empty_id)
    1.66 +								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int new_empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined.")
    1.67  						end
    1.68  					| _ =>
    1.69  						raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens."
    1.70 @@ -662,10 +662,10 @@
    1.71  			  | process_lines (l::ls) proof =
    1.72  				process_lines ls (process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l) proof)
    1.73  			(* proof *)
    1.74 -			val (clause_table, conflict_id) = process_lines proof_lines (Inttab.empty, ~1)
    1.75 -			val _                           = if conflict_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
    1.76 +			val (clause_table, empty_id) = process_lines proof_lines (Inttab.empty, ~1)
    1.77 +			val _                        = if empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
    1.78  		in
    1.79 -			SatSolver.UNSATISFIABLE (SOME (clause_table, conflict_id))
    1.80 +			SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id))
    1.81  		end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
    1.82  	| result =>
    1.83  		result