interpreters for fst and snd added
authorwebertj
Thu Nov 09 18:48:45 2006 +0100 (2006-11-09)
changeset 212675294ecae6708
parent 21266 288a504c24d6
child 21268 7a6299a17386
interpreters for fst and snd added
src/HOL/Tools/refute.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/Tools/sat_solver.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Nov 09 16:14:43 2006 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Nov 09 18:48:45 2006 +0100
     1.3 @@ -628,6 +628,8 @@
     1.4  			| Const ("List.op @", T)          => collect_type_axioms (axs, T)
     1.5  			| Const ("Lfp.lfp", T)            => collect_type_axioms (axs, T)
     1.6  			| Const ("Gfp.gfp", T)            => collect_type_axioms (axs, T)
     1.7 +			| Const ("fst", T)                => collect_type_axioms (axs, T)
     1.8 +			| Const ("snd", T)                => collect_type_axioms (axs, T)
     1.9  			(* simply-typed lambda calculus *)
    1.10  			| Const (s, T)                    =>
    1.11  				let
    1.12 @@ -2376,6 +2378,46 @@
    1.13  		| _ =>
    1.14  			NONE;
    1.15  
    1.16 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
    1.17 +
    1.18 +	(* only an optimization: 'fst' could in principle be interpreted with     *)
    1.19 +	(* interpreters available already (using its definition), but the code    *)
    1.20 +	(* below is more efficient                                                *)
    1.21 +
    1.22 +	fun Product_Type_fst_interpreter thy model args t =
    1.23 +		case t of
    1.24 +		  Const ("fst", Type ("fun", [Type ("*", [T, U]), _])) =>
    1.25 +			let
    1.26 +				val (iT, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
    1.27 +				val is_T       = make_constants iT
    1.28 +				val (iU, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", U))
    1.29 +				val size_U     = size_of_type iU
    1.30 +			in
    1.31 +				SOME (Node (List.concat (map (replicate size_U) is_T)), model, args)
    1.32 +			end
    1.33 +		| _ =>
    1.34 +			NONE;
    1.35 +
    1.36 +	(* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *)
    1.37 +
    1.38 +	(* only an optimization: 'snd' could in principle be interpreted with     *)
    1.39 +	(* interpreters available already (using its definition), but the code    *)
    1.40 +	(* below is more efficient                                                *)
    1.41 +
    1.42 +	fun Product_Type_snd_interpreter thy model args t =
    1.43 +		case t of
    1.44 +		  Const ("snd", Type ("fun", [Type ("*", [T, U]), _])) =>
    1.45 +			let
    1.46 +				val (iT, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", T))
    1.47 +				val size_T     = size_of_type iT
    1.48 +				val (iU, _, _) = interpret thy model {maxvars=0, def_eq=false, next_idx=1, bounds=[], wellformed=True} (Free ("dummy", U))
    1.49 +				val is_U       = make_constants iU
    1.50 +			in
    1.51 +				SOME (Node (List.concat (replicate size_T is_U)), model, args)
    1.52 +			end
    1.53 +		| _ =>
    1.54 +			NONE;
    1.55 +
    1.56  
    1.57  (* ------------------------------------------------------------------------- *)
    1.58  (* PRINTERS                                                                  *)
    1.59 @@ -2616,6 +2658,8 @@
    1.60  		 add_interpreter "List.op @" List_append_interpreter #>
    1.61  		 add_interpreter "Lfp.lfp" Lfp_lfp_interpreter #>
    1.62  		 add_interpreter "Gfp.gfp" Gfp_gfp_interpreter #>
    1.63 +		 add_interpreter "fst" Product_Type_fst_interpreter #>
    1.64 +		 add_interpreter "snd" Product_Type_snd_interpreter #>
    1.65  		 add_printer "stlc" stlc_printer #>
    1.66  		 add_printer "set"  set_printer #>
    1.67  		 add_printer "IDT"  IDT_printer;
     2.1 --- a/src/HOL/Tools/sat_funcs.ML	Thu Nov 09 16:14:43 2006 +0100
     2.2 +++ b/src/HOL/Tools/sat_funcs.ML	Thu Nov 09 18:48:45 2006 +0100
     2.3 @@ -51,9 +51,10 @@
     2.4  
     2.5  signature SAT =
     2.6  sig
     2.7 -	val trace_sat  : bool ref    (* print trace messages *)
     2.8 -	val solver     : string ref  (* name of SAT solver to be used *)
     2.9 -	val counter    : int ref     (* number of resolution steps during last proof replay *)
    2.10 +	val trace_sat  : bool ref    (* input: print trace messages *)
    2.11 +	val solver     : string ref  (* input: name of SAT solver to be used *)
    2.12 +	val counter    : int ref     (* output: number of resolution steps during last proof replay *)
    2.13 +	val rawsat_thm : cterm list -> thm
    2.14  	val rawsat_tac : int -> Tactical.tactic
    2.15  	val sat_tac    : int -> Tactical.tactic
    2.16  	val satx_tac   : int -> Tactical.tactic
    2.17 @@ -69,7 +70,7 @@
    2.18  val counter = ref 0;
    2.19  
    2.20  (* Thm.thm *)
    2.21 -val resolution_thm =  (* "[| P ==> False; ~P ==> False |] ==> False" *)
    2.22 +val resolution_thm =  (* "[| ?P ==> False; ~ ?P ==> False |] ==> False" *)
    2.23  	let
    2.24  		val cterm = cterm_of (the_context ())
    2.25  		val Q     = Var (("Q", 0), HOLogic.boolT)
    2.26 @@ -256,52 +257,70 @@
    2.27    | string_of_prop_formula (PropLogic.And (fm1, fm2)) = "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
    2.28  
    2.29  (* ------------------------------------------------------------------------- *)
    2.30 -(* rawsat_thm: run external SAT solver with the given clauses.  Reconstructs *)
    2.31 -(*      a proof from the resulting proof trace of the SAT solver.  Each      *)
    2.32 -(*      premise in 'prems' that is not a clause is ignored, and the theorem  *)
    2.33 -(*      returned is just "False" (with some clauses as hyps).                *)
    2.34 +(* take_prefix:                                                              *)
    2.35 +(*      take_prefix n [x_1, ..., x_k] = ([x_1, ..., x_n], [x_n+1, ..., x_k]) *)
    2.36  (* ------------------------------------------------------------------------- *)
    2.37  
    2.38 -(* Thm.thm list -> Thm.thm *)
    2.39 +(* int -> 'a list -> 'a list * 'a list *)
    2.40 +
    2.41 +fun take_prefix n xs =
    2.42 +let
    2.43 +	fun take 0 (rxs, xs)      = (rev rxs, xs)
    2.44 +	  | take _ (rxs, [])      = (rev rxs, [])
    2.45 +	  | take n (rxs, x :: xs) = take (n-1) (x :: rxs, xs)
    2.46 +in
    2.47 +	take n ([], xs)
    2.48 +end;
    2.49  
    2.50 -fun rawsat_thm prems =
    2.51 +(* ------------------------------------------------------------------------- *)
    2.52 +(* rawsat_thm: run external SAT solver with the given clauses.  Reconstructs *)
    2.53 +(*      a proof from the resulting proof trace of the SAT solver.  The       *)
    2.54 +(*      theorem returned is just "False" (with some of the given clauses as  *)
    2.55 +(*      hyps).                                                               *)
    2.56 +(* ------------------------------------------------------------------------- *)
    2.57 +
    2.58 +(* Thm.cterm list -> Thm.thm *)
    2.59 +
    2.60 +fun rawsat_thm clauses =
    2.61  let
    2.62  	(* remove premises that equal "True" *)
    2.63 -	val non_triv_prems    = filter (fn thm =>
    2.64 -		(not_equal HOLogic.true_const o HOLogic.dest_Trueprop o prop_of) thm
    2.65 -			handle TERM ("dest_Trueprop", _) => true) prems
    2.66 +	val clauses' = filter (fn clause =>
    2.67 +		(not_equal HOLogic.true_const o HOLogic.dest_Trueprop o term_of) clause
    2.68 +			handle TERM ("dest_Trueprop", _) => true) clauses
    2.69  	(* remove non-clausal premises -- of course this shouldn't actually   *)
    2.70 -	(* remove anything as long as 'rawsat_thm' is only called after the   *)
    2.71 +	(* remove anything as long as 'rawsat_tac' is only called after the   *)
    2.72  	(* premises have been converted to clauses                            *)
    2.73 -	val clauses           = filter (fn thm =>
    2.74 -		((cnf.is_clause o HOLogic.dest_Trueprop o prop_of) thm handle TERM ("dest_Trueprop", _) => false)
    2.75 -		orelse (warning ("Ignoring non-clausal premise " ^ (string_of_cterm o cprop_of) thm); false)) non_triv_prems
    2.76 +	val clauses'' = filter (fn clause =>
    2.77 +		((cnf.is_clause o HOLogic.dest_Trueprop o term_of) clause
    2.78 +			handle TERM ("dest_Trueprop", _) => false)
    2.79 +		orelse (
    2.80 +			warning ("Ignoring non-clausal premise " ^ string_of_cterm clause);
    2.81 +			false)) clauses'
    2.82  	(* remove trivial clauses -- this is necessary because zChaff removes *)
    2.83  	(* trivial clauses during preprocessing, and otherwise our clause     *)
    2.84  	(* numbering would be off                                             *)
    2.85 -	val non_triv_clauses  = filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o prop_of) clauses
    2.86 -	val _                 = if !trace_sat then
    2.87 -			tracing ("Non-trivial clauses:\n" ^ space_implode "\n" (map (string_of_cterm o cprop_of) non_triv_clauses))
    2.88 +	val clauses''' = filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o term_of) clauses''
    2.89 +	val _ = if !trace_sat then
    2.90 +			tracing ("Non-trivial clauses:\n" ^ space_implode "\n" (map string_of_cterm clauses'''))
    2.91  		else ()
    2.92  	(* translate clauses from HOL terms to PropLogic.prop_formula *)
    2.93 -	val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o prop_of) non_triv_clauses Termtab.empty
    2.94 -	val _                 = if !trace_sat then
    2.95 +	val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o term_of) clauses''' Termtab.empty
    2.96 +	val _ = if !trace_sat then
    2.97  			tracing ("Invoking SAT solver on clauses:\n" ^ space_implode "\n" (map string_of_prop_formula fms))
    2.98  		else ()
    2.99  	val fm                = PropLogic.all fms
   2.100  	(* unit -> Thm.thm *)
   2.101 -	fun make_quick_and_dirty_thm () = (
   2.102 -		if !trace_sat then
   2.103 -			tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
   2.104 -		else ();
   2.105 -		(* of course just returning "False" is unsound; what we should return *)
   2.106 -		(* instead is "False" with all 'non_triv_clauses' as hyps -- but this *)
   2.107 -		(* might be rather slow, and it makes no real difference as long as   *)
   2.108 -		(* 'rawsat_thm' is only called from 'rawsat_tac'                      *)
   2.109 -		SkipProof.make_thm (the_context ()) (HOLogic.Trueprop $ HOLogic.false_const)
   2.110 -	)
   2.111 +	fun make_quick_and_dirty_thm () =
   2.112 +	let
   2.113 +		val _ = if !trace_sat then
   2.114 +				tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
   2.115 +			else ()
   2.116 +		val False_thm = SkipProof.make_thm (the_context ()) (HOLogic.Trueprop $ HOLogic.false_const)
   2.117 +	in
   2.118 +		fold Thm.weaken clauses''' False_thm
   2.119 +	end
   2.120  in
   2.121 -	case SatSolver.invoke_solver (!solver) fm of
   2.122 +	case (tracing "Invoking solver"; timeap (SatSolver.invoke_solver (!solver)) fm) of  (*TODO*)
   2.123  	  SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => (
   2.124  		if !trace_sat then
   2.125  			tracing ("Proof trace from SAT solver:\n" ^
   2.126 @@ -312,35 +331,28 @@
   2.127  			make_quick_and_dirty_thm ()
   2.128  		else
   2.129  			let
   2.130 -				(* optimization: convert the given clauses from "[c_i] |- c_i" to *)
   2.131 -				(* "[c_1 && ... && c_n] |- c_i"; this avoids accumulation of      *)
   2.132 -				(* hypotheses during resolution                                   *)
   2.133 +				(* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i";  *)
   2.134 +				(*               this avoids accumulation of hypotheses during resolution    *)
   2.135 +				(* [c_1, ..., c_n] |- c_1 && ... && c_n *)
   2.136 +				val _           = tracing "Conjunction.intr_list"  (*TODO*)
   2.137 +				val clauses_thm = timeap Conjunction.intr_list (map Thm.assume clauses''')  (*TODO*)
   2.138  				(* [c_1 && ... && c_n] |- c_1 && ... && c_n *)
   2.139 -				val cnf_cterm = Conjunction.mk_conjunction_list (map cprop_of non_triv_clauses)
   2.140 +				val cnf_cterm = cprop_of clauses_thm
   2.141  				val cnf_thm   = Thm.assume cnf_cterm
   2.142 -				(* cf. Conjunction.elim_list *)
   2.143 -				fun right_elim_list th =
   2.144 -					let val (th1, th2) = Conjunction.elim th
   2.145 -					in th1 :: right_elim_list th2 end handle THM _ => [th]
   2.146  				(* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
   2.147 -				val converted_clauses = right_elim_list cnf_thm
   2.148 +				val _           = tracing "Conjunction.elim_list"  (*TODO*)
   2.149 +				val cnf_clauses = timeap Conjunction.elim_list cnf_thm  (*TODO*)
   2.150  				(* initialize the clause array with the given clauses *)
   2.151  				val max_idx    = valOf (Inttab.max_key clause_table)
   2.152  				val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
   2.153 -				val _          = fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1)) converted_clauses 0
   2.154 +				val _          = fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1)) cnf_clauses 0
   2.155  				(* replay the proof to derive the empty clause *)
   2.156  				(* [c_1 && ... && c_n] |- False *)
   2.157 -				val FalseThm   = replay_proof atom_table clause_arr (clause_table, empty_id)
   2.158 +				val _       = tracing "replay_proof"  (*TODO*)
   2.159 +				val raw_thm = timeap (replay_proof atom_table clause_arr) (clause_table, empty_id)  (*TODO*)
   2.160  			in
   2.161 -				(* convert the &&-hyp back to the original clauses format *)
   2.162 -				FalseThm
   2.163 -				(* [] |- c_1 && ... && c_n ==> False *)
   2.164 -				|> Thm.implies_intr cnf_cterm
   2.165 -				(* c_1 ==> ... ==> c_n ==> False *)
   2.166 -				|> Conjunction.curry ~1
   2.167  				(* [c_1, ..., c_n] |- False *)
   2.168 -				|> (fn thm => fold (fn cprem => fn thm' =>
   2.169 -					Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm)
   2.170 +				Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm
   2.171  			end)
   2.172  	| SatSolver.UNSATISFIABLE NONE =>
   2.173  		if !quick_and_dirty then (
   2.174 @@ -377,7 +389,7 @@
   2.175  
   2.176  (* int -> Tactical.tactic *)
   2.177  
   2.178 -fun rawsat_tac i = METAHYPS (fn prems => rtac (rawsat_thm prems) 1) i;
   2.179 +fun rawsat_tac i = METAHYPS (fn prems => rtac (rawsat_thm (map cprop_of prems)) 1) i;
   2.180  
   2.181  (* ------------------------------------------------------------------------- *)
   2.182  (* pre_cnf_tac: converts the i-th subgoal                                    *)
     3.1 --- a/src/HOL/Tools/sat_solver.ML	Thu Nov 09 16:14:43 2006 +0100
     3.2 +++ b/src/HOL/Tools/sat_solver.ML	Thu Nov 09 18:48:45 2006 +0100
     3.3 @@ -1,7 +1,7 @@
     3.4  (*  Title:      HOL/Tools/sat_solver.ML
     3.5      ID:         $Id$
     3.6      Author:     Tjark Weber
     3.7 -    Copyright   2004-2005
     3.8 +    Copyright   2004-2006
     3.9  
    3.10  Interface to external SAT solvers, and (simple) built-in SAT solvers.
    3.11  *)
    3.12 @@ -580,25 +580,60 @@
    3.13  	  SatSolver.UNSATISFIABLE NONE =>
    3.14  		(let
    3.15  			(* string list *)
    3.16 -			val proof_lines = ((split_lines o File.read) proofpath)
    3.17 +			val proof_lines = (split_lines o File.read) proofpath
    3.18  				handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\""
    3.19 -			(* a simple representation of the CNF formula as list of clauses (paired with their ID), *)
    3.20 -			(* where each clause is a sorted list of literals, where each literal is an int          *)
    3.21 -			(* removes duplicates from an ordered list *)
    3.22 -			(* int list -> int list *)
    3.23 -			fun remove_dups []             = []
    3.24 -			  | remove_dups [x]            = [x]
    3.25 -			  | remove_dups (x :: y :: xs) = if x = y then remove_dups (y :: xs) else x :: remove_dups (y :: xs)
    3.26 +			(* representation of clauses as ordered lists of literals (with duplicates removed) *)
    3.27  			(* prop_formula -> int list *)
    3.28 -			fun clause_to_lit_list (PropLogic.Or (fm1, fm2))             = clause_to_lit_list fm1 @ clause_to_lit_list fm2
    3.29 -			  | clause_to_lit_list (PropLogic.BoolVar i)                 = [i]
    3.30 -			  | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) = [~i]
    3.31 -			  | clause_to_lit_list _                 = raise INVALID_PROOF "Error: invalid clause in CNF formula."
    3.32 -			(* prop_formula -> int list list *)
    3.33 -			fun cnf_to_clause_list (PropLogic.And (fm1, fm2)) = cnf_to_clause_list fm1 @ cnf_to_clause_list fm2
    3.34 -			  | cnf_to_clause_list fm                         = [(remove_dups o sort int_ord o clause_to_lit_list) fm]
    3.35 -			(* (int list * int) list * int *)
    3.36 -			val (clauses, length_clauses) = fold_map (fn clause => fn n => ((clause, n), n+1)) (cnf_to_clause_list cnf) 0
    3.37 +			fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) =
    3.38 +				OrdList.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2)
    3.39 +			  | clause_to_lit_list (PropLogic.BoolVar i) =
    3.40 +				[i]
    3.41 +			  | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) =
    3.42 +				[~i]
    3.43 +			  | clause_to_lit_list _ =
    3.44 +				raise INVALID_PROOF "Error: invalid clause in CNF formula."
    3.45 +			(* prop_formula -> int *)
    3.46 +			fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) =
    3.47 +				cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
    3.48 +			  | cnf_number_of_clauses _ =
    3.49 +				1
    3.50 +			val number_of_clauses = cnf_number_of_clauses cnf
    3.51 +			(* int list array *)
    3.52 +			val clauses = Array.array (number_of_clauses, [])
    3.53 +			(* initialize the 'clauses' array *)
    3.54 +			(* prop_formula * int -> int *)
    3.55 +			fun init_array (PropLogic.And (fm1, fm2), n) =
    3.56 +				init_array (fm2, init_array (fm1, n))
    3.57 +			  | init_array (fm, n) =
    3.58 +				(Array.update (clauses, n, clause_to_lit_list fm); n+1)
    3.59 +			val _ = init_array (cnf, 0)
    3.60 +			(* optimization for the common case where MiniSat "R"s clauses in their *)
    3.61 +			(* original order:                                                      *)
    3.62 +			val last_ref_clause = ref (number_of_clauses - 1)
    3.63 +			(* search the 'clauses' array for the given list of literals 'lits', *)
    3.64 +			(* starting at index '!last_ref_clause + 1'                          *)
    3.65 +			(* int list -> int option *)
    3.66 +			fun original_clause_id lits =
    3.67 +			let
    3.68 +				fun original_clause_id_from index =
    3.69 +					if index = number_of_clauses then
    3.70 +						(* search from beginning again *)
    3.71 +						original_clause_id_from 0
    3.72 +					(* both 'lits' and the list of literals used in 'clauses' are sorted, so *)
    3.73 +					(* testing for equality should suffice -- barring duplicate literals     *)
    3.74 +					else if Array.sub (clauses, index) = lits then (
    3.75 +						(* success *)
    3.76 +						last_ref_clause := index;
    3.77 +						SOME index
    3.78 +					) else if index = !last_ref_clause then
    3.79 +						(* failure *)
    3.80 +						NONE
    3.81 +					else
    3.82 +						(* continue search *)
    3.83 +						original_clause_id_from (index + 1)
    3.84 +			in
    3.85 +				original_clause_id_from (!last_ref_clause + 1)
    3.86 +			end
    3.87  			(* string -> int *)
    3.88  			fun int_from_string s = (
    3.89  				case Int.fromString s of
    3.90 @@ -606,6 +641,8 @@
    3.91  				| NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
    3.92  			)
    3.93  			(* parse the proof file *)
    3.94 +			val clause_table  = ref (Inttab.empty : int list Inttab.table)
    3.95 +			val empty_id      = ref ~1
    3.96  			(* contains a mapping from clause IDs as used by MiniSat to clause IDs in *)
    3.97  			(* our proof format, where original clauses are numbered starting from 0  *)
    3.98  			val clause_id_map = ref (Inttab.empty : int Inttab.table)
    3.99 @@ -614,30 +651,27 @@
   3.100  				  SOME id' => id'
   3.101  				| NONE     => raise INVALID_PROOF ("Clause ID " ^ Int.toString id ^ " used, but not defined.")
   3.102  			)
   3.103 -			val next_id = ref (length_clauses - 1)
   3.104 -			(* string list -> proof -> proof *)
   3.105 -			fun process_tokens [] proof =
   3.106 -				proof
   3.107 -			  | process_tokens (tok::toks) (clause_table, empty_id) =
   3.108 +			val next_id = ref (number_of_clauses - 1)
   3.109 +			(* string list -> unit *)
   3.110 +			fun process_tokens [] =
   3.111 +				()
   3.112 +			  | process_tokens (tok::toks) =
   3.113  				if tok="R" then (
   3.114  					case toks of
   3.115  					  id::sep::lits =>
   3.116  						let
   3.117 -							val _        = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"."
   3.118 +							val _        = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"."
   3.119  							val cid      = int_from_string id
   3.120  							val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
   3.121  							val ls       = sort int_ord (map int_from_string lits)
   3.122 -							val proof_id = (* both 'ls' and the list of literals used as key in 'clauses' are sorted, *)
   3.123 -							               (* so testing for equality should suffice -- barring duplicate literals    *)
   3.124 -							               case AList.lookup (op =) clauses ls of
   3.125 +							val proof_id = case original_clause_id ls of
   3.126  							                 SOME orig_id => orig_id
   3.127 -						                   | NONE         => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.")
   3.128 +							               | NONE         => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.")
   3.129 +						in
   3.130  							(* extend the mapping of clause IDs with this newly defined ID *)
   3.131 -							val _        = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
   3.132 -							                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").")
   3.133 -						in
   3.134 +							clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
   3.135 +								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").")
   3.136  							(* the proof itself doesn't change *)
   3.137 -							(clause_table, empty_id)
   3.138  						end
   3.139  					| _ =>
   3.140  						raise INVALID_PROOF "File format error: \"R\" followed by an insufficient number of tokens."
   3.141 @@ -645,7 +679,7 @@
   3.142  					case toks of
   3.143  					  id::sep::ids =>
   3.144  						let
   3.145 -							val _        = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"."
   3.146 +							val _        = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"."
   3.147  							val cid      = int_from_string id
   3.148  							val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
   3.149  							(* ignore the pivot literals in MiniSat's trace *)
   3.150 @@ -659,7 +693,7 @@
   3.151  							                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").")
   3.152  						in
   3.153  							(* update clause table *)
   3.154 -							(Inttab.update_new (proof_id, rs) clause_table, empty_id)
   3.155 +							clause_table := Inttab.update_new (proof_id, rs) (!clause_table)
   3.156  								handle Inttab.DUP _ => raise INVALID_PROOF ("Error: internal ID for clause " ^ id ^ " already used.")
   3.157  						end
   3.158  					| _ =>
   3.159 @@ -668,11 +702,11 @@
   3.160  					case toks of
   3.161  					  [id] =>
   3.162  						let
   3.163 -							val _ = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"."
   3.164 +							val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"."
   3.165  							val _ = sat_to_proof (int_from_string id)
   3.166  						in
   3.167  							(* simply ignore "D" *)
   3.168 -							(clause_table, empty_id)
   3.169 +							()
   3.170  						end
   3.171  					| _ =>
   3.172  						raise INVALID_PROOF "File format error: \"D\" followed by an illegal number of tokens."
   3.173 @@ -680,27 +714,29 @@
   3.174  					case toks of
   3.175  					  [id1, id2] =>
   3.176  						let
   3.177 -							val _            = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement."
   3.178 +							val _            = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement."
   3.179  							val _            = sat_to_proof (int_from_string id1)
   3.180  							val new_empty_id = sat_to_proof (int_from_string id2)
   3.181  						in
   3.182  							(* update conflict id *)
   3.183 -							(clause_table, new_empty_id)
   3.184 +							empty_id := new_empty_id
   3.185  						end
   3.186  					| _ =>
   3.187  						raise INVALID_PROOF "File format error: \"X\" followed by an illegal number of tokens."
   3.188  				) else
   3.189  					raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
   3.190 -			(* string list -> proof -> proof *)
   3.191 -			fun process_lines [] proof =
   3.192 -				proof
   3.193 -			  | process_lines (l::ls) proof =
   3.194 -				process_lines ls (process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l) proof)
   3.195 +			(* string list -> unit *)
   3.196 +			fun process_lines [] =
   3.197 +				()
   3.198 +			  | process_lines (l::ls) = (
   3.199 +					process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l);
   3.200 +					process_lines ls
   3.201 +				)
   3.202  			(* proof *)
   3.203 -			val (clause_table, empty_id) = process_lines proof_lines (Inttab.empty, ~1)
   3.204 -			val _                        = if empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
   3.205 +			val _ = process_lines proof_lines
   3.206 +			val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
   3.207  		in
   3.208 -			SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id))
   3.209 +			SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id))
   3.210  		end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
   3.211  	| result =>
   3.212  		result
   3.213 @@ -856,7 +892,8 @@
   3.214  					process_lines ls
   3.215  				)
   3.216  			(* proof *)
   3.217 -			val _ = process_lines proof_lines
   3.218 +			val _ = tracing "process_lines"  (*TODO*)
   3.219 +			val _ = timeap process_lines proof_lines  (*TODO*)
   3.220  			val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
   3.221  		in
   3.222  			SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id))