# HG changeset patch # User wenzelm # Date 1392208278 -3600 # Node ID 9781e17dcc23d57b308d5f622c6bae0ec4f017be # Parent 662e0fd398236ae2e8e863f49351b97736424df0 removed odd comments -- inferred types are shown by Prover IDE; diff -r 662e0fd39823 -r 9781e17dcc23 src/HOL/Tools/prop_logic.ML --- a/src/HOL/Tools/prop_logic.ML Wed Feb 12 11:28:17 2014 +0100 +++ b/src/HOL/Tools/prop_logic.ML Wed Feb 12 13:31:18 2014 +0100 @@ -258,12 +258,9 @@ let val fm' = nnf fm (* 'new' specifies the next index that is available to introduce an auxiliary variable *) - (* int ref *) val new = Unsynchronized.ref (maxidx fm' + 1) - (* unit -> int *) fun new_idx () = let val idx = !new in new := idx+1; idx end (* replaces 'And' by an auxiliary variable (and its definition) *) - (* prop_formula -> prop_formula * prop_formula list *) fun defcnf_or (And x) = let val i = new_idx () @@ -279,7 +276,6 @@ (Or (fm1', fm2'), defs1 @ defs2) end | defcnf_or fm = (fm, []) - (* prop_formula -> prop_formula *) fun defcnf_from_nnf True = True | defcnf_from_nnf False = False | defcnf_from_nnf (BoolVar i) = BoolVar i diff -r 662e0fd39823 -r 9781e17dcc23 src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Wed Feb 12 11:28:17 2014 +0100 +++ b/src/HOL/Tools/sat_solver.ML Wed Feb 12 13:31:18 2014 +0100 @@ -108,11 +108,8 @@ (* Note: 'fm' must be given in CNF. *) (* ------------------------------------------------------------------------- *) - (* Path.T -> prop_formula -> unit *) - fun write_dimacs_cnf_file path fm = let - (* prop_formula -> prop_formula *) fun cnf_True_False_elim True = Or (BoolVar 1, Not (BoolVar 1)) | cnf_True_False_elim False = @@ -120,15 +117,12 @@ | cnf_True_False_elim fm = fm (* since 'fm' is in CNF, either 'fm'='True'/'False', or 'fm' does not contain 'True'/'False' at all *) - (* prop_formula -> int *) fun cnf_number_of_clauses (And (fm1, fm2)) = (cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2) | cnf_number_of_clauses _ = 1 - (* TextIO.outstream -> unit *) fun write_cnf_file out = let - (* prop_formula -> unit *) fun write_formula True = error "formula is not in CNF" | write_formula False = @@ -170,14 +164,10 @@ (* Note: 'fm' must not contain a variable index less than 1. *) (* ------------------------------------------------------------------------- *) - (* Path.T -> prop_formula -> unit *) - fun write_dimacs_sat_file path fm = let - (* TextIO.outstream -> unit *) fun write_sat_file out = let - (* prop_formula -> unit *) fun write_formula True = TextIO.output (out, "*()") | write_formula False = @@ -243,21 +233,16 @@ (* value of i is taken to be unspecified. *) (* ------------------------------------------------------------------------- *) - (* Path.T -> string * string * string -> result *) - fun read_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) = let - (* string -> int list *) fun int_list_from_string s = map_filter Int.fromString (space_explode " " s) - (* int list -> assignment *) fun assignment_from_list [] i = NONE (* the SAT solver didn't provide a value for this variable *) | assignment_from_list (x::xs) i = if x=i then (SOME true) else if x=(~i) then (SOME false) else assignment_from_list xs i - (* int list -> string list -> assignment *) fun parse_assignment xs [] = assignment_from_list xs | parse_assignment xs (line::lines) = @@ -265,7 +250,6 @@ parse_assignment (xs @ int_list_from_string line) lines else assignment_from_list xs - (* string -> string -> bool *) fun is_substring needle haystack = let val length1 = String.size needle @@ -277,7 +261,6 @@ true else is_substring needle (String.substring (haystack, 1, length2-1)) end - (* string list -> result *) fun parse_lines [] = UNKNOWN | parse_lines (line::lines) = @@ -305,7 +288,6 @@ fun read_dimacs_cnf_file path = let - (* string list -> string list *) fun filter_preamble [] = error "problem line not found in DIMACS CNF file" | filter_preamble (line::lines) = @@ -319,12 +301,10 @@ lines else error "preamble in DIMACS CNF file contains a line that does not begin with \"c \" or \"p \"" - (* string -> int *) fun int_from_string s = case Int.fromString s of SOME i => i | NONE => error ("token " ^ quote s ^ " in DIMACS CNF file is not a number") - (* int list -> int list list *) fun clauses xs = let val (xs1, xs2) = take_prefix (fn i => i <> 0) xs @@ -377,8 +357,6 @@ (* add_solver: updates 'solvers' by adding a new solver *) (* ------------------------------------------------------------------------- *) - (* string * solver -> unit *) - fun add_solver (name, new_solver) = CRITICAL (fn () => let val the_solvers = !solvers; @@ -393,8 +371,6 @@ (* raised. *) (* ------------------------------------------------------------------------- *) - (* string -> solver *) - fun invoke_solver name = (the o AList.lookup (op =) (!solvers)) name; @@ -413,9 +389,7 @@ let fun enum_solver fm = let - (* int list *) val indices = Prop_Logic.indices fm - (* int list -> int list -> int list option *) (* binary increment: list 'xs' of current bits, list 'ys' of all bits (lower bits first) *) fun next_list _ ([]:int list) = NONE @@ -428,10 +402,8 @@ else (* set the lowest bit that wasn't set before, keep the higher bits *) SOME (y::x::xs) - (* int list -> int -> bool *) fun assignment_from_list xs i = member (op =) xs i - (* int list -> SatSolver.result *) fun solver_loop xs = if Prop_Logic.eval (assignment_from_list xs) fm then SatSolver.SATISFIABLE (SOME o (assignment_from_list xs)) @@ -463,19 +435,15 @@ (* but that sometimes leads to worse performance due to the *) (* introduction of additional variables. *) val fm' = Prop_Logic.nnf fm - (* int list *) val indices = Prop_Logic.indices fm' - (* int list -> int -> prop_formula *) fun partial_var_eval [] i = BoolVar i | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i - (* int list -> prop_formula -> prop_formula *) fun partial_eval xs True = True | partial_eval xs False = False | partial_eval xs (BoolVar i) = partial_var_eval xs i | partial_eval xs (Not fm) = SNot (partial_eval xs fm) | partial_eval xs (Or (fm1, fm2)) = SOr (partial_eval xs fm1, partial_eval xs fm2) | partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2) - (* prop_formula -> int list *) fun forced_vars True = [] | forced_vars False = [] | forced_vars (BoolVar i) = [i] @@ -485,7 +453,6 @@ (* Above, i *and* ~i may be forced. In this case the first occurrence takes *) (* precedence, and the next partial evaluation of the formula returns 'False'. *) | forced_vars _ = error "formula is not in negation normal form" - (* int list -> prop_formula -> (int list * prop_formula) *) fun eval_and_force xs fm = let val fm' = partial_eval xs fm @@ -497,10 +464,8 @@ eval_and_force (xs@xs') fm' (* xs and xs' should be distinct, so '@' here should have *) (* the same effect as 'union_int' *) end - (* int list -> int option *) fun fresh_var xs = find_first (fn i => not (member (op =) xs i) andalso not (member (op =) xs (~i))) indices - (* int list -> prop_formula -> int list option *) (* partial assignment 'xs' *) fun dpll xs fm = let @@ -518,7 +483,6 @@ | NONE => dpll ((~x)::xs') fm' (* now try interpreting 'x' as 'False' *) end end - (* int list -> assignment *) fun assignment_from_list [] i = NONE (* the DPLL procedure didn't provide a value for this variable *) | assignment_from_list (x::xs) i = @@ -603,11 +567,9 @@ in case result of SatSolver.UNSATISFIABLE NONE => (let - (* string list *) val proof_lines = (split_lines o File.read) proofpath handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\"" (* representation of clauses as ordered lists of literals (with duplicates removed) *) - (* prop_formula -> int list *) fun clause_to_lit_list (Prop_Logic.Or (fm1, fm2)) = Ord_List.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2) | clause_to_lit_list (Prop_Logic.BoolVar i) = @@ -616,7 +578,6 @@ [~i] | clause_to_lit_list _ = raise INVALID_PROOF "Error: invalid clause in CNF formula." - (* prop_formula -> int *) fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 | cnf_number_of_clauses _ = @@ -625,7 +586,6 @@ (* int list array *) val clauses = Array.array (number_of_clauses, []) (* initialize the 'clauses' array *) - (* prop_formula * int -> int *) fun init_array (Prop_Logic.And (fm1, fm2), n) = init_array (fm2, init_array (fm1, n)) | init_array (fm, n) = @@ -636,7 +596,6 @@ val last_ref_clause = Unsynchronized.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 = @@ -658,12 +617,10 @@ in original_clause_id_from (!last_ref_clause + 1) end - (* string -> int *) - fun int_from_string s = ( - case Int.fromString s of + fun int_from_string s = + (case Int.fromString s of SOME i => i - | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") - ) + | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")) (* parse the proof file *) val clause_table = Unsynchronized.ref (Inttab.empty : int list Inttab.table) val empty_id = Unsynchronized.ref ~1 @@ -676,7 +633,6 @@ | NONE => raise INVALID_PROOF ("Clause ID " ^ string_of_int id ^ " used, but not defined.") ) val next_id = Unsynchronized.ref (number_of_clauses - 1) - (* string list -> unit *) fun process_tokens [] = () | process_tokens (tok::toks) = @@ -749,7 +705,6 @@ 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 -> unit *) fun process_lines [] = () | process_lines (l::ls) = ( @@ -812,14 +767,12 @@ case SatSolver.invoke_solver "zchaff" fm of SatSolver.UNSATISFIABLE NONE => (let - (* string list *) (* FIXME File.tmp_path (!?) *) val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace")) handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\"" fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 | cnf_number_of_clauses _ = 1 - (* string -> int *) fun int_from_string s = ( case Int.fromString s of SOME i => i @@ -829,7 +782,6 @@ val clause_offset = Unsynchronized.ref ~1 val clause_table = Unsynchronized.ref (Inttab.empty : int list Inttab.table) val empty_id = Unsynchronized.ref ~1 - (* string list -> unit *) fun process_tokens [] = () | process_tokens (tok::toks) = @@ -910,7 +862,6 @@ 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 -> unit *) fun process_lines [] = () | process_lines (l::ls) = ( @@ -1004,16 +955,3 @@ SatSolver.add_solver ("jerusat", jerusat) end; -(* ------------------------------------------------------------------------- *) -(* Add code for other SAT solvers below. *) -(* ------------------------------------------------------------------------- *) - -(* -let - fun mysolver fm = ... -in - SatSolver.add_solver ("myname", (fn fm => if mysolver_is_configured then mysolver fm else raise SatSolver.NOT_CONFIGURED)); -- register the solver -end; - --- the solver is now available as SatSolver.invoke_solver "myname" -*)