diff -r 288a504c24d6 -r 5294ecae6708 src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Thu Nov 09 16:14:43 2006 +0100 +++ b/src/HOL/Tools/sat_solver.ML Thu Nov 09 18:48:45 2006 +0100 @@ -1,7 +1,7 @@ (* Title: HOL/Tools/sat_solver.ML ID: $Id$ Author: Tjark Weber - Copyright 2004-2005 + Copyright 2004-2006 Interface to external SAT solvers, and (simple) built-in SAT solvers. *) @@ -580,25 +580,60 @@ SatSolver.UNSATISFIABLE NONE => (let (* string list *) - val proof_lines = ((split_lines o File.read) proofpath) + val proof_lines = (split_lines o File.read) proofpath handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\"" - (* a simple representation of the CNF formula as list of clauses (paired with their ID), *) - (* where each clause is a sorted list of literals, where each literal is an int *) - (* removes duplicates from an ordered list *) - (* int list -> int list *) - fun remove_dups [] = [] - | remove_dups [x] = [x] - | remove_dups (x :: y :: xs) = if x = y then remove_dups (y :: xs) else x :: remove_dups (y :: xs) + (* representation of clauses as ordered lists of literals (with duplicates removed) *) (* prop_formula -> int list *) - fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) = clause_to_lit_list fm1 @ clause_to_lit_list fm2 - | clause_to_lit_list (PropLogic.BoolVar i) = [i] - | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) = [~i] - | clause_to_lit_list _ = raise INVALID_PROOF "Error: invalid clause in CNF formula." - (* prop_formula -> int list list *) - fun cnf_to_clause_list (PropLogic.And (fm1, fm2)) = cnf_to_clause_list fm1 @ cnf_to_clause_list fm2 - | cnf_to_clause_list fm = [(remove_dups o sort int_ord o clause_to_lit_list) fm] - (* (int list * int) list * int *) - val (clauses, length_clauses) = fold_map (fn clause => fn n => ((clause, n), n+1)) (cnf_to_clause_list cnf) 0 + fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) = + OrdList.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2) + | clause_to_lit_list (PropLogic.BoolVar i) = + [i] + | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) = + [~i] + | clause_to_lit_list _ = + raise INVALID_PROOF "Error: invalid clause in CNF formula." + (* prop_formula -> int *) + fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = + cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 + | cnf_number_of_clauses _ = + 1 + val number_of_clauses = cnf_number_of_clauses cnf + (* int list array *) + val clauses = Array.array (number_of_clauses, []) + (* initialize the 'clauses' array *) + (* prop_formula * int -> int *) + fun init_array (PropLogic.And (fm1, fm2), n) = + init_array (fm2, init_array (fm1, n)) + | init_array (fm, n) = + (Array.update (clauses, n, clause_to_lit_list fm); n+1) + val _ = init_array (cnf, 0) + (* optimization for the common case where MiniSat "R"s clauses in their *) + (* original order: *) + val last_ref_clause = ref (number_of_clauses - 1) + (* search the 'clauses' array for the given list of literals 'lits', *) + (* starting at index '!last_ref_clause + 1' *) + (* int list -> int option *) + fun original_clause_id lits = + let + fun original_clause_id_from index = + if index = number_of_clauses then + (* search from beginning again *) + original_clause_id_from 0 + (* both 'lits' and the list of literals used in 'clauses' are sorted, so *) + (* testing for equality should suffice -- barring duplicate literals *) + else if Array.sub (clauses, index) = lits then ( + (* success *) + last_ref_clause := index; + SOME index + ) else if index = !last_ref_clause then + (* failure *) + NONE + else + (* continue search *) + original_clause_id_from (index + 1) + in + original_clause_id_from (!last_ref_clause + 1) + end (* string -> int *) fun int_from_string s = ( case Int.fromString s of @@ -606,6 +641,8 @@ | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") ) (* parse the proof file *) + val clause_table = ref (Inttab.empty : int list Inttab.table) + val empty_id = ref ~1 (* contains a mapping from clause IDs as used by MiniSat to clause IDs in *) (* our proof format, where original clauses are numbered starting from 0 *) val clause_id_map = ref (Inttab.empty : int Inttab.table) @@ -614,30 +651,27 @@ SOME id' => id' | NONE => raise INVALID_PROOF ("Clause ID " ^ Int.toString id ^ " used, but not defined.") ) - val next_id = ref (length_clauses - 1) - (* string list -> proof -> proof *) - fun process_tokens [] proof = - proof - | process_tokens (tok::toks) (clause_table, empty_id) = + val next_id = ref (number_of_clauses - 1) + (* string list -> unit *) + fun process_tokens [] = + () + | process_tokens (tok::toks) = if tok="R" then ( case toks of id::sep::lits => let - val _ = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"." + val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"." val cid = int_from_string id val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") val ls = sort int_ord (map int_from_string lits) - val proof_id = (* both 'ls' and the list of literals used as key in 'clauses' are sorted, *) - (* so testing for equality should suffice -- barring duplicate literals *) - case AList.lookup (op =) clauses ls of + val proof_id = case original_clause_id ls of SOME orig_id => orig_id - | NONE => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.") + | NONE => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.") + in (* extend the mapping of clause IDs with this newly defined ID *) - val _ = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map) - handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").") - in + clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map) + handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").") (* the proof itself doesn't change *) - (clause_table, empty_id) end | _ => raise INVALID_PROOF "File format error: \"R\" followed by an insufficient number of tokens." @@ -645,7 +679,7 @@ case toks of id::sep::ids => let - val _ = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"." + val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"." val cid = int_from_string id val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") (* ignore the pivot literals in MiniSat's trace *) @@ -659,7 +693,7 @@ handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").") in (* update clause table *) - (Inttab.update_new (proof_id, rs) clause_table, empty_id) + clause_table := Inttab.update_new (proof_id, rs) (!clause_table) handle Inttab.DUP _ => raise INVALID_PROOF ("Error: internal ID for clause " ^ id ^ " already used.") end | _ => @@ -668,11 +702,11 @@ case toks of [id] => let - val _ = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"." + val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"." val _ = sat_to_proof (int_from_string id) in (* simply ignore "D" *) - (clause_table, empty_id) + () end | _ => raise INVALID_PROOF "File format error: \"D\" followed by an illegal number of tokens." @@ -680,27 +714,29 @@ case toks of [id1, id2] => let - val _ = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement." + val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement." val _ = sat_to_proof (int_from_string id1) val new_empty_id = sat_to_proof (int_from_string id2) in (* update conflict id *) - (clause_table, new_empty_id) + empty_id := new_empty_id end | _ => raise INVALID_PROOF "File format error: \"X\" followed by an illegal 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 @@ -856,7 +892,8 @@ process_lines ls ) (* proof *) - val _ = process_lines proof_lines + val _ = tracing "process_lines" (*TODO*) + val _ = timeap process_lines proof_lines (*TODO*) 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))