src/HOL/Tools/sat_solver.ML
changeset 17527 5c25f27da4ca
parent 17494 e70600834f44
child 17541 6a52083b71c3
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Tue Sep 20 18:47:42 2005 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Tue Sep 20 19:38:35 2005 +0200
     1.3 @@ -586,6 +586,7 @@
     1.4  					  id::sep::ids =>
     1.5  						let
     1.6  							val _   = if !clause_offset = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"VAR:\".")
     1.7 +							val _   = if conflict_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".")
     1.8  							val cid = int_from_string id
     1.9  							val _   = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
    1.10  							val rs  = map int_from_string ids
    1.11 @@ -600,11 +601,12 @@
    1.12  					case toks of
    1.13  					  id::levsep::levid::valsep::valid::antesep::anteid::litsep::lits =>
    1.14  						let
    1.15 +							val _   = if conflict_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".")
    1.16  							(* set 'clause_offset' to the largest used clause ID *)
    1.17  							val _   = if !clause_offset = ~1 then clause_offset :=
    1.18  								(case Inttab.max_key clause_table of
    1.19  								  SOME id => id
    1.20 -								| NONE    => cnf_number_of_clauses (PropLogic.defcnf fm))
    1.21 +								| NONE    => cnf_number_of_clauses (PropLogic.defcnf fm) - 1  (* the first clause ID is 0, not 1 *))
    1.22  								else
    1.23  									()
    1.24  							val vid = int_from_string id
    1.25 @@ -629,7 +631,7 @@
    1.26  						in
    1.27  							(* update clause table *)
    1.28  							(Inttab.update_new (cid, rs) clause_table, conflict_id)
    1.29 -								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (antecedent for variable " ^ id ^ ") defined more than once.")
    1.30 +								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (derived from antecedent for variable " ^ id ^ ") already defined.")
    1.31  						end
    1.32  					| _ =>
    1.33  						raise INVALID_PROOF "File format error: \"VAR:\" followed by an insufficient number of tokens."
    1.34 @@ -637,13 +639,19 @@
    1.35  					case toks of
    1.36  					  id::sep::ids =>
    1.37  						let
    1.38 +							val _   = if conflict_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified."
    1.39  							val cid = int_from_string id
    1.40  							val _   = if sep = "==" then () else raise INVALID_PROOF ("File format error: \"==\" expected (" ^ quote sep ^ " encountered).")
    1.41 -							val _   = map int_from_string ids
    1.42 -							val _   = if conflict_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified."
    1.43 +							val ls  = map int_from_string ids
    1.44 +							(* the conflict clause must be resolved with the unit clauses *)
    1.45 +							(* for its literals to obtain the empty clause                *)
    1.46 +							val vids     = map (fn l => l div 2) ls
    1.47 +							val rs       = cid :: map (fn v => !clause_offset + v) vids
    1.48 +							val empty_id = getOpt (Inttab.max_key clause_table, ~1) + 1
    1.49  						in
    1.50 -							(* update conflict id *)
    1.51 -							(clause_table, cid)
    1.52 +							(* update clause table and conflict id *)
    1.53 +							(Inttab.update_new (empty_id, rs) clause_table, empty_id)
    1.54 +								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined.")
    1.55  						end
    1.56  					| _ =>
    1.57  						raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens."