src/HOL/Tools/sat_solver.ML
changeset 20463 062c4e9bf3bb
parent 20441 a9034285b96b
child 21267 5294ecae6708
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Fri Sep 01 23:18:01 2006 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Sat Sep 02 01:10:10 2006 +0200
     1.3 @@ -764,24 +764,25 @@
     1.4  				| NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
     1.5  			)
     1.6  			(* parse the "resolve_trace" file *)
     1.7 -			(* int ref *)
     1.8  			val clause_offset = ref ~1
     1.9 -			(* string list -> proof -> proof *)
    1.10 -			fun process_tokens [] proof =
    1.11 -				proof
    1.12 -			  | process_tokens (tok::toks) (clause_table, empty_id) =
    1.13 +			val clause_table  = ref (Inttab.empty : int list Inttab.table)
    1.14 +			val empty_id      = ref ~1
    1.15 +			(* string list -> unit *)
    1.16 +			fun process_tokens [] =
    1.17 +				()
    1.18 +			  | process_tokens (tok::toks) =
    1.19  				if tok="CL:" then (
    1.20  					case toks of
    1.21  					  id::sep::ids =>
    1.22  						let
    1.23  							val _   = if !clause_offset = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"VAR:\".")
    1.24 -							val _   = if empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".")
    1.25 +							val _   = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".")
    1.26  							val cid = int_from_string id
    1.27  							val _   = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
    1.28  							val rs  = map int_from_string ids
    1.29  						in
    1.30  							(* update clause table *)
    1.31 -							(Inttab.update_new (cid, rs) clause_table, empty_id)
    1.32 +							clause_table := Inttab.update_new (cid, rs) (!clause_table)
    1.33  								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.")
    1.34  						end
    1.35  					| _ =>
    1.36 @@ -790,10 +791,10 @@
    1.37  					case toks of
    1.38  					  id::levsep::levid::valsep::valid::antesep::anteid::litsep::lits =>
    1.39  						let
    1.40 -							val _   = if empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".")
    1.41 +							val _   = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".")
    1.42  							(* set 'clause_offset' to the largest used clause ID *)
    1.43  							val _   = if !clause_offset = ~1 then clause_offset :=
    1.44 -								(case Inttab.max_key clause_table of
    1.45 +								(case Inttab.max_key (!clause_table) of
    1.46  								  SOME id => id
    1.47  								| NONE    => cnf_number_of_clauses (PropLogic.defcnf fm) - 1  (* the first clause ID is 0, not 1 *))
    1.48  								else
    1.49 @@ -819,7 +820,7 @@
    1.50  							val rs   = aid :: map (fn v => !clause_offset + v) vids
    1.51  						in
    1.52  							(* update clause table *)
    1.53 -							(Inttab.update_new (cid, rs) clause_table, empty_id)
    1.54 +							clause_table := Inttab.update_new (cid, rs) (!clause_table)
    1.55  								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (derived from antecedent for variable " ^ id ^ ") already defined.")
    1.56  						end
    1.57  					| _ =>
    1.58 @@ -828,7 +829,7 @@
    1.59  					case toks of
    1.60  					  id::sep::ids =>
    1.61  						let
    1.62 -							val _   = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified."
    1.63 +							val _   = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified."
    1.64  							val cid = int_from_string id
    1.65  							val _   = if sep = "==" then () else raise INVALID_PROOF ("File format error: \"==\" expected (" ^ quote sep ^ " encountered).")
    1.66  							val ls  = map int_from_string ids
    1.67 @@ -836,26 +837,29 @@
    1.68  							(* for its literals to obtain the empty clause                *)
    1.69  							val vids         = map (fn l => l div 2) ls
    1.70  							val rs           = cid :: map (fn v => !clause_offset + v) vids
    1.71 -							val new_empty_id = getOpt (Inttab.max_key clause_table, !clause_offset) + 1
    1.72 +							val new_empty_id = getOpt (Inttab.max_key (!clause_table), !clause_offset) + 1
    1.73  						in
    1.74  							(* update clause table and conflict id *)
    1.75 -							(Inttab.update_new (new_empty_id, rs) clause_table, new_empty_id)
    1.76 -								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.77 +							clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table)
    1.78 +								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.79 +							empty_id     := new_empty_id
    1.80  						end
    1.81  					| _ =>
    1.82  						raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens."
    1.83  				) else
    1.84  					raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
    1.85 -			(* string list -> proof -> proof *)
    1.86 -			fun process_lines [] proof =
    1.87 -				proof
    1.88 -			  | process_lines (l::ls) proof =
    1.89 -				process_lines ls (process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l) proof)
    1.90 +			(* string list -> unit *)
    1.91 +			fun process_lines [] =
    1.92 +				()
    1.93 +			  | process_lines (l::ls) = (
    1.94 +					process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l);
    1.95 +					process_lines ls
    1.96 +				)
    1.97  			(* proof *)
    1.98 -			val (clause_table, empty_id) = process_lines proof_lines (Inttab.empty, ~1)
    1.99 -			val _                        = if empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
   1.100 +			val _ = process_lines proof_lines
   1.101 +			val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
   1.102  		in
   1.103 -			SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id))
   1.104 +			SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id))
   1.105  		end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
   1.106  	| result =>
   1.107  		result