# HG changeset patch # User webertj # Date 1242915812 -3600 # Node ID 034f2310463555373b79263c1142afb6e3f26760 # Parent 3dde56615750825b2ab64aad024ec8c1417ba418 write_dimacs_{sat,cnf}_file now write the DIMACS file on the fly, without building it in memory first diff -r 3dde56615750 -r 034f23104635 src/HOL/Tools/sat_solver.ML --- 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; (* ------------------------------------------------------------------------- *)