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