# HG changeset patch # User blanchet # Date 1399223309 -7200 # Node ID a265e41cc33bdf826ee0dd04e8a17ed9c0e03aec # Parent b38c5b9cf59007119f49e451ebccea39f4dfbde2 tuned structure name diff -r b38c5b9cf590 -r a265e41cc33b src/HOL/Library/refute.ML --- a/src/HOL/Library/refute.ML Sun May 04 19:01:36 2014 +0200 +++ b/src/HOL/Library/refute.ML Sun May 04 19:08:29 2014 +0200 @@ -1074,32 +1074,32 @@ \external solver.") else ()); val solver = - SatSolver.invoke_solver satsolver + SAT_Solver.invoke_solver satsolver handle Option.Option => error ("Unknown SAT solver: " ^ quote satsolver ^ ". Available solvers: " ^ - commas (map (quote o fst) (SatSolver.get_solvers ())) ^ ".") + commas (map (quote o fst) (SAT_Solver.get_solvers ())) ^ ".") in Output.urgent_message "Invoking SAT solver..."; (case solver fm of - SatSolver.SATISFIABLE assignment => + SAT_Solver.SATISFIABLE assignment => (Output.urgent_message ("Model found:\n" ^ print_model ctxt model (fn i => case assignment i of SOME b => b | NONE => true)); if maybe_spurious then "potential" else "genuine") - | SatSolver.UNSATISFIABLE _ => + | SAT_Solver.UNSATISFIABLE _ => (Output.urgent_message "No model exists."; case next_universe universe sizes minsize maxsize of SOME universe' => find_model_loop universe' | NONE => (Output.urgent_message "Search terminated, no larger universe within the given limits."; "none")) - | SatSolver.UNKNOWN => + | SAT_Solver.UNKNOWN => (Output.urgent_message "No model found."; case next_universe universe sizes minsize maxsize of SOME universe' => find_model_loop universe' | NONE => (Output.urgent_message "Search terminated, no larger universe within the given limits."; - "unknown"))) handle SatSolver.NOT_CONFIGURED => + "unknown"))) handle SAT_Solver.NOT_CONFIGURED => (error ("SAT solver " ^ quote satsolver ^ " is not configured."); "unknown") end diff -r b38c5b9cf590 -r a265e41cc33b src/HOL/Tools/Function/scnp_solve.ML --- a/src/HOL/Tools/Function/scnp_solve.ML Sun May 04 19:01:36 2014 +0200 +++ b/src/HOL/Tools/Function/scnp_solve.ML Sun May 04 19:08:29 2014 +0200 @@ -73,7 +73,7 @@ (* SAT solving *) val solver = Unsynchronized.ref "auto"; fun sat_solver x = - Function_Common.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x + Function_Common.PROFILE "sat_solving..." (SAT_Solver.invoke_solver (!solver)) x (* "Virtual constructors" for various propositional variables *) fun var_constrs (gp as GP (arities, _)) = @@ -250,7 +250,7 @@ in get_first (fn l => case sat_solver (encode bits gp l) of - SatSolver.SATISFIABLE f => SOME (mk_certificate bits l gp f) + SAT_Solver.SATISFIABLE f => SOME (mk_certificate bits l gp f) | _ => NONE) labels end diff -r b38c5b9cf590 -r a265e41cc33b src/HOL/Tools/Nitpick/kodkod_sat.ML --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Sun May 04 19:01:36 2014 +0200 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Sun May 04 19:08:29 2014 +0200 @@ -28,7 +28,7 @@ External of string * string * string list | ExternalV2 of sink * string * string * string list * string * string * string -(* for compatibility with "SatSolver" *) +(* for compatibility with "SAT_Solver" *) val berkmin_exec = getenv "BERKMIN_EXE" val static_list = diff -r b38c5b9cf590 -r a265e41cc33b src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Sun May 04 19:01:36 2014 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Sun May 04 19:08:29 2014 +0200 @@ -573,7 +573,7 @@ let (* use the first ML solver (to avoid startup overhead) *) val (ml_solvers, nonml_solvers) = - SatSolver.get_solvers () + SAT_Solver.get_solvers () |> List.partition (member (op =) ["dptsat", "cdclite"] o fst) val res = if null nonml_solvers then @@ -582,10 +582,10 @@ TimeLimit.timeLimit ml_solver_timeout (snd (hd ml_solvers)) prop handle TimeLimit.TimeOut => TimeLimit.timeLimit tac_timeout - (SatSolver.invoke_solver "auto") prop + (SAT_Solver.invoke_solver "auto") prop in case res of - SatSolver.SATISFIABLE assigns => do_assigns assigns + SAT_Solver.SATISFIABLE assigns => do_assigns assigns | _ => (trace_msg (K "*** Unsolvable"); NONE) end handle TimeLimit.TimeOut => (trace_msg (K "*** Timed out"); NONE) diff -r b38c5b9cf590 -r a265e41cc33b src/HOL/Tools/sat.ML --- a/src/HOL/Tools/sat.ML Sun May 04 19:01:36 2014 +0200 +++ b/src/HOL/Tools/sat.ML Sun May 04 19:08:29 2014 +0200 @@ -202,7 +202,7 @@ (* ------------------------------------------------------------------------- *) (* replay_proof: replays the resolution proof returned by the SAT solver; *) -(* cf. SatSolver.proof for details of the proof format. Updates the *) +(* cf. SAT_Solver.proof for details of the proof format. Updates the *) (* 'clauses' array with derived clauses, and returns the derived clause *) (* at index 'empty_id' (which should just be "False" if proof *) (* reconstruction was successful, with the used clauses as hyps). *) @@ -335,9 +335,9 @@ let val the_solver = Config.get ctxt solver val _ = cond_tracing ctxt (fn () => "Invoking solver " ^ the_solver) - in SatSolver.invoke_solver the_solver fm end + in SAT_Solver.invoke_solver the_solver fm end of - SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => + SAT_Solver.UNSATISFIABLE (SOME (clause_table, empty_id)) => (cond_tracing ctxt (fn () => "Proof trace from SAT solver:\n" ^ "clauses: " ^ ML_Syntax.print_list @@ -370,13 +370,13 @@ (* [c_1, ..., c_n] |- False *) Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm end) - | SatSolver.UNSATISFIABLE NONE => + | SAT_Solver.UNSATISFIABLE NONE => if Config.get ctxt quick_and_dirty then (warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof"; make_quick_and_dirty_thm ()) else raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, []) - | SatSolver.SATISFIABLE assignment => + | SAT_Solver.SATISFIABLE assignment => let val msg = "SAT solver found a countermodel:\n" ^ @@ -388,7 +388,7 @@ in raise THM (msg, 0, []) end - | SatSolver.UNKNOWN => + | SAT_Solver.UNKNOWN => raise THM ("SAT solver failed to decide the formula", 0, []) end; diff -r b38c5b9cf590 -r a265e41cc33b src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Sun May 04 19:01:36 2014 +0200 +++ b/src/HOL/Tools/sat_solver.ML Sun May 04 19:08:29 2014 +0200 @@ -47,7 +47,7 @@ val invoke_solver : string -> solver (* exception Option *) end; -structure SatSolver : SAT_SOLVER = +structure SAT_Solver : SAT_SOLVER = struct open Prop_Logic; @@ -147,7 +147,7 @@ val number_of_vars = maxidx fm' val number_of_clauses = cnf_number_of_clauses fm' in - TextIO.output (out, "c This file was generated by SatSolver.write_dimacs_cnf_file\n"); + TextIO.output (out, "c This file was generated by SAT_Solver.write_dimacs_cnf_file\n"); TextIO.output (out, "p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n"); write_formula fm'; @@ -209,7 +209,7 @@ write_formula fm val number_of_vars = Int.max (maxidx fm, 1) in - TextIO.output (out, "c This file was generated by SatSolver.write_dimacs_sat_file\n"); + TextIO.output (out, "c This file was generated by SAT_Solver.write_dimacs_sat_file\n"); TextIO.output (out, "p sat " ^ string_of_int number_of_vars ^ "\n"); TextIO.output (out, "("); write_formula fm; @@ -313,7 +313,7 @@ [] => [xs1] | (0::[]) => [xs1] | (0::tl) => xs1 :: clauses tl - | _ => raise Fail "SatSolver.clauses" + | _ => raise Fail "SAT_Solver.clauses" end fun literal_from_int i = (i<>0 orelse error "variable index in DIMACS CNF file is 0"; @@ -376,7 +376,7 @@ fun invoke_solver name = the (AList.lookup (op =) (get_solvers ()) name); -end; (* SatSolver *) +end; (* SAT_Solver *) (* ------------------------------------------------------------------------- *) @@ -384,7 +384,7 @@ (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) -(* Internal SAT solver, available as 'SatSolver.invoke_solver "cdclite"' -- *) +(* Internal SAT solver, available as 'SAT_Solver.invoke_solver "cdclite"' -- *) (* a simplified implementation of the conflict-driven clause-learning *) (* algorithm (cf. L. Zhang, S. Malik: "The Quest for Efficient Boolean *) (* Satisfiability Solvers", July 2002, Fig. 2). This solver produces models *) @@ -520,7 +520,7 @@ (case propagate units state of (NONE, state' as (_, _, vars, _, _)) => (case decide state' of - NONE => SatSolver.SATISFIABLE (assignment_of vars) + NONE => SAT_Solver.SATISFIABLE (assignment_of vars) | SOME (lit, state'') => search [lit] state'') | (SOME conflicting_cls, state' as (level, trail, vars, clss, proofs)) => let @@ -557,7 +557,7 @@ in uncurry search (fold add_clause clss ([], state)) end handle UNSAT (conflicting_cls, (_, _, vars, _, proofs)) => let val (idx, (_, ptab)) = mk_proof vars conflicting_cls proofs - in SatSolver.UNSATISFIABLE (SOME (ptab, idx)) end + in SAT_Solver.UNSATISFIABLE (SOME (ptab, idx)) end fun variable_of (Prop_Logic.BoolVar 0) = error "bad propositional variable" | variable_of (Prop_Logic.BoolVar i) = i @@ -575,11 +575,11 @@ let val fm' = if Prop_Logic.is_cnf fm then fm else Prop_Logic.defcnf fm in solve (clauses_of fm') end in - SatSolver.add_solver ("cdclite", dpll_solver) + SAT_Solver.add_solver ("cdclite", dpll_solver) end; (* ------------------------------------------------------------------------- *) -(* Internal SAT solver, available as 'SatSolver.invoke_solver "auto"': uses *) +(* Internal SAT solver, available as 'SAT_Solver.invoke_solver "auto"': uses *) (* the last installed solver (other than "auto" itself) that does not raise *) (* 'NOT_CONFIGURED'. (However, the solver may return 'UNKNOWN'.) *) (* ------------------------------------------------------------------------- *) @@ -588,7 +588,7 @@ fun auto_solver fm = let fun loop [] = - SatSolver.UNKNOWN + SAT_Solver.UNKNOWN | loop ((name, solver)::solvers) = if name="auto" then (* do not call solver "auto" from within "auto" *) @@ -596,13 +596,13 @@ else ( (* apply 'solver' to 'fm' *) solver fm - handle SatSolver.NOT_CONFIGURED => loop solvers + handle SAT_Solver.NOT_CONFIGURED => loop solvers ) in - loop (SatSolver.get_solvers ()) + loop (SAT_Solver.get_solvers ()) end in - SatSolver.add_solver ("auto", auto_solver) + SAT_Solver.add_solver ("auto", auto_solver) end; (* ------------------------------------------------------------------------- *) @@ -628,22 +628,22 @@ exception INVALID_PROOF of string fun minisat_with_proofs fm = let - val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () + val _ = if (getenv "MINISAT_HOME") = "" then raise SAT_Solver.NOT_CONFIGURED else () val serial_str = serial_string () val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) val proofpath = File.tmp_path (Path.explode ("result" ^ serial_str ^ ".prf")) val cmd = getenv "MINISAT_HOME" ^ "/minisat " ^ File.shell_path inpath ^ " -r " ^ File.shell_path outpath ^ " -t " ^ File.shell_path proofpath ^ "> /dev/null" - fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm - fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT") + fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath fm + fun readfn () = SAT_Solver.read_std_result_file outpath ("SAT", "", "UNSAT") val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else () val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else () val cnf = Prop_Logic.defcnf fm - val result = SatSolver.make_external_solver cmd writefn readfn cnf + val result = SAT_Solver.make_external_solver cmd writefn readfn cnf val _ = try File.rm inpath val _ = try File.rm outpath in case result of - SatSolver.UNSATISFIABLE NONE => + SAT_Solver.UNSATISFIABLE NONE => (let val proof_lines = (split_lines o File.read) proofpath handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\"" @@ -793,35 +793,35 @@ 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)) - end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE)) + SAT_Solver.UNSATISFIABLE (SOME (!clause_table, !empty_id)) + end handle INVALID_PROOF reason => (warning reason; SAT_Solver.UNSATISFIABLE NONE)) | result => result end in - SatSolver.add_solver ("minisat_with_proofs", minisat_with_proofs) + SAT_Solver.add_solver ("minisat_with_proofs", minisat_with_proofs) end; let fun minisat fm = let - val _ = if getenv "MINISAT_HOME" = "" then raise SatSolver.NOT_CONFIGURED else () + val _ = if getenv "MINISAT_HOME" = "" then raise SAT_Solver.NOT_CONFIGURED else () val serial_str = serial_string () val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) val cmd = getenv "MINISAT_HOME" ^ "/minisat " ^ File.shell_path inpath ^ " -r " ^ File.shell_path outpath ^ " > /dev/null" - fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) - fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT") + fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) + fun readfn () = SAT_Solver.read_std_result_file outpath ("SAT", "", "UNSAT") val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else () val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else () - val result = SatSolver.make_external_solver cmd writefn readfn fm + val result = SAT_Solver.make_external_solver cmd writefn readfn fm val _ = try File.rm inpath val _ = try File.rm outpath in result end in - SatSolver.add_solver ("minisat", minisat) + SAT_Solver.add_solver ("minisat", minisat) end; (* ------------------------------------------------------------------------- *) @@ -842,8 +842,8 @@ let exception INVALID_PROOF of string fun zchaff_with_proofs fm = - case SatSolver.invoke_solver "zchaff" fm of - SatSolver.UNSATISFIABLE NONE => + case SAT_Solver.invoke_solver "zchaff" fm of + SAT_Solver.UNSATISFIABLE NONE => (let (* FIXME File.tmp_path (!?) *) val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace")) @@ -950,34 +950,34 @@ 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)) - end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE)) + SAT_Solver.UNSATISFIABLE (SOME (!clause_table, !empty_id)) + end handle INVALID_PROOF reason => (warning reason; SAT_Solver.UNSATISFIABLE NONE)) | result => result in - SatSolver.add_solver ("zchaff_with_proofs", zchaff_with_proofs) + SAT_Solver.add_solver ("zchaff_with_proofs", zchaff_with_proofs) end; let fun zchaff fm = let - val _ = if getenv "ZCHAFF_HOME" = "" then raise SatSolver.NOT_CONFIGURED else () + val _ = if getenv "ZCHAFF_HOME" = "" then raise SAT_Solver.NOT_CONFIGURED else () val serial_str = serial_string () val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) val cmd = getenv "ZCHAFF_HOME" ^ "/zchaff " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath - fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) - fun readfn () = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable") + fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) + fun readfn () = SAT_Solver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable") val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else () val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else () - val result = SatSolver.make_external_solver cmd writefn readfn fm + val result = SAT_Solver.make_external_solver cmd writefn readfn fm val _ = try File.rm inpath val _ = try File.rm outpath in result end in - SatSolver.add_solver ("zchaff", zchaff) + SAT_Solver.add_solver ("zchaff", zchaff) end; (* ------------------------------------------------------------------------- *) @@ -987,24 +987,24 @@ let fun berkmin fm = let - val _ = if (getenv "BERKMIN_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () + val _ = if (getenv "BERKMIN_HOME") = "" then raise SAT_Solver.NOT_CONFIGURED else () val serial_str = serial_string () val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) val exec = getenv "BERKMIN_EXE" val cmd = getenv "BERKMIN_HOME" ^ "/" ^ (if exec = "" then "BerkMin561" else exec) ^ " " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath - fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) - fun readfn () = SatSolver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!") + fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) + fun readfn () = SAT_Solver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!") val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else () val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else () - val result = SatSolver.make_external_solver cmd writefn readfn fm + val result = SAT_Solver.make_external_solver cmd writefn readfn fm val _ = try File.rm inpath val _ = try File.rm outpath in result end in - SatSolver.add_solver ("berkmin", berkmin) + SAT_Solver.add_solver ("berkmin", berkmin) end; (* ------------------------------------------------------------------------- *) @@ -1014,21 +1014,21 @@ let fun jerusat fm = let - val _ = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () + val _ = if (getenv "JERUSAT_HOME") = "" then raise SAT_Solver.NOT_CONFIGURED else () val serial_str = serial_string () val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) val cmd = getenv "JERUSAT_HOME" ^ "/Jerusat1.3 " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath - fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) - fun readfn () = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE") + fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) + fun readfn () = SAT_Solver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE") val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else () val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else () - val result = SatSolver.make_external_solver cmd writefn readfn fm + val result = SAT_Solver.make_external_solver cmd writefn readfn fm val _ = try File.rm inpath val _ = try File.rm outpath in result end in - SatSolver.add_solver ("jerusat", jerusat) + SAT_Solver.add_solver ("jerusat", jerusat) end; diff -r b38c5b9cf590 -r a265e41cc33b src/HOL/ex/SAT_Examples.thy --- a/src/HOL/ex/SAT_Examples.thy Sun May 04 19:01:36 2014 +0200 +++ b/src/HOL/ex/SAT_Examples.thy Sun May 04 19:08:29 2014 +0200 @@ -529,7 +529,7 @@ ML {* fun benchmark dimacsfile = let - val prop_fm = SatSolver.read_dimacs_cnf_file (Path.explode dimacsfile) + val prop_fm = SAT_Solver.read_dimacs_cnf_file (Path.explode dimacsfile) fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc) | and_to_list fm acc = rev (fm :: acc) val clauses = and_to_list prop_fm []