parse_std_result_file renamed to read_std_result_file
authorwebertj
Sat Sep 24 02:53:08 2005 +0200 (2005-09-24)
changeset 1762049568e5e0450
parent 17619 026f7bbc8a0f
child 17621 afffade1697e
parse_std_result_file renamed to read_std_result_file
src/HOL/Tools/sat_solver.ML
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Fri Sep 23 23:28:59 2005 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Sat Sep 24 02:53:08 2005 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  	(* auxiliary functions to create external SAT solvers *)
     1.5  	val write_dimacs_cnf_file : Path.T -> PropLogic.prop_formula -> unit
     1.6  	val write_dimacs_sat_file : Path.T -> PropLogic.prop_formula -> unit
     1.7 -	val parse_std_result_file : Path.T -> string * string * string -> result
     1.8 +	val read_std_result_file  : Path.T -> string * string * string -> result
     1.9  	val make_external_solver  : string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver
    1.10  
    1.11  	val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula
    1.12 @@ -200,7 +200,7 @@
    1.13  	end;
    1.14  
    1.15  (* ------------------------------------------------------------------------- *)
    1.16 -(* parse_std_result_file: scans a SAT solver's output file for a satisfying  *)
    1.17 +(* read_std_result_file: scans a SAT solver's output file for a satisfying   *)
    1.18  (*      variable assignment.  Returns the assignment, or 'UNSATISFIABLE' if  *)
    1.19  (*      the file contains 'unsatisfiable', or 'UNKNOWN' if the file contains *)
    1.20  (*      neither 'satisfiable' nor 'unsatisfiable'.  Empty lines are ignored. *)
    1.21 @@ -215,7 +215,7 @@
    1.22  
    1.23  	(* Path.T -> string * string * string -> result *)
    1.24  
    1.25 -	fun parse_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) =
    1.26 +	fun read_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) =
    1.27  	let
    1.28  		(* string -> int list *)
    1.29  		fun int_list_from_string s =
    1.30 @@ -685,7 +685,7 @@
    1.31  		val outpath    = File.tmp_path (Path.unpack "result")
    1.32  		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
    1.33  		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
    1.34 -		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
    1.35 +		fun readfn ()  = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
    1.36  		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
    1.37  		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
    1.38  		val result     = SatSolver.make_external_solver cmd writefn readfn fm
    1.39 @@ -710,7 +710,7 @@
    1.40  		val outpath    = File.tmp_path (Path.unpack "result")
    1.41  		val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
    1.42  		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
    1.43 -		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
    1.44 +		fun readfn ()  = SatSolver.read_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
    1.45  		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
    1.46  		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
    1.47  		val result     = SatSolver.make_external_solver cmd writefn readfn fm
    1.48 @@ -735,7 +735,7 @@
    1.49  		val outpath    = File.tmp_path (Path.unpack "result")
    1.50  		val cmd        = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
    1.51  		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
    1.52 -		fun readfn ()  = SatSolver.parse_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
    1.53 +		fun readfn ()  = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
    1.54  		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
    1.55  		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
    1.56  		val result     = SatSolver.make_external_solver cmd writefn readfn fm