# HG changeset patch
# User webertj
# Date 1127523188 -7200
# Node ID 49568e5e0450586720157588e3f43e61e188a93e
# Parent  026f7bbc8a0f37932c3518909deb67c1d15c9856
parse_std_result_file renamed to read_std_result_file

diff -r 026f7bbc8a0f -r 49568e5e0450 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Fri Sep 23 23:28:59 2005 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Sat Sep 24 02:53:08 2005 +0200
@@ -20,7 +20,7 @@
 	(* auxiliary functions to create external SAT solvers *)
 	val write_dimacs_cnf_file : Path.T -> PropLogic.prop_formula -> unit
 	val write_dimacs_sat_file : Path.T -> PropLogic.prop_formula -> unit
-	val parse_std_result_file : Path.T -> string * string * string -> result
+	val read_std_result_file  : Path.T -> string * string * string -> result
 	val make_external_solver  : string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver
 
 	val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula
@@ -200,7 +200,7 @@
 	end;
 
 (* ------------------------------------------------------------------------- *)
-(* parse_std_result_file: scans a SAT solver's output file for a satisfying  *)
+(* read_std_result_file: scans a SAT solver's output file for a satisfying   *)
 (*      variable assignment.  Returns the assignment, or 'UNSATISFIABLE' if  *)
 (*      the file contains 'unsatisfiable', or 'UNKNOWN' if the file contains *)
 (*      neither 'satisfiable' nor 'unsatisfiable'.  Empty lines are ignored. *)
@@ -215,7 +215,7 @@
 
 	(* Path.T -> string * string * string -> result *)
 
-	fun parse_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) =
+	fun read_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) =
 	let
 		(* string -> int list *)
 		fun int_list_from_string s =
@@ -685,7 +685,7 @@
 		val outpath    = File.tmp_path (Path.unpack "result")
 		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
-		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
+		fun readfn ()  = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
 		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
 		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
@@ -710,7 +710,7 @@
 		val outpath    = File.tmp_path (Path.unpack "result")
 		val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
-		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
+		fun readfn ()  = SatSolver.read_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
 		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
 		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
@@ -735,7 +735,7 @@
 		val outpath    = File.tmp_path (Path.unpack "result")
 		val cmd        = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
-		fun readfn ()  = SatSolver.parse_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
+		fun readfn ()  = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
 		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
 		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
 		val result     = SatSolver.make_external_solver cmd writefn readfn fm