--- a/src/HOL/Tools/sat_solver.ML Tue Jun 22 10:05:47 2004 +0200
+++ b/src/HOL/Tools/sat_solver.ML Tue Jun 22 14:14:08 2004 +0200
@@ -88,31 +88,38 @@
| cnf_number_of_clauses _ =
1
(* prop_formula -> string *)
- fun cnf_string True =
- error "formula is not in CNF"
- | cnf_string False =
- error "formula is not in CNF"
- | cnf_string (BoolVar i) =
- (assert (i>=1) "formula contains a variable index less than 1";
- string_of_int i)
- | cnf_string (Not fm) =
- "-" ^ cnf_string fm
- | cnf_string (Or (fm1,fm2)) =
- cnf_string fm1 ^ " " ^ cnf_string fm2
- | cnf_string (And (fm1,fm2)) =
- cnf_string fm1 ^ " 0\n" ^ cnf_string fm2
+ fun cnf_string fm =
+ 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 =
+ (assert (i>=1) "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)
+ in
+ concat (cnf_string_acc fm [])
+ end
in
File.write path
(let
val fm' = cnf_True_False_elim fm
val number_of_vars = maxidx fm'
val number_of_clauses = cnf_number_of_clauses fm'
- val cnfstring = cnf_string fm'
in
"c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^
"c (c) Tjark Weber\n" ^
"p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n" ^
- cnfstring ^ " 0\n"
+ cnf_string fm' ^ " 0\n"
end)
end;
@@ -128,19 +135,25 @@
fun write_dimacs_sat_file path fm =
let
(* prop_formula -> string *)
- fun sat_string True =
- "*()"
- | sat_string False =
- "+()"
- | sat_string (BoolVar i) =
- (assert (i>=1) "formula contains a variable index less than 1";
- string_of_int i)
- | sat_string (Not fm) =
- "-(" ^ sat_string fm ^ ")"
- | sat_string (Or (fm1,fm2)) =
- "+(" ^ sat_string fm1 ^ " " ^ sat_string fm2 ^ ")"
- | sat_string (And (fm1,fm2)) =
- "*(" ^ sat_string fm1 ^ " " ^ sat_string fm2 ^ ")"
+ fun sat_string fm =
+ 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 =
+ (assert (i>=1) "formula contains a variable index less than 1";
+ string_of_int i :: acc)
+ | sat_string_acc (Not fm) acc =
+ "-(" :: sat_string_acc fm (")" :: acc)
+ | sat_string_acc (Or (fm1,fm2)) acc =
+ "+(" :: sat_string_acc fm1 (" " :: sat_string_acc fm2 (")" :: acc))
+ | sat_string_acc (And (fm1,fm2)) acc =
+ "*(" :: sat_string_acc fm1 (" " :: sat_string_acc fm2 (")" :: acc))
+ in
+ concat (sat_string_acc fm [])
+ end
in
File.write path
(let