--- a/src/HOL/Tools/sat_solver.ML Fri Sep 01 23:18:01 2006 +0200
+++ b/src/HOL/Tools/sat_solver.ML Sat Sep 02 01:10:10 2006 +0200
@@ -764,24 +764,25 @@
| NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
)
(* parse the "resolve_trace" file *)
- (* int ref *)
val clause_offset = ref ~1
- (* string list -> proof -> proof *)
- fun process_tokens [] proof =
- proof
- | process_tokens (tok::toks) (clause_table, empty_id) =
+ val clause_table = ref (Inttab.empty : int list Inttab.table)
+ val empty_id = ref ~1
+ (* string list -> unit *)
+ fun process_tokens [] =
+ ()
+ | process_tokens (tok::toks) =
if tok="CL:" then (
case toks of
id::sep::ids =>
let
val _ = if !clause_offset = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"VAR:\".")
- val _ = if empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".")
+ val _ = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".")
val cid = int_from_string id
val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
val rs = map int_from_string ids
in
(* update clause table *)
- (Inttab.update_new (cid, rs) clause_table, empty_id)
+ clause_table := Inttab.update_new (cid, rs) (!clause_table)
handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.")
end
| _ =>
@@ -790,10 +791,10 @@
case toks of
id::levsep::levid::valsep::valid::antesep::anteid::litsep::lits =>
let
- val _ = if empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".")
+ val _ = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".")
(* set 'clause_offset' to the largest used clause ID *)
val _ = if !clause_offset = ~1 then clause_offset :=
- (case Inttab.max_key clause_table of
+ (case Inttab.max_key (!clause_table) of
SOME id => id
| NONE => cnf_number_of_clauses (PropLogic.defcnf fm) - 1 (* the first clause ID is 0, not 1 *))
else
@@ -819,7 +820,7 @@
val rs = aid :: map (fn v => !clause_offset + v) vids
in
(* update clause table *)
- (Inttab.update_new (cid, rs) clause_table, empty_id)
+ clause_table := Inttab.update_new (cid, rs) (!clause_table)
handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (derived from antecedent for variable " ^ id ^ ") already defined.")
end
| _ =>
@@ -828,7 +829,7 @@
case toks of
id::sep::ids =>
let
- val _ = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified."
+ val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified."
val cid = int_from_string id
val _ = if sep = "==" then () else raise INVALID_PROOF ("File format error: \"==\" expected (" ^ quote sep ^ " encountered).")
val ls = map int_from_string ids
@@ -836,26 +837,29 @@
(* for its literals to obtain the empty clause *)
val vids = map (fn l => l div 2) ls
val rs = cid :: map (fn v => !clause_offset + v) vids
- val new_empty_id = getOpt (Inttab.max_key clause_table, !clause_offset) + 1
+ val new_empty_id = getOpt (Inttab.max_key (!clause_table), !clause_offset) + 1
in
(* update clause table and conflict id *)
- (Inttab.update_new (new_empty_id, rs) clause_table, new_empty_id)
- handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int new_empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined.")
+ clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table)
+ handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int new_empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined.");
+ empty_id := new_empty_id
end
| _ =>
raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens."
) else
raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
- (* string list -> proof -> proof *)
- fun process_lines [] proof =
- proof
- | process_lines (l::ls) proof =
- process_lines ls (process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l) proof)
+ (* string list -> unit *)
+ fun process_lines [] =
+ ()
+ | process_lines (l::ls) = (
+ process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l);
+ process_lines ls
+ )
(* proof *)
- val (clause_table, empty_id) = process_lines proof_lines (Inttab.empty, ~1)
- val _ = if empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
+ val _ = process_lines proof_lines
+ val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
in
- SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id))
+ SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id))
end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
| result =>
result