author webertj Thu, 21 May 2009 15:25:44 +0100 changeset 31221 0a3a9bd5ca83 parent 31218 fa54c1e614df (current diff) parent 31220 f1c0ed85a33b (diff) child 31224 6f4fb815439a
merged
```--- a/src/HOL/Tools/prop_logic.ML	Wed May 20 22:24:07 2009 +0200
+++ b/src/HOL/Tools/prop_logic.ML	Thu May 21 15:25:44 2009 +0100
@@ -1,7 +1,6 @@
(*  Title:      HOL/Tools/prop_logic.ML
-    ID:         \$Id\$
Author:     Tjark Weber

Formulas of propositional logic.
*)
@@ -33,7 +32,6 @@

val nnf    : prop_formula -> prop_formula  (* negation normal form *)
val cnf    : prop_formula -> prop_formula  (* conjunctive normal form *)
-	val auxcnf : prop_formula -> prop_formula  (* cnf with auxiliary variables *)
val defcnf : prop_formula -> prop_formula  (* definitional cnf *)

val eval : (int -> bool) -> prop_formula -> bool  (* semantics *)
@@ -156,7 +154,7 @@
fun dot_product (xs,ys) = exists (map SAnd (xs~~ys));

(* ------------------------------------------------------------------------- *)
-(* is_nnf: returns 'true' iff the formula is in negation normal form (i.e.   *)
+(* is_nnf: returns 'true' iff the formula is in negation normal form (i.e.,  *)
(*         only variables may be negated, but not subformulas).              *)
(* ------------------------------------------------------------------------- *)

@@ -178,7 +176,8 @@

(* ------------------------------------------------------------------------- *)
(* is_cnf: returns 'true' iff the formula is in conjunctive normal form      *)
-(*         (i.e. a conjunction of disjunctions).                             *)
+(*         (i.e., a conjunction of disjunctions of literals). 'is_cnf'       *)
+(*         implies 'is_nnf'.                                                 *)
(* ------------------------------------------------------------------------- *)

local
@@ -197,170 +196,90 @@

(* ------------------------------------------------------------------------- *)
(* nnf: computes the negation normal form of a formula 'fm' of propositional *)
-(*      logic (i.e. only variables may be negated, but not subformulas).     *)
-(*      Simplification (c.f. 'simplify') is performed as well.               *)
+(*      logic (i.e., only variables may be negated, but not subformulas).    *)
+(*      Simplification (cf. 'simplify') is performed as well. Not            *)
+(*      surprisingly, 'is_nnf o nnf' always returns 'true'. 'nnf fm' returns *)
+(*      'fm' if (and only if) 'is_nnf fm' returns 'true'.                    *)
(* ------------------------------------------------------------------------- *)

(* prop_formula -> prop_formula *)

-	fun
-	(* constants *)
-	    nnf True                   = True
-	  | nnf False                  = False
-	(* variables *)
-	  | nnf (BoolVar i)            = (BoolVar i)
-	(* 'or' and 'and' as outermost connectives are left untouched *)
-	  | nnf (Or  (fm1, fm2))       = SOr  (nnf fm1, nnf fm2)
-	  | nnf (And (fm1, fm2))       = SAnd (nnf fm1, nnf fm2)
-	(* 'not' + constant *)
-	  | nnf (Not True)             = False
-	  | nnf (Not False)            = True
-	(* 'not' + variable *)
-	  | nnf (Not (BoolVar i))      = Not (BoolVar i)
-	(* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
-	  | nnf (Not (Or  (fm1, fm2))) = SAnd (nnf (SNot fm1), nnf (SNot fm2))
-	  | nnf (Not (And (fm1, fm2))) = SOr  (nnf (SNot fm1), nnf (SNot fm2))
-	(* double-negation elimination *)
-	  | nnf (Not (Not fm))         = nnf fm;
+	fun nnf fm =
+	let
+		fun
+			(* constants *)
+			    nnf_aux True                   = True
+			  | nnf_aux False                  = False
+			(* variables *)
+			  | nnf_aux (BoolVar i)            = (BoolVar i)
+			(* 'or' and 'and' as outermost connectives are left untouched *)
+			  | nnf_aux (Or  (fm1, fm2))       = SOr  (nnf_aux fm1, nnf_aux fm2)
+			  | nnf_aux (And (fm1, fm2))       = SAnd (nnf_aux fm1, nnf_aux fm2)
+			(* 'not' + constant *)
+			  | nnf_aux (Not True)             = False
+			  | nnf_aux (Not False)            = True
+			(* 'not' + variable *)
+			  | nnf_aux (Not (BoolVar i))      = Not (BoolVar i)
+			(* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
+			  | nnf_aux (Not (Or  (fm1, fm2))) = SAnd (nnf_aux (SNot fm1), nnf_aux (SNot fm2))
+			  | nnf_aux (Not (And (fm1, fm2))) = SOr  (nnf_aux (SNot fm1), nnf_aux (SNot fm2))
+			(* double-negation elimination *)
+			  | nnf_aux (Not (Not fm))         = nnf_aux fm
+	in
+		if is_nnf fm then
+			fm
+		else
+			nnf_aux fm
+	end;

(* ------------------------------------------------------------------------- *)
-(* cnf: computes the conjunctive normal form (i.e. a conjunction of          *)
-(*      disjunctions) of a formula 'fm' of propositional logic.  The result  *)
-(*      formula may be exponentially longer than 'fm'.                       *)
+(* cnf: computes the conjunctive normal form (i.e., a conjunction of         *)
+(*      disjunctions of literals) of a formula 'fm' of propositional logic.  *)
+(*      Simplification (cf. 'simplify') is performed as well. The result     *)
+(*      is equivalent to 'fm', but may be exponentially longer. Not          *)
+(*      surprisingly, 'is_cnf o cnf' always returns 'true'. 'cnf fm' returns *)
+(*      'fm' if (and only if) 'is_cnf fm' returns 'true'.                    *)
(* ------------------------------------------------------------------------- *)

(* prop_formula -> prop_formula *)

fun cnf fm =
let
-		fun
-		(* constants *)
-		    cnf_from_nnf True             = True
+		(* function to push an 'Or' below 'And's, using distributive laws *)
+		fun cnf_or (And (fm11, fm12), fm2) =
+			And (cnf_or (fm11, fm2), cnf_or (fm12, fm2))
+		  | cnf_or (fm1, And (fm21, fm22)) =
+			And (cnf_or (fm1, fm21), cnf_or (fm1, fm22))
+		(* neither subformula contains 'And' *)
+		  | cnf_or (fm1, fm2) =
+			Or (fm1, fm2)
+		fun cnf_from_nnf True             = True
| cnf_from_nnf False            = False
-		(* literals *)
| cnf_from_nnf (BoolVar i)      = BoolVar i
-		  | cnf_from_nnf (Not fm1)        = Not fm1  (* 'fm1' must be a variable since the formula is in NNF *)
-		(* pushing 'or' inside of 'and' using distributive laws *)
+		(* 'fm' must be a variable since the formula is in NNF *)
+		  | cnf_from_nnf (Not fm)         = Not fm
+		(* 'Or' may need to be pushed below 'And' *)
| cnf_from_nnf (Or (fm1, fm2))  =
-			let
-				fun cnf_or (And (fm11, fm12), fm2) =
-					And (cnf_or (fm11, fm2), cnf_or (fm12, fm2))
-				  | cnf_or (fm1, And (fm21, fm22)) =
-					And (cnf_or (fm1, fm21), cnf_or (fm1, fm22))
-				(* neither subformula contains 'and' *)
-				  | cnf_or (fm1, fm2) =
-					Or (fm1, fm2)
-			in
-				cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2)
-			end
-		(* 'and' as outermost connective is left untouched *)
-		  | cnf_from_nnf (And (fm1, fm2)) = And (cnf_from_nnf fm1, cnf_from_nnf fm2)
+		    cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2)
+		(* 'And' as outermost connective is left untouched *)
+		  | cnf_from_nnf (And (fm1, fm2)) =
+		    And (cnf_from_nnf fm1, cnf_from_nnf fm2)
in
-		(cnf_from_nnf o nnf) fm
+		if is_cnf fm then
+			fm
+		else
+			(cnf_from_nnf o nnf) fm
end;

(* ------------------------------------------------------------------------- *)
-(* auxcnf: computes the definitional conjunctive normal form of a formula    *)
-(*      'fm' of propositional logic, introducing auxiliary variables if      *)
-(*      necessary to avoid an exponential blowup of the formula.  The result *)
-(*      formula is satisfiable if and only if 'fm' is satisfiable.           *)
-(*      Auxiliary variables are introduced as switches for OR-nodes, based   *)
-(*      on the observation that e.g. "fm1 OR (fm21 AND fm22)" is             *)
-(*      equisatisfiable with "(fm1 OR ~aux) AND (fm21 OR aux) AND (fm22 OR   *)
-(*      aux)".                                                               *)
-(* ------------------------------------------------------------------------- *)
-
-(* ------------------------------------------------------------------------- *)
-(* Note: 'auxcnf' tends to use fewer variables and fewer clauses than        *)
-(*      'defcnf' below, but sometimes generates much larger SAT problems     *)
-(*      overall (hence it must sometimes generate longer clauses than        *)
-(*      'defcnf' does).  It is currently not quite clear to me if one of the *)
-(*      algorithms is clearly superior to the other, but I suggest using     *)
-(* ------------------------------------------------------------------------- *)
-
-	(* prop_formula -> prop_formula *)
-
-	fun auxcnf fm =
-	let
-		(* convert formula to NNF first *)
-		val fm' = nnf fm
-		(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
-		(* int ref *)
-		val new = ref (maxidx fm' + 1)
-		(* unit -> int *)
-		fun new_idx () = let val idx = !new in new := idx+1; idx end
-		(* prop_formula -> prop_formula *)
-		fun
-		(* constants *)
-		    auxcnf_from_nnf True  = True
-		  | auxcnf_from_nnf False = False
-		(* literals *)
-		  | auxcnf_from_nnf (BoolVar i) = BoolVar i
-		  | auxcnf_from_nnf (Not fm1)   = Not fm1  (* 'fm1' must be a variable since the formula is in NNF *)
-		(* pushing 'or' inside of 'and' using auxiliary variables *)
-		  | auxcnf_from_nnf (Or (fm1, fm2)) =
-			let
-				val fm1' = auxcnf_from_nnf fm1
-				val fm2' = auxcnf_from_nnf fm2
-				(* prop_formula * prop_formula -> prop_formula *)
-				fun auxcnf_or (And (fm11, fm12), fm2) =
-					(case fm2 of
-					(* do not introduce an auxiliary variable for literals *)
-					  BoolVar _ =>
-							And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2))
-					| Not _ =>
-							And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2))
-					| _ =>
-						let
-							val aux = BoolVar (new_idx ())
-						in
-							And (And (auxcnf_or (fm11, aux), auxcnf_or (fm12, aux)), auxcnf_or (fm2, Not aux))
-						end)
-				  | auxcnf_or (fm1, And (fm21, fm22)) =
-					(case fm1 of
-					(* do not introduce an auxiliary variable for literals *)
-					  BoolVar _ =>
-							And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22))
-					| Not _ =>
-							And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22))
-					| _ =>
-						let
-							val aux = BoolVar (new_idx ())
-						in
-							And (auxcnf_or (fm1, Not aux), And (auxcnf_or (fm21, aux), auxcnf_or (fm22, aux)))
-						end)
-				(* neither subformula contains 'and' *)
-				  | auxcnf_or (fm1, fm2) =
-					Or (fm1, fm2)
-			in
-				auxcnf_or (fm1', fm2')
-			end
-		(* 'and' as outermost connective is left untouched *)
-		  | auxcnf_from_nnf (And (fm1, fm2)) =
-				And (auxcnf_from_nnf fm1, auxcnf_from_nnf fm2)
-	in
-		auxcnf_from_nnf fm'
-	end;
-
-(* ------------------------------------------------------------------------- *)
-(* defcnf: computes the definitional conjunctive normal form of a formula    *)
-(*      'fm' of propositional logic, introducing auxiliary variables to      *)
-(*      avoid an exponential blowup of the formula.  The result formula is   *)
-(*      satisfiable if and only if 'fm' is satisfiable.  Auxiliary variables *)
-(*      are introduced as abbreviations for AND-, OR-, and NOT-nodes, based  *)
-(*      on the following equisatisfiabilities (+/- indicates polarity):      *)
-(*      LITERAL+       == LITERAL                                            *)
-(*      LITERAL-       == NOT LITERAL                                        *)
-(*      (NOT fm1)+     == aux AND (NOT aux OR fm1-)                          *)
-(*      (fm1 OR fm2)+  == aux AND (NOT aux OR fm1+ OR fm2+)                  *)
-(*      (fm1 AND fm2)+ == aux AND (NOT aux OR fm1+) AND (NOT aux OR fm2+)    *)
-(*      (NOT fm1)-     == aux AND (NOT aux OR fm1+)                          *)
-(*      (fm1 OR fm2)-  == aux AND (NOT aux OR fm1-) AND (NOT aux OR fm2-)    *)
-(*      (fm1 AND fm2)- == aux AND (NOT aux OR fm1- OR fm2-)                  *)
-(*      Example:                                                             *)
-(*      NOT (a AND b) == aux1 AND (NOT aux1 OR aux2)                         *)
-(*                            AND (NOT aux2 OR NOT a OR NOT b)               *)
+(* defcnf: computes a definitional conjunctive normal form of a formula 'fm' *)
+(*      of propositional logic. Simplification (cf. 'simplify') is performed *)
+(*      as well. 'defcnf' may introduce auxiliary Boolean variables to avoid *)
+(*      an exponential blowup of the formula.  The result is equisatisfiable *)
+(*      (i.e., satisfiable if and only if 'fm' is satisfiable), but not      *)
+(*      necessarily equivalent to 'fm'. Not surprisingly, 'is_cnf o defcnf'  *)
+(*      always returns 'true'. 'defcnf fm' returns 'fm' if (and only if)     *)
+(*      'is_cnf fm' returns 'true'.                                          *)
(* ------------------------------------------------------------------------- *)

(* prop_formula -> prop_formula *)
@@ -368,93 +287,66 @@
fun defcnf fm =
if is_cnf fm then
fm
-		else let
-			(* simplify formula first *)
-			val fm' = simplify fm
+		else
+		let
+			val fm' = nnf fm
(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
(* int ref *)
val new = ref (maxidx fm' + 1)
(* unit -> int *)
fun new_idx () = let val idx = !new in new := idx+1; idx end
-			(* optimization for n-ary disjunction/conjunction *)
-			(* prop_formula -> prop_formula list *)
-			fun disjuncts (Or (fm1, fm2)) = (disjuncts fm1) @ (disjuncts fm2)
-			| disjuncts fm1             = [fm1]
-			(* prop_formula -> prop_formula list *)
-			fun conjuncts (And (fm1, fm2)) = (conjuncts fm1) @ (conjuncts fm2)
-			| conjuncts fm1              = [fm1]
-			(* polarity -> formula -> (defining clauses, literal) *)
-			(* bool -> prop_formula -> prop_formula * prop_formula *)
-			fun
-			(* constants *)
-				defcnf' true  True  = (True, True)
-			| defcnf' false True  = (*(True, False)*) error "formula is not simplified, True occurs with negative polarity"
-			| defcnf' true  False = (True, False)
-			| defcnf' false False = (*(True, True)*) error "formula is not simplified, False occurs with negative polarity"
-			(* literals *)
-			| defcnf' true  (BoolVar i)       = (True, BoolVar i)
-			| defcnf' false (BoolVar i)       = (True, Not (BoolVar i))
-			| defcnf' true  (Not (BoolVar i)) = (True, Not (BoolVar i))
-			| defcnf' false (Not (BoolVar i)) = (True, BoolVar i)
-			(* 'not' *)
-			| defcnf' polarity (Not fm1) =
+			(* replaces 'And' by an auxiliary variable (and its definition) *)
+			(* prop_formula -> prop_formula * prop_formula list *)
+			fun defcnf_or (And x) =
let
-					val (def1, aux1) = defcnf' (not polarity) fm1
-					val aux          = BoolVar (new_idx ())
-					val def          = Or (Not aux, aux1)
+					val i = new_idx ()
in
-					(SAnd (def1, def), aux)
+					(* Note that definitions are in NNF, but not CNF. *)
+					(BoolVar i, [Or (Not (BoolVar i), And x)])
end
-			(* 'or' *)
-			| defcnf' polarity (Or (fm1, fm2)) =
+			  | defcnf_or (Or (fm1, fm2)) =
let
-					val fms          = disjuncts (Or (fm1, fm2))
-					val (defs, auxs) = split_list (map (defcnf' polarity) fms)
-					val aux          = BoolVar (new_idx ())
-					val def          = if polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs)
+					val (fm1', defs1) = defcnf_or fm1
+					val (fm2', defs2) = defcnf_or fm2
in
-					(SAnd (all defs, def), aux)
+					(Or (fm1', fm2'), defs1 @ defs2)
end
-			(* 'and' *)
-			| defcnf' polarity (And (fm1, fm2)) =
+			  | defcnf_or fm =
+				(fm, [])
+			(* prop_formula -> prop_formula *)
+			fun defcnf_from_nnf True             = True
+			  | defcnf_from_nnf False            = False
+			  | defcnf_from_nnf (BoolVar i)      = BoolVar i
+			(* 'fm' must be a variable since the formula is in NNF *)
+			  | defcnf_from_nnf (Not fm)         = Not fm
+			(* 'Or' may need to be pushed below 'And' *)
+			(* 'Or' of literal and 'And': use distributivity *)
+			  | defcnf_from_nnf (Or (BoolVar i, And (fm1, fm2))) =
+				And (defcnf_from_nnf (Or (BoolVar i, fm1)),
+				     defcnf_from_nnf (Or (BoolVar i, fm2)))
+			  | defcnf_from_nnf (Or (Not (BoolVar i), And (fm1, fm2))) =
+				And (defcnf_from_nnf (Or (Not (BoolVar i), fm1)),
+				     defcnf_from_nnf (Or (Not (BoolVar i), fm2)))
+			  | defcnf_from_nnf (Or (And (fm1, fm2), BoolVar i)) =
+				And (defcnf_from_nnf (Or (fm1, BoolVar i)),
+				     defcnf_from_nnf (Or (fm2, BoolVar i)))
+			  | defcnf_from_nnf (Or (And (fm1, fm2), Not (BoolVar i))) =
+				And (defcnf_from_nnf (Or (fm1, Not (BoolVar i))),
+				     defcnf_from_nnf (Or (fm2, Not (BoolVar i))))
+			(* all other cases: turn the formula into a disjunction of literals, *)
+			(*                  adding definitions as necessary                  *)
+			  | defcnf_from_nnf (Or x) =
let
-					val fms          = conjuncts (And (fm1, fm2))
-					val (defs, auxs) = split_list (map (defcnf' polarity) fms)
-					val aux          = BoolVar (new_idx ())
-					val def          = if not polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs)
+					val (fm, defs) = defcnf_or (Or x)
+					val cnf_defs   = map defcnf_from_nnf defs
in
-					(SAnd (all defs, def), aux)
-				end
-			(* optimization: do not introduce auxiliary variables for parts of the formula that are in CNF already *)
-			(* prop_formula -> prop_formula * prop_formula *)
-			fun defcnf_or (Or (fm1, fm2)) =
-				let
-					val (def1, aux1) = defcnf_or fm1
-					val (def2, aux2) = defcnf_or fm2
-				in
-					(SAnd (def1, def2), Or (aux1, aux2))
+					all (fm :: cnf_defs)
end
-			| defcnf_or fm =
-				defcnf' true fm
-			(* prop_formula -> prop_formula * prop_formula *)
-			fun defcnf_and (And (fm1, fm2)) =
-				let
-					val (def1, aux1) = defcnf_and fm1
-					val (def2, aux2) = defcnf_and fm2
-				in
-					(SAnd (def1, def2), And (aux1, aux2))
-				end
-			| defcnf_and (Or (fm1, fm2)) =
-				let
-					val (def1, aux1) = defcnf_or fm1
-					val (def2, aux2) = defcnf_or fm2
-				in
-					(SAnd (def1, def2), Or (aux1, aux2))
-				end
-			| defcnf_and fm =
-				defcnf' true fm
+			(* 'And' as outermost connective is left untouched *)
+			  | defcnf_from_nnf (And (fm1, fm2)) =
+				And (defcnf_from_nnf fm1, defcnf_from_nnf fm2)
in
-			SAnd (defcnf_and fm')
+			defcnf_from_nnf fm'
end;

(* ------------------------------------------------------------------------- *)
@@ -545,16 +437,16 @@

(* prop_formula -> Term.term *)
fun term_of_prop_formula True             =
-			HOLogic.true_const
-		| term_of_prop_formula False            =
-			HOLogic.false_const
-		| term_of_prop_formula (BoolVar i)      =
-			Free ("v" ^ Int.toString i, HOLogic.boolT)
-		| term_of_prop_formula (Not fm)         =
-			HOLogic.mk_not (term_of_prop_formula fm)
-		| term_of_prop_formula (Or (fm1, fm2))  =
-			HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2)
-		| term_of_prop_formula (And (fm1, fm2)) =
-			HOLogic.mk_conj (term_of_prop_formula fm1, term_of_prop_formula fm2);
+		HOLogic.true_const
+	  | term_of_prop_formula False            =
+		HOLogic.false_const
+	  | term_of_prop_formula (BoolVar i)      =
+		Free ("v" ^ Int.toString i, HOLogic.boolT)
+	  | term_of_prop_formula (Not fm)         =
+		HOLogic.mk_not (term_of_prop_formula fm)
+	  | term_of_prop_formula (Or (fm1, fm2))  =
+		HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2)
+	  | term_of_prop_formula (And (fm1, fm2)) =
+		HOLogic.mk_conj (term_of_prop_formula fm1, term_of_prop_formula fm2);

end;```
```--- a/src/HOL/Tools/sat_solver.ML	Wed May 20 22:24:07 2009 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Thu May 21 15:25:44 2009 +0100
@@ -1,7 +1,6 @@
(*  Title:      HOL/Tools/sat_solver.ML
-    ID:         \$Id\$
Author:     Tjark Weber

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;

(* ------------------------------------------------------------------------- *)```