Minisat/dimacs_tools.ml

   1
   2 (*open satCommonTools;;*)
   3
   4 (* translation from terms to DIMACS cnf and back  *)
   5
   6 (* mapping from HOL variable names to DIMACS  variable numbers
   7    is stored in a global assignable (i.e. reference) variable sat_var_map.
   8    The type of sat_var_map is (int * (term * int) map) ref and
   9    the integer first component is the next available number
  10    (i.e. it is one plus the number of elements in the map)
  11    in th second component (t,n), if n<0 then the literal represented
  12    is ~t (the stored t is never negated)
  13 *)
  14
  15 (*
  16   initialise sat_var_map to integer 1 paired with the empty map
  17  (in DIMACS  variable numbering starts from 1 because 0
  18   is the clause separator)
  19 *)
  20
  21 let sat_var_map = ref(1, Termmap.empty)
  22 let sat_var_arr = ref(Array.make 0 t_tm) (* varnum->+ve lit. *)
  23
  24 (*
  25  Reinitialise sat_var_map.
  26  Needs to be done for each translation of a term to DIMACS
  27  as numbers must be an initial segment of 1,2,3,...
  28  (otherwise grasp, zchaff etc may crash)
  29 *)
  30
  31 (*+1 'cos var numbers start at 1*)
  32 let initSatVarMap var_count =
  33   (sat_var_map := (1, Termmap.empty);
  34    sat_var_arr := Array.make (var_count+1) t_tm)
  35
  36
  37 (*
  38  Lookup the var number corresponding to a +ve literal s, possibly extending sat_var_map
  39 *)
  40
  41 let lookup_sat_var s =
  42   let (c,svm) = !sat_var_map in
  43   snd (try Termmap.find s svm with
  44     Not_found ->
  45       let svm' = Termmap.add s (s,c) svm in
  46       let _    = (sat_var_map := (c+1,svm')) in
  47       let _    =
  48         try (Array.set (!sat_var_arr) c s)
  49         with Invalid_argument _  ->
  50           failwith ("lookup_sat_varError: "^(string_of_term s)^"::"^(string_of_int c)^"\n") in
  51       (t_tm,c))
  52
  53
  54 (*
  55  Lookup the +ve lit corresponding to a var number
  56 *)
  57 let lookup_sat_num n =
  58   try (Array.get (!sat_var_arr) n)
  59   with Invalid_argument _ ->
  60     failwith ("lookup_sat_numError: "^(string_of_int n)^"\n")
  61
  62
  63 (*
  64  Show sat_var_map as a list of its elements
  65 *)
  66
  67 let showSatVarMap () =
  68  let (c,st) = !sat_var_map in
  69   (c, List.map snd (tm_listItems st))
  70
  71 (*
  72  Print a term showing types
  73 *)
  74
  75 let all_string_of_term t =
  76   ((string_of_term) t^" : "^(string_of_type (type_of t)))
  77
  78 let print_all_term t =
  79   print_string (all_string_of_term t);;
  80
  81 (*
  82  Convert a literal to a (bool * integer) pair, where
  83  the boolean is true iff the literal is negated,
  84  if necessary extend sat_var_map
  85 *)
  86
  87 exception Lit_to_int_err of string
  88
  89 let literalToInt t =
  90   let (sign,v) =
  91       if is_neg t
  92       then
  93         let t1 = dest_neg t in
  94         if type_of t1 = bool_ty
  95         then (true, t1)
  96         else raise (Lit_to_int_err (all_string_of_term t))
  97       else
  98         if type_of t = bool_ty
  99         then (false, t)
 100         else raise (Lit_to_int_err (all_string_of_term t)) in
 101   let v_num = lookup_sat_var v in
 102   (sign, v_num)
 103
 104 (*
 105  Convert an integer (a possibly negated var number) to a literal,
 106  raising lookup_sat_numError if the absolute value of
 107  the integer isn't in sat_var_map
 108 *)
 109 let intToLiteral n =
 110     let t = lookup_sat_num (abs n) in
 111     if n>=0 then t else mk_neg t
 112
 113 (*
 114  termToDimacs t
 115  checks t is CNF of the form
 116   ``(v11 \/ ... \/ v1p) /\ (v21 \/ ... \/ v2q) /\ ... /\ (vr1 \/ ... \/vrt)``
 117  where vij is a literal, i.e. a boolean variable or a negated
 118  boolean variable.
 119  If t is such a CNF then termToDimacs t returns a list of lists of integers
 120  [[n11,...,n1p],[n21,...,n2q], ... , [nr1,...,nrt]]
 121  If vij is a boolean variable ``v`` then nij is the entry
 122  for v in sat_var_map. If vij is ``~v``, then nij is the negation
 123  of the entry for v in sat_var_map
 124  N.B. Definition of termToDimacs processes last clause first,
 125       so variables are not numbered in the left-to-right order.
 126       Not clear if this matters.
 127 *)
 128
 129 let termToDimacs t =
 130  List.fold_right
 131   (fun c d ->  (List.map literalToInt (disjuncts c)) :: d)
 132   (conjuncts t) []
 133
 134 (* Test data
 135 val t1 = ``x:bool``;
 136 val t2 = ``~x``;
 137 val t3 = ``x \/ y \/ ~z \/ w``;
 138 val t4 = ``(x \/ y \/ ~z \/ w) /\ (~w \/ ~x \/ y)``;
 139 val t5 = ``(x \/ y \/ ~z \/ w) /\ !x. (~w \/ ~x \/ y)``;
 140 val t6 = ``(x \/ y \/ ~z \/ w) /\ (~w)``;
 141 val t7 = ``(x \/ y \/ ~z \/ w) /\ (~w) /\ (w \/ x) /\ (p /\ q /\ r)``;
 142 *)
 143
 144 (*
 145  reference containing prefix used to make variables from numbers
 146  when reading DIMACS
 147 *)
 148
 149 let prefix = ref "v"
 150
 151 (*
 152  intToPrefixedLiteral n = ``(!prefix)n``
 153  intToPrefixedLiteral (~n) = ``~(!prefix)n``
 154 *)
 155
 156 let intToPrefixedLiteral n =
 157  if n >= 0
 158   then mk_var(((!prefix) ^ (string_of_int n)), bool_ty)
 159   else mk_neg(mk_var((!prefix) ^ (string_of_int(abs n)), bool_ty))
 160
 161 (*
 162  buildClause [n1,...,np] builds
 163  ``(!prefix)np /\ ... /\ (!prefix)n1``
 164  Raises exception Empty on the empty list
 165 *)
 166
 167 let buildClause l =
 168  List.fold_left
 169   (fun t n -> mk_disj(intToPrefixedLiteral n, t))
 170   (intToPrefixedLiteral (hd l))
 171   (tl l)
 172
 173 (*
 174  dimacsToTerm l
 175  converts a list of integers
 176  [n11,...,n1p,0,n21,...,n2q,0, ... , 0,nr1,...,nrt,0]
 177  into a term in CNF of the form
 178   ``(v11 \/ ... \/ v1p) /\ (v21 \/ ... \/ v2q) /\ ... /\ (vr1 \/ ... \/vrt)``
 179  where vij is a literal, i.e. a boolean variable or a negated boolena variable.
 180  If nij is non-negative then vij is ``(!prefix)nij``;
 181  If nij is negative ~mij then vij is ``~(!prefix)mij``;
 182 *)
 183
 184 (* dimacsToTerm_aux splits off one clause, dimacsToTerm iterates it *)
 185 let rec dimacsToTerm_aux acc = function
 186  [] -> (buildClause acc,[])
 187  | (0::l) -> (buildClause acc,l)
 188  | (x::l) -> dimacsToTerm_aux (x::acc) l
 189
 190 let rec dimacsToTerm l =
 191  let (t,l1) = dimacsToTerm_aux [] l in
 192  if List.length l1 = 0
 193  then t
 194  else mk_conj(t, dimacsToTerm l1)
 195
 196 (*
 197  Convert (true,n) to "-n" and (false,n) to "n"
 198 *)
 199
 200 let literalToString b n =
 201   if b
 202   then ("-" ^ (string_of_int n))
 203   else string_of_int n
 204
 205 (*
 206  termToDimacsFile t
 207  converts t to DIMACS  and then writes out a
 208  file into the temporary directory.
 209  the name of the temporary file (without extension ".cnf") is returned.
 210 *)
 211
 212 (*
 213  Refererence containing name of temporary file used
 214  for last invocation of a SAT solver
 215 *)
 216
 217 let tmp_name = ref "undefined"
 218
 219 let termToDimacsFile fname t var_count =
 220   let clause_count = List.length(conjuncts t) in
 221   let _            = initSatVarMap var_count in
 222   let dlist        = termToDimacs t in
 223   let tmp          = Filename.temp_file "sat" "" in
 224   let tmpname      =
 225     match fname with
 226       (Some fname) -> fname^".cnf"
 227     | None ->  tmp^".cnf" in
 228   let outstr       = open_out tmpname in
 229   let out s        = output_string outstr s in
 230   let res = (out "c File "; out tmpname; out " generated by HolSatLib\n";
 231              out "c\n";
 232              out "p cnf ";
 233              out (string_of_int var_count); out " ";
 234              out (string_of_int clause_count); out "\n";
 235              List.iter
 236                 (fun l -> (List.iter (fun (x,y) ->
 237                   (out(literalToString x y); out " ")) l;
 238                            out "\n0\n"))
 239                dlist;
 240              close_out outstr;
 241              tmp_name := tmp;
 242              match fname with
 243                (Some _) ->  tmpname
 244              | None -> tmp) in
 245   res;;
 246
 247 (*
 248  readDimacs filename
 249  reads a DIMACS  file called filename and returns
 250  a term in CNF in which each number n in the DIMACS file
 251  is a boolean variable (!prefix)n
 252  Code below by Ken Larsen (replaces earlier implementation by MJCG)
 253 *)
 254 exception Read_dimacs_error;;
 255
 256 let rec dropLine ins =
 257   match Stream.peek ins with
 258     Some '\n' -> Stream.junk ins
 259   | Some _    -> (Stream.junk ins; dropLine ins)
 260   | None      -> raise Read_dimacs_error
 261
 262 let rec stripPreamble ins =
 263   match Stream.peek ins with
 264     Some 'c' -> (dropLine ins; stripPreamble ins)
 265   | Some 'p' -> (dropLine ins; stripPreamble ins)
 266   | Some _   -> Some ()
 267   | None     -> None
 268
 269 let rec getIntClause lex acc =
 270   match
 271     (try Stream.next lex with
 272       Stream.Failure -> Genlex.Kwd "EOF" (* EOF *))
 273   with
 274     (Genlex.Int 0)     -> Some acc
 275   | (Genlex.Int i)     -> getIntClause lex (i::acc)
 276   | (Genlex.Kwd "EOF") ->
 277       if List.length acc = 0
 278       then None
 279       else Some acc
 280    |  _                 -> raise Read_dimacs_error
 281
 282
 283 (* This implementation is inspired by
 284    (and hopefully faithful to) dimacsToTerm.
 285 *)
 286 let getTerms lex =
 287   let rec loop acc =
 288     match getIntClause lex [] with
 289       Some ns -> loop (mk_conj(buildClause ns, acc))
 290     | None    -> Some acc in
 291   match getIntClause lex [] with
 292     Some ns -> loop (buildClause ns)
 293   | None    -> None
 294
 295 let readTerms ins =
 296   match stripPreamble ins with
 297     Some _ ->
 298       let lex = (Genlex.make_lexer ["EOF"] ins) in
 299       getTerms lex
 300   | None     -> None
 301
 302 let readDimacs filename =
 303  (*let val fullfilename = Path.mkAbsolute(filename, FileSys.getDir())*)
 304   let inf          = Pervasives.open_in filename in
 305   let ins          = Stream.of_channel inf in
 306   let term         = readTerms ins in
 307   (close_in inf;
 308    match term with Some t -> t | None -> raise Read_dimacs_error)
 309