Minisat/sat_solvers.ml

   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   good_exit,      (* code return upon normal termination                 *)
  10   notime_run,     (* command to invoke solver on a file                  *)
  11   time_run,       (* command to invoke on a file and time                *)
  12   only_true       (* true if only the true atoms are listed in models    *)
  13   failure_string, (* string whose presence indicates unsatisfiability    *)
  14   start_string,   (* string signalling start of variable assignment      *)
  15   end_string}     (* string signalling end of variable assignment        *)
  16 *)
  17
  18 type sat_solver =
  19   {name           : string;
  20    url            : string;
  21    executable     : string;
  22    good_exit      : int;
  23    notime_run     : string -> string * string -> string;
  24    time_run       : string -> (string * string) * int -> string;
  25    only_true      : bool;
  26    failure_string : string;
  27    start_string   : string;
  28    end_string     : string}
  29
  30 let zchaff =
  31   {name           = "zchaff";
  32    url            =
  33     "http://www.ee.princeton.edu/~chaff/zchaff/zchaff.2001.2.17.linux.gz";
  34    executable     = "zchaff";
  35    good_exit      = 0;
  36    notime_run     = (fun ex -> fun (infile,outfile) ->
  37                   (ex ^ " " ^ infile ^ " > " ^ outfile ^
  38                    "; zc2mso " ^ infile ^
  39                    " -m " ^ outfile ^ ".proof -z "^
  40                    (Filename.concat (!temp_path) "resolve_trace")^
  41                    "> "^
  42                    (Filename.concat (!temp_path) "zc2mso_trace")));
  43    time_run       = (fun ex -> fun ((infile,outfile),time) ->
  44                       (ex ^ " " ^ infile ^ " " ^ (string_of_int time) ^ " > " ^ outfile));
  45    only_true      = false;
  46    failure_string = "UNSAT";
  47    start_string   = "Instance Satisfiable";
  48    end_string     = "Random Seed Used"}
  49
  50 let minisat =
  51   {name           = "minisat";
  52    url            = "http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/cgi/MiniSat_v1.13_linux.cgi";
  53    executable     = "minisat";
  54    good_exit      = 10;
  55    notime_run     = (fun ex -> fun (infile,outfile) ->
  56                       (ex ^ " -r " ^ outfile ^" "^ infile ^ " > " ^ outfile ^".stats"));
  57    time_run       = (fun ex -> fun ((infile,outfile),time) ->
  58                       (ex ^ " " ^ infile ^ " " ^ (string_of_int time) ^ " > " ^ outfile));
  59    only_true      = false;
  60    failure_string = "UNSAT";
  61    start_string   = "v";
  62    end_string     = "0"}
  63
  64 let minisatp =
  65   {name           = "minisatp";
  66    url            = "http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/cgi/MiniSat_v1.13_linux.cgi";
  67    executable     =
  68    (match (Sys.os_type) with
  69       "Win32" | "Cygwin" -> "minisat.exe"
  70     | _       -> "minisat");
  71    good_exit      = 10;
  72    notime_run     = (fun ex -> fun (infile,outfile) ->
  73                       (ex ^ " -r " ^ outfile ^ " -p " ^ outfile ^ ".proof " ^ infile ^ " > " ^ outfile ^".stats"));
  74    time_run       = (fun ex -> fun ((infile,outfile),time) ->
  75                       (ex ^ " " ^ infile ^ " " ^ (string_of_int time) ^ " > " ^ outfile));
  76    only_true      = false;
  77    failure_string = "UNSAT";
  78    start_string   = "SAT";
  79    end_string     = "0"}