1(* 2** This file contains specifications of the SAT tools that 3** can be invoked from HOL. 4** Details of format in the comments following each field name. 5** 6** {name (* solver name *) 7** URL, (* source for downloading *) 8** executable, (* path to executable *) 9** post_exe, (* path to post_processor executable if any *) 10** notime_run, (* command to invoke solver on a file *) 11** time_run, (* command to invoke on a file and time *) 12** post_run, (* transform SAT solver output before reading into HOL *) 13** only_true (* true if only the true atoms are listed in models *) 14** failure_string, (* string whose presence indicates unsatisfiability *) 15** start_string, (* string signalling start of variable assignment *) 16** end_string} (* string signalling end of variable assignment *) 17*) 18 19structure SatSolvers = 20struct 21 22datatype sat_solver = 23 SatSolver of 24 {name : string, 25 URL : string, 26 executable : string, 27 post_exe : string option, 28 notime_run : string -> string * string -> string , 29 time_run : string -> (string * string) * int -> string, 30 post_run : string -> (string * string) -> string , 31 only_true : bool, 32 failure_string : string, 33 start_string : string, 34 end_string : string}; 35 36fun getSolverName (SatSolver {name,...}) = name 37fun getSolverExe (SatSolver {executable,...}) = executable 38fun getSolverPostExe (SatSolver {post_exe,...}) = post_exe 39fun getSolverRun (SatSolver {notime_run,...}) = notime_run 40fun getSolverPostRun (SatSolver {post_run,...}) = post_run 41fun getSolverTrue (SatSolver {only_true,...}) = only_true 42fun getSolverFail (SatSolver {failure_string,...}) = failure_string 43fun getSolverStart (SatSolver {start_string,...}) = start_string 44fun getSolverEnd (SatSolver {end_string,...}) = end_string 45 46val p = Systeml.protect 47fun spacify [] = "" 48 | spacify [h] = h 49 | spacify (h::t) = h ^ " " ^ spacify t 50 51 52val zchaff = 53 SatSolver 54 {name = "zchaff", 55 URL = "http://www.princeton.edu/~chaff/zchaff", 56 executable = if isSome (Process.getEnv "OS") 57 andalso String.compare(valOf(Process.getEnv "OS"),"Windows_NT")=EQUAL 58 then Globals.HOLDIR^"/src/HolSat/sat_solvers/zchaff/zchaff.exe" 59 else Globals.HOLDIR^"/src/HolSat/sat_solvers/zchaff/zchaff", 60 post_exe = SOME (if isSome (Process.getEnv "OS") 61 andalso String.compare(valOf(Process.getEnv "OS"),"Windows_NT")=EQUAL 62 then Globals.HOLDIR^"/src/HolSat/sat_solvers/zc2hs/zc2hs.exe" 63 else Globals.HOLDIR^"/src/HolSat/sat_solvers/zc2hs/zc2hs"), 64 notime_run = (fn ex => fn (infile,outfile) => 65 spacify [p ex, p infile,">", p outfile]), 66 time_run = (fn ex => fn ((infile,outfile),time) => 67 spacify [p ex, p infile, p (Int.toString time), ">", 68 p outfile]), 69 post_run = (fn ex => fn (infile,outfile) => 70 spacify [p ex, p infile, "-m", 71 p (outfile ^ ".proof"), 72 "-z", 73 "resolve_trace", ">", "zc2hs_trace"]), 74 only_true = false, 75 failure_string = "UNSAT", 76 start_string = "Instance Satisfiable", 77 end_string = "Random Seed Used"}; 78 79val minisatp = 80 SatSolver 81 {name = "minisatp", 82 URL = "http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat", 83 executable = if isSome (Process.getEnv "OS") 84 andalso String.compare(valOf(Process.getEnv "OS"),"Windows_NT")=EQUAL 85 then Globals.HOLDIR^"/src/HolSat/sat_solvers/minisat/minisat.exe" 86 else Globals.HOLDIR^"/src/HolSat/sat_solvers/minisat/minisat", 87 post_exe = NONE, 88 notime_run = (fn ex => fn (infile,outfile) => 89 spacify [p ex, "-r", p outfile, "-p", 90 p (outfile^".proof"), p infile, "-x", ">", 91 p (outfile ^".stats")]), 92 time_run = (fn ex => fn ((infile,outfile),time) => 93 spacify [p ex, p infile, p (Int.toString time), ">", 94 p outfile]), 95 post_run = (fn _ => fn _ => ""), 96 only_true = false, 97 failure_string = "UNSAT", 98 start_string = "SAT", 99 end_string = " 0"}; 100 101end 102