567 let |
567 let |
568 exception INVALID_PROOF of string |
568 exception INVALID_PROOF of string |
569 fun minisat_with_proofs fm = |
569 fun minisat_with_proofs fm = |
570 let |
570 let |
571 val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () |
571 val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () |
572 val inpath = File.tmp_path (Path.explode "isabelle.cnf") |
572 val serial_str = serial_string () |
573 val outpath = File.tmp_path (Path.explode "result") |
573 val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) |
574 val proofpath = File.tmp_path (Path.explode "result.prf") |
574 val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) |
|
575 val proofpath = File.tmp_path (Path.explode ("result" ^ serial_str ^ ".prf")) |
575 val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " -t " ^ (Path.implode proofpath) ^ "> /dev/null" |
576 val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " -t " ^ (Path.implode proofpath) ^ "> /dev/null" |
576 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm |
577 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm |
577 fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT") |
578 fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT") |
578 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
579 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
579 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
580 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
752 |
753 |
753 let |
754 let |
754 fun minisat fm = |
755 fun minisat fm = |
755 let |
756 let |
756 val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () |
757 val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () |
757 val inpath = File.tmp_path (Path.explode "isabelle.cnf") |
758 val serial_str = serial_string () |
758 val outpath = File.tmp_path (Path.explode "result") |
759 val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) |
|
760 val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) |
759 val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " > /dev/null" |
761 val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " > /dev/null" |
760 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) |
762 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) |
761 fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT") |
763 fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT") |
762 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
764 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
763 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
765 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
914 val _ = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () |
916 val _ = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () |
915 val _ = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso |
917 val _ = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso |
916 (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else () |
918 (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else () |
917 (* both versions of zChaff appear to have the same interface, so we do *) |
919 (* both versions of zChaff appear to have the same interface, so we do *) |
918 (* not actually need to distinguish between them in the following code *) |
920 (* not actually need to distinguish between them in the following code *) |
919 val inpath = File.tmp_path (Path.explode "isabelle.cnf") |
921 val serial_str = serial_string () |
920 val outpath = File.tmp_path (Path.explode "result") |
922 val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) |
|
923 val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) |
921 val cmd = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) |
924 val cmd = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) |
922 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) |
925 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) |
923 fun readfn () = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable") |
926 fun readfn () = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable") |
924 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
927 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
925 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
928 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
939 |
942 |
940 let |
943 let |
941 fun berkmin fm = |
944 fun berkmin fm = |
942 let |
945 let |
943 val _ = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else () |
946 val _ = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else () |
944 val inpath = File.tmp_path (Path.explode "isabelle.cnf") |
947 val serial_str = serial_string () |
945 val outpath = File.tmp_path (Path.explode "result") |
948 val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) |
|
949 val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) |
946 val cmd = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) |
950 val cmd = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) |
947 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) |
951 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) |
948 fun readfn () = SatSolver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!") |
952 fun readfn () = SatSolver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!") |
949 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
953 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
950 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
954 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
964 |
968 |
965 let |
969 let |
966 fun jerusat fm = |
970 fun jerusat fm = |
967 let |
971 let |
968 val _ = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () |
972 val _ = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () |
969 val inpath = File.tmp_path (Path.explode "isabelle.cnf") |
973 val serial_str = serial_string () |
970 val outpath = File.tmp_path (Path.explode "result") |
974 val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) |
|
975 val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) |
971 val cmd = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) |
976 val cmd = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) |
972 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) |
977 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) |
973 fun readfn () = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE") |
978 fun readfn () = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE") |
974 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
979 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
975 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
980 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |