912 |
912 |
913 let |
913 let |
914 fun zchaff fm = |
914 fun zchaff fm = |
915 let |
915 let |
916 val _ = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () |
916 val _ = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () |
917 val _ = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso |
|
918 (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else () |
|
919 (* both versions of zChaff appear to have the same interface, so we do *) |
|
920 (* not actually need to distinguish between them in the following code *) |
|
921 val serial_str = serial_string () |
917 val serial_str = serial_string () |
922 val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) |
918 val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) |
923 val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) |
919 val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) |
924 val cmd = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) |
920 val cmd = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) |
925 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) |
921 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) |
941 (* ------------------------------------------------------------------------- *) |
937 (* ------------------------------------------------------------------------- *) |
942 |
938 |
943 let |
939 let |
944 fun berkmin fm = |
940 fun berkmin fm = |
945 let |
941 let |
946 val _ = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else () |
942 val _ = if (getenv "BERKMIN_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () |
947 val serial_str = serial_string () |
943 val serial_str = serial_string () |
948 val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) |
944 val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) |
949 val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) |
945 val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) |
950 val cmd = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) |
946 val exec = getenv "BERKMIN_EXE" |
|
947 val cmd = (getenv "BERKMIN_HOME") ^ "/" ^ (if exec = "" then "BerkMin561" else exec) ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) |
951 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) |
948 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) |
952 fun readfn () = SatSolver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!") |
949 fun readfn () = SatSolver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!") |
953 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
950 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
954 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
951 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
955 val result = SatSolver.make_external_solver cmd writefn readfn fm |
952 val result = SatSolver.make_external_solver cmd writefn readfn fm |