--- 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;