src/HOL/Tools/sat_solver.ML
changeset 21267 5294ecae6708
parent 20463 062c4e9bf3bb
child 21268 7a6299a17386
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Thu Nov 09 16:14:43 2006 +0100
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Thu Nov 09 18:48:45 2006 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      HOL/Tools/sat_solver.ML
     1.5      ID:         $Id$
     1.6      Author:     Tjark Weber
     1.7 -    Copyright   2004-2005
     1.8 +    Copyright   2004-2006
     1.9  
    1.10  Interface to external SAT solvers, and (simple) built-in SAT solvers.
    1.11  *)
    1.12 @@ -580,25 +580,60 @@
    1.13  	  SatSolver.UNSATISFIABLE NONE =>
    1.14  		(let
    1.15  			(* string list *)
    1.16 -			val proof_lines = ((split_lines o File.read) proofpath)
    1.17 +			val proof_lines = (split_lines o File.read) proofpath
    1.18  				handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\""
    1.19 -			(* a simple representation of the CNF formula as list of clauses (paired with their ID), *)
    1.20 -			(* where each clause is a sorted list of literals, where each literal is an int          *)
    1.21 -			(* removes duplicates from an ordered list *)
    1.22 -			(* int list -> int list *)
    1.23 -			fun remove_dups []             = []
    1.24 -			  | remove_dups [x]            = [x]
    1.25 -			  | remove_dups (x :: y :: xs) = if x = y then remove_dups (y :: xs) else x :: remove_dups (y :: xs)
    1.26 +			(* representation of clauses as ordered lists of literals (with duplicates removed) *)
    1.27  			(* prop_formula -> int list *)
    1.28 -			fun clause_to_lit_list (PropLogic.Or (fm1, fm2))             = clause_to_lit_list fm1 @ clause_to_lit_list fm2
    1.29 -			  | clause_to_lit_list (PropLogic.BoolVar i)                 = [i]
    1.30 -			  | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) = [~i]
    1.31 -			  | clause_to_lit_list _                 = raise INVALID_PROOF "Error: invalid clause in CNF formula."
    1.32 -			(* prop_formula -> int list list *)
    1.33 -			fun cnf_to_clause_list (PropLogic.And (fm1, fm2)) = cnf_to_clause_list fm1 @ cnf_to_clause_list fm2
    1.34 -			  | cnf_to_clause_list fm                         = [(remove_dups o sort int_ord o clause_to_lit_list) fm]
    1.35 -			(* (int list * int) list * int *)
    1.36 -			val (clauses, length_clauses) = fold_map (fn clause => fn n => ((clause, n), n+1)) (cnf_to_clause_list cnf) 0
    1.37 +			fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) =
    1.38 +				OrdList.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2)
    1.39 +			  | clause_to_lit_list (PropLogic.BoolVar i) =
    1.40 +				[i]
    1.41 +			  | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) =
    1.42 +				[~i]
    1.43 +			  | clause_to_lit_list _ =
    1.44 +				raise INVALID_PROOF "Error: invalid clause in CNF formula."
    1.45 +			(* prop_formula -> int *)
    1.46 +			fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) =
    1.47 +				cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
    1.48 +			  | cnf_number_of_clauses _ =
    1.49 +				1
    1.50 +			val number_of_clauses = cnf_number_of_clauses cnf
    1.51 +			(* int list array *)
    1.52 +			val clauses = Array.array (number_of_clauses, [])
    1.53 +			(* initialize the 'clauses' array *)
    1.54 +			(* prop_formula * int -> int *)
    1.55 +			fun init_array (PropLogic.And (fm1, fm2), n) =
    1.56 +				init_array (fm2, init_array (fm1, n))
    1.57 +			  | init_array (fm, n) =
    1.58 +				(Array.update (clauses, n, clause_to_lit_list fm); n+1)
    1.59 +			val _ = init_array (cnf, 0)
    1.60 +			(* optimization for the common case where MiniSat "R"s clauses in their *)
    1.61 +			(* original order:                                                      *)
    1.62 +			val last_ref_clause = ref (number_of_clauses - 1)
    1.63 +			(* search the 'clauses' array for the given list of literals 'lits', *)
    1.64 +			(* starting at index '!last_ref_clause + 1'                          *)
    1.65 +			(* int list -> int option *)
    1.66 +			fun original_clause_id lits =
    1.67 +			let
    1.68 +				fun original_clause_id_from index =
    1.69 +					if index = number_of_clauses then
    1.70 +						(* search from beginning again *)
    1.71 +						original_clause_id_from 0
    1.72 +					(* both 'lits' and the list of literals used in 'clauses' are sorted, so *)
    1.73 +					(* testing for equality should suffice -- barring duplicate literals     *)
    1.74 +					else if Array.sub (clauses, index) = lits then (
    1.75 +						(* success *)
    1.76 +						last_ref_clause := index;
    1.77 +						SOME index
    1.78 +					) else if index = !last_ref_clause then
    1.79 +						(* failure *)
    1.80 +						NONE
    1.81 +					else
    1.82 +						(* continue search *)
    1.83 +						original_clause_id_from (index + 1)
    1.84 +			in
    1.85 +				original_clause_id_from (!last_ref_clause + 1)
    1.86 +			end
    1.87  			(* string -> int *)
    1.88  			fun int_from_string s = (
    1.89  				case Int.fromString s of
    1.90 @@ -606,6 +641,8 @@
    1.91  				| NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
    1.92  			)
    1.93  			(* parse the proof file *)
    1.94 +			val clause_table  = ref (Inttab.empty : int list Inttab.table)
    1.95 +			val empty_id      = ref ~1
    1.96  			(* contains a mapping from clause IDs as used by MiniSat to clause IDs in *)
    1.97  			(* our proof format, where original clauses are numbered starting from 0  *)
    1.98  			val clause_id_map = ref (Inttab.empty : int Inttab.table)
    1.99 @@ -614,30 +651,27 @@
   1.100  				  SOME id' => id'
   1.101  				| NONE     => raise INVALID_PROOF ("Clause ID " ^ Int.toString id ^ " used, but not defined.")
   1.102  			)
   1.103 -			val next_id = ref (length_clauses - 1)
   1.104 -			(* string list -> proof -> proof *)
   1.105 -			fun process_tokens [] proof =
   1.106 -				proof
   1.107 -			  | process_tokens (tok::toks) (clause_table, empty_id) =
   1.108 +			val next_id = ref (number_of_clauses - 1)
   1.109 +			(* string list -> unit *)
   1.110 +			fun process_tokens [] =
   1.111 +				()
   1.112 +			  | process_tokens (tok::toks) =
   1.113  				if tok="R" then (
   1.114  					case toks of
   1.115  					  id::sep::lits =>
   1.116  						let
   1.117 -							val _        = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"."
   1.118 +							val _        = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"."
   1.119  							val cid      = int_from_string id
   1.120  							val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
   1.121  							val ls       = sort int_ord (map int_from_string lits)
   1.122 -							val proof_id = (* both 'ls' and the list of literals used as key in 'clauses' are sorted, *)
   1.123 -							               (* so testing for equality should suffice -- barring duplicate literals    *)
   1.124 -							               case AList.lookup (op =) clauses ls of
   1.125 +							val proof_id = case original_clause_id ls of
   1.126  							                 SOME orig_id => orig_id
   1.127 -						                   | NONE         => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.")
   1.128 +							               | NONE         => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.")
   1.129 +						in
   1.130  							(* extend the mapping of clause IDs with this newly defined ID *)
   1.131 -							val _        = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
   1.132 -							                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").")
   1.133 -						in
   1.134 +							clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
   1.135 +								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").")
   1.136  							(* the proof itself doesn't change *)
   1.137 -							(clause_table, empty_id)
   1.138  						end
   1.139  					| _ =>
   1.140  						raise INVALID_PROOF "File format error: \"R\" followed by an insufficient number of tokens."
   1.141 @@ -645,7 +679,7 @@
   1.142  					case toks of
   1.143  					  id::sep::ids =>
   1.144  						let
   1.145 -							val _        = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"."
   1.146 +							val _        = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"."
   1.147  							val cid      = int_from_string id
   1.148  							val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
   1.149  							(* ignore the pivot literals in MiniSat's trace *)
   1.150 @@ -659,7 +693,7 @@
   1.151  							                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").")
   1.152  						in
   1.153  							(* update clause table *)
   1.154 -							(Inttab.update_new (proof_id, rs) clause_table, empty_id)
   1.155 +							clause_table := Inttab.update_new (proof_id, rs) (!clause_table)
   1.156  								handle Inttab.DUP _ => raise INVALID_PROOF ("Error: internal ID for clause " ^ id ^ " already used.")
   1.157  						end
   1.158  					| _ =>
   1.159 @@ -668,11 +702,11 @@
   1.160  					case toks of
   1.161  					  [id] =>
   1.162  						let
   1.163 -							val _ = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"."
   1.164 +							val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"."
   1.165  							val _ = sat_to_proof (int_from_string id)
   1.166  						in
   1.167  							(* simply ignore "D" *)
   1.168 -							(clause_table, empty_id)
   1.169 +							()
   1.170  						end
   1.171  					| _ =>
   1.172  						raise INVALID_PROOF "File format error: \"D\" followed by an illegal number of tokens."
   1.173 @@ -680,27 +714,29 @@
   1.174  					case toks of
   1.175  					  [id1, id2] =>
   1.176  						let
   1.177 -							val _            = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement."
   1.178 +							val _            = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement."
   1.179  							val _            = sat_to_proof (int_from_string id1)
   1.180  							val new_empty_id = sat_to_proof (int_from_string id2)
   1.181  						in
   1.182  							(* update conflict id *)
   1.183 -							(clause_table, new_empty_id)
   1.184 +							empty_id := new_empty_id
   1.185  						end
   1.186  					| _ =>
   1.187  						raise INVALID_PROOF "File format error: \"X\" followed by an illegal number of tokens."
   1.188  				) else
   1.189  					raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
   1.190 -			(* string list -> proof -> proof *)
   1.191 -			fun process_lines [] proof =
   1.192 -				proof
   1.193 -			  | process_lines (l::ls) proof =
   1.194 -				process_lines ls (process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l) proof)
   1.195 +			(* string list -> unit *)
   1.196 +			fun process_lines [] =
   1.197 +				()
   1.198 +			  | process_lines (l::ls) = (
   1.199 +					process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l);
   1.200 +					process_lines ls
   1.201 +				)
   1.202  			(* proof *)
   1.203 -			val (clause_table, empty_id) = process_lines proof_lines (Inttab.empty, ~1)
   1.204 -			val _                        = if empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
   1.205 +			val _ = process_lines proof_lines
   1.206 +			val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
   1.207  		in
   1.208 -			SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id))
   1.209 +			SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id))
   1.210  		end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
   1.211  	| result =>
   1.212  		result
   1.213 @@ -856,7 +892,8 @@
   1.214  					process_lines ls
   1.215  				)
   1.216  			(* proof *)
   1.217 -			val _ = process_lines proof_lines
   1.218 +			val _ = tracing "process_lines"  (*TODO*)
   1.219 +			val _ = timeap process_lines proof_lines  (*TODO*)
   1.220  			val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
   1.221  		in
   1.222  			SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id))