--- a/src/HOL/Tools/sat_solver.ML Tue May 19 13:52:12 2009 +0200
+++ b/src/HOL/Tools/sat_solver.ML Thu May 21 15:23:32 2009 +0100
@@ -1,7 +1,6 @@
(* Title: HOL/Tools/sat_solver.ML
- ID: $Id$
Author: Tjark Weber
- Copyright 2004-2006
+ Copyright 2004-2009
Interface to external SAT solvers, and (simple) built-in SAT solvers.
*)
@@ -21,7 +20,8 @@
val write_dimacs_cnf_file : Path.T -> PropLogic.prop_formula -> unit
val write_dimacs_sat_file : Path.T -> PropLogic.prop_formula -> unit
val read_std_result_file : Path.T -> string * string * string -> result
- val make_external_solver : string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver
+ val make_external_solver : string -> (PropLogic.prop_formula -> unit) ->
+ (unit -> result) -> solver
val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula
@@ -102,45 +102,49 @@
| cnf_True_False_elim False =
And (BoolVar 1, Not (BoolVar 1))
| cnf_True_False_elim fm =
- fm (* since 'fm' is in CNF, either 'fm'='True'/'False', or 'fm' does not contain 'True'/'False' at all *)
+ 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)) =
+ fun cnf_number_of_clauses (And (fm1, fm2)) =
(cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
| cnf_number_of_clauses _ =
1
- (* prop_formula -> string list *)
- fun cnf_string fm =
+ (* TextIO.outstream -> unit *)
+ fun write_cnf_file out =
let
- (* prop_formula -> string list -> string list *)
- fun cnf_string_acc True acc =
- error "formula is not in CNF"
- | cnf_string_acc False acc =
- error "formula is not in CNF"
- | cnf_string_acc (BoolVar i) acc =
- (i>=1 orelse error "formula contains a variable index less than 1";
- string_of_int i :: acc)
- | cnf_string_acc (Not (BoolVar i)) acc =
- "-" :: cnf_string_acc (BoolVar i) acc
- | cnf_string_acc (Not _) acc =
- error "formula is not in CNF"
- | cnf_string_acc (Or (fm1,fm2)) acc =
- cnf_string_acc fm1 (" " :: cnf_string_acc fm2 acc)
- | cnf_string_acc (And (fm1,fm2)) acc =
- cnf_string_acc fm1 (" 0\n" :: cnf_string_acc fm2 acc)
+ (* prop_formula -> unit *)
+ fun write_formula True =
+ error "formula is not in CNF"
+ | write_formula False =
+ error "formula is not in CNF"
+ | write_formula (BoolVar i) =
+ (i>=1 orelse error "formula contains a variable index less than 1";
+ TextIO.output (out, string_of_int i))
+ | write_formula (Not (BoolVar i)) =
+ (TextIO.output (out, "-");
+ write_formula (BoolVar i))
+ | write_formula (Not _) =
+ error "formula is not in CNF"
+ | write_formula (Or (fm1, fm2)) =
+ (write_formula fm1;
+ TextIO.output (out, " ");
+ write_formula fm2)
+ | write_formula (And (fm1, fm2)) =
+ (write_formula fm1;
+ TextIO.output (out, " 0\n");
+ write_formula fm2)
+ val fm' = cnf_True_False_elim fm
+ val number_of_vars = maxidx fm'
+ val number_of_clauses = cnf_number_of_clauses fm'
in
- cnf_string_acc fm []
+ TextIO.output (out, "c This file was generated by SatSolver.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';
+ TextIO.output (out, " 0\n")
end
- val fm' = cnf_True_False_elim fm
- val number_of_vars = maxidx fm'
- val number_of_clauses = cnf_number_of_clauses fm'
in
- File.write path
- ("c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^
- "p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n");
- File.append_list path
- (cnf_string fm');
- File.append path
- " 0\n"
+ File.open_output write_cnf_file path
end;
(* ------------------------------------------------------------------------- *)
@@ -154,49 +158,59 @@
fun write_dimacs_sat_file path fm =
let
- (* prop_formula -> string list *)
- fun sat_string fm =
+ (* TextIO.outstream -> unit *)
+ fun write_sat_file out =
let
- (* prop_formula -> string list -> string list *)
- fun sat_string_acc True acc =
- "*()" :: acc
- | sat_string_acc False acc =
- "+()" :: acc
- | sat_string_acc (BoolVar i) acc =
- (i>=1 orelse error "formula contains a variable index less than 1";
- string_of_int i :: acc)
- | sat_string_acc (Not (BoolVar i)) acc =
- "-" :: sat_string_acc (BoolVar i) acc
- | sat_string_acc (Not fm) acc =
- "-(" :: sat_string_acc fm (")" :: acc)
- | sat_string_acc (Or (fm1,fm2)) acc =
- "+(" :: sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 (")" :: acc))
- | sat_string_acc (And (fm1,fm2)) acc =
- "*(" :: sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 (")" :: acc))
+ (* prop_formula -> unit *)
+ fun write_formula True =
+ TextIO.output (out, "*()")
+ | write_formula False =
+ TextIO.output (out, "+()")
+ | write_formula (BoolVar i) =
+ (i>=1 orelse error "formula contains a variable index less than 1";
+ TextIO.output (out, string_of_int i))
+ | write_formula (Not (BoolVar i)) =
+ (TextIO.output (out, "-");
+ write_formula (BoolVar i))
+ | write_formula (Not fm) =
+ (TextIO.output (out, "-(");
+ write_formula fm;
+ TextIO.output (out, ")"))
+ | write_formula (Or (fm1, fm2)) =
+ (TextIO.output (out, "+(");
+ write_formula_or fm1;
+ TextIO.output (out, " ");
+ write_formula_or fm2;
+ TextIO.output (out, ")"))
+ | write_formula (And (fm1, fm2)) =
+ (TextIO.output (out, "*(");
+ write_formula_and fm1;
+ TextIO.output (out, " ");
+ write_formula_and fm2;
+ TextIO.output (out, ")"))
(* optimization to make use of n-ary disjunction/conjunction *)
- (* prop_formula -> string list -> string list *)
- and sat_string_acc_or (Or (fm1,fm2)) acc =
- sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 acc)
- | sat_string_acc_or fm acc =
- sat_string_acc fm acc
- (* prop_formula -> string list -> string list *)
- and sat_string_acc_and (And (fm1,fm2)) acc =
- sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 acc)
- | sat_string_acc_and fm acc =
- sat_string_acc fm acc
+ and write_formula_or (Or (fm1, fm2)) =
+ (write_formula_or fm1;
+ TextIO.output (out, " ");
+ write_formula_or fm2)
+ | write_formula_or fm =
+ write_formula fm
+ and write_formula_and (And (fm1, fm2)) =
+ (write_formula_and fm1;
+ TextIO.output (out, " ");
+ write_formula_and fm2)
+ | write_formula_and fm =
+ write_formula fm
+ val number_of_vars = Int.max (maxidx fm, 1)
in
- sat_string_acc fm []
+ TextIO.output (out, "c This file was generated by SatSolver.write_dimacs_sat_file\n");
+ TextIO.output (out, "p sat " ^ string_of_int number_of_vars ^ "\n");
+ TextIO.output (out, "(");
+ write_formula fm;
+ TextIO.output (out, ")\n")
end
- val number_of_vars = Int.max (maxidx fm, 1)
in
- File.write path
- ("c This file was generated by SatSolver.write_dimacs_sat_file\n" ^
- "p sat " ^ string_of_int number_of_vars ^ "\n" ^
- "(");
- File.append_list path
- (sat_string fm);
- File.append path
- ")\n"
+ File.open_output write_sat_file path
end;
(* ------------------------------------------------------------------------- *)