--- 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
--- 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
--- 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 =
--- 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)
--- 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;
--- 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;
--- 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 []