Minisat/sat_tools.ml

   1
   2 (*open dimacsTools;;*)
   3
   4 (* Functions for parsing the DIMACS-compliant output of SAT solvers,
   5    This is generic. Parser for minisat proof log is in minisatParse.ml  *)
   6
   7 (*
   8 ** Use Binaryset to encode mapping between HOL variable names
   9 ** and DIMACS  variable numbers as a set of string*int pairs.
  10 *)
  11
  12 (*
  13 ** substringContains s ss
  14 ** tests whether substring ss contains string s
  15 *)
  16
  17 let substringContains s ss =
  18   let re = Str.regexp_string s in
  19   match
  20     (try Str.search_forward re ss 0 with
  21       Not_found -> -1) with
  22     -1 -> false
  23   | _  -> true
  24
  25
  26 (*
  27 ** parseSat (s1,s2) ss
  28 ** returns a list of numbers corresponding to the tokenised
  29 ** substring of ss (tokenised wrt Char.isSpace) that starts immediately
  30 ** after the first occurrence of s1 and ends just before the first
  31 ** occurrence of s2 that is after the first occurrence of s1
  32 *)
  33
  34 let parseSat (s1,s2) ss =
  35   let p1 = Str.search_forward (Str.regexp s1) ss 0 in
  36   let p2 = Str.search_backward (Str.regexp s2) ss (String.length ss) in
  37   let ss1 = Str.string_before ss p2 in
  38   let ss2 = Str.string_after ss1 (p1+String.length s1) in
  39   let ssl = Str.split (Str.regexp "[ \n\t\r]") ss2 in
  40   List.map int_of_string ssl
  41
  42
  43 (*
  44 ** invokeSat solver t
  45 ** invokes solver on t and returns SOME s (where s is the satisfying instance
  46 ** as a string of integers) or NONE, if unsatisfiable
  47 *)
  48
  49 (*
  50 ** Reference containing last command used to invoke a SAT solver
  51 *)
  52
  53 let sat_command = ref "undef"
  54
  55 (*
  56 ** Test for success of the result of Process.system
  57 ** N.B. isSuccess expected to primitive in next release of
  58 ** Moscow ML, and Process.status will lose eqtype status
  59 *)
  60
  61 let satdir = "";;
  62
  63 (* if fname is NONE, then use a temp file, otherwise assume fname.cnf alredy exists*)
  64 let invokeSat sat_solver fname t vc =
  65   let {name=name;
  66        url=url;
  67        executable=executable;
  68        good_exit=good_exit;
  69        notime_run=notime_run;
  70        time_run=time_run;
  71        only_true=only_true;
  72        failure_string=failure_string;
  73        start_string=start_string;
  74        end_string=end_string} = sat_solver in
  75   let var_count  =
  76     match vc with
  77       Some n -> n |
  78       None -> List.length(variables t) in
  79   let tmp        =
  80     match fname with
  81       Some fnm ->
  82         (initSatVarMap var_count;
  83          ignore (termToDimacs t); (*FIXME: this regenerates sat_var_map:
  84                                     better to save/load it*)
  85          fnm)
  86     | None     -> termToDimacsFile None t var_count in
  87   let infile     = tmp ^ ".cnf" in
  88   let outfile    = tmp ^ "." ^ name in
  89   let ex         = Filename.concat satdir executable in
  90   let run_cmd    = notime_run ex (infile,outfile) in
  91   let _          = (sat_command := run_cmd) in
  92   let code       = Sys.command run_cmd in
  93   let _          =
  94     if ((name = "minisat") or (name = "minisatp") or (code = good_exit))
  95     then ()
  96     else print_string("Warning:\n Failure signalled by\n " ^ run_cmd ^ "\n") in
  97   let ins        = Pervasives.open_in outfile in
  98   let sat_res    = input_all ins in
  99   let _          = close_in ins in
 100   let result     = substringContains failure_string sat_res in
 101   if result
 102   then None
 103   else
 104     let model1 = parseSat(start_string,end_string) sat_res in
 105     let model2 =
 106       if only_true
 107       then model1
 108         @
 109           (List.map
 110              (fun n -> 0-n)
 111              (subtract (List.map snd (snd(showSatVarMap()))) model1))
 112       else model1 in
 113     Some (List.map intToLiteral model2)
 114
 115
 116 (*
 117 ** satOracle sat_solver t
 118 ** invokes sat_solver on t and returns a theorem tagged by the solver name
 119 ** of the form |- (l1 /\ ... ln) ==> t (satisfied with literals l1,...,ln)
 120 ** or |- ~t (failure)
 121 *)
 122
 123 let satOracle sat_solver t =
 124   let res = invokeSat sat_solver None t None in
 125   match res with
 126     Some l -> mk_thm ([], mk_imp(list_mk_conj l, t))
 127   | None   -> mk_thm ([], mk_neg t)
 128
 129 (*
 130 ** satProve sat_solver t
 131 ** invokes sat_solver on t and if a model is found then
 132 ** then it is verified using proof in HOL and a theorem
 133 ** |- (l1 /\ ... /\ ln) ==> t is returned
 134 ** (where l1,...,ln are the literals making up the model);
 135 ** Raises satProveError if no model is found.
 136 ** Raises satCheckError if the found model is bogus
 137 *)
 138
 139 (*
 140 ** satCheck [l1,...,ln] t
 141 ** attempts to prove (l1 /\ ... /\ ln) ==> t
 142 ** if it succeeds then the theorem is returned, else
 143 ** exception satCheckError is raised
 144 *)
 145
 146 let EQT_Imp1 = TAUT `!b. b ==> (b<=>T)`
 147 let EQF_Imp1 = TAUT `!b. (~b) ==> (b<=>F)`
 148 let EQT_Imp2 = TAUT `!b. (b<=>T) ==> b`;;
 149
 150 exception Sat_check_error
 151
 152 let satCheck model t =
 153  try
 154    let mtm  = list_mk_conj model in
 155    let th1  = ASSUME mtm in
 156    let thl  = List.map
 157        (fun th ->
 158          if is_neg(concl th)
 159          then MP (SPEC (dest_neg(concl th)) EQF_Imp1) th
 160          else MP (SPEC (concl th) EQT_Imp1) th)
 161        (CONJUNCTS th1) in
 162    let th3 = SUBS_CONV thl t in
 163    let th4 = CONV_RULE(RAND_CONV(REWRITE_CONV[])) th3 in
 164    let th5 = MP (SPEC t EQT_Imp2) th4 in
 165    DISCH mtm th5
 166  with
 167    Sys.Break -> raise Sys.Break
 168  | _         -> raise Sat_check_error;;
 169
 170 exception Sat_prove_error
 171
 172 (* old interface by MJCG. assumes t is in cnf; only for finding SAT *)
 173 let satProve sat_solver t  =
 174  match invokeSat sat_solver None t None with
 175    Some model -> satCheck model t
 176  | None       -> raise Sat_prove_error
 177