QBF/qbfr.ml

   1 (* Code for reading QDicams.        *)
   2 (* Based on Minisat/dimacs_tools.ml *)
   3 (* from HOL Light distribution.     *)
   4
   5
   6 exception Read_dimacs_error;;
   7
   8 let prefix = ref "v_"
   9
  10 let intToPrefixedLiteral n =
  11  if n >= 0
  12   then mk_var(((!prefix) ^ (string_of_int n)), bool_ty)
  13   else mk_neg(mk_var((!prefix) ^ (string_of_int(abs n)), bool_ty))
  14
  15 let buildClause l =
  16  List.fold_left
  17   (fun t n -> mk_disj(intToPrefixedLiteral n, t))
  18   (intToPrefixedLiteral (hd l))
  19   (tl l)
  20
  21 let rec dropLine ins =
  22   match Stream.peek ins with
  23     Some '\n' -> Stream.junk ins
  24   | Some _    -> (Stream.junk ins; dropLine ins)
  25   | None      -> raise Read_dimacs_error
  26
  27 let rec stripPreamble ins =
  28   match Stream.peek ins with
  29     Some 'c' -> (dropLine ins; stripPreamble ins)
  30   | Some 'p' -> (dropLine ins; stripPreamble ins)
  31   | Some _   -> Some ()
  32   | None     -> None
  33
  34 let rec getIntClause lex acc =
  35   match
  36     (try Stream.next lex with
  37       Stream.Failure -> Genlex.Kwd "EOF" (* EOF *))
  38   with
  39     (Genlex.Int 0)     -> Some acc
  40   | (Genlex.Int i)     -> getIntClause lex (i::acc)
  41   | (Genlex.Kwd "EOF") ->
  42       if List.length acc = 0
  43       then None
  44       else Some acc
  45    |  _                 -> raise Read_dimacs_error
  46
  47 let rec getIntClause2 lex acc =
  48   match Stream.next lex with
  49     (Genlex.Int 0)     -> acc
  50   | (Genlex.Int i)     -> i::(getIntClause2 lex acc)
  51   | _ -> raise Read_dimacs_error
  52
  53 let getTerms lex start_acc =
  54   let rec loop acc =
  55     match getIntClause lex [] with
  56       Some ns -> loop (mk_conj(buildClause ns,acc))
  57     | None    -> Some acc in
  58   match getIntClause lex start_acc with
  59     Some ns -> loop (buildClause ns)
  60   | None    -> None
  61
  62 type qs = Qe of int list | Qa of int list;;
  63
  64 let read_quant lex =
  65   let rec loop acc =
  66   match Stream.next lex with
  67     Genlex.Kwd "e" ->
  68       let vars = getIntClause2 lex [] in
  69       let (acc',var) = loop acc in
  70       ((Qe vars)::acc',var)
  71     | Genlex.Kwd "a" ->
  72       let vars = getIntClause2 lex [] in
  73       let (acc',var) = loop acc in
  74       ((Qa vars)::acc',var)
  75     | Genlex.Int i -> (acc,i)
  76     | _ -> raise Read_dimacs_error
  77   in
  78   loop []
  79
  80 let var_map l =
  81    List.map intToPrefixedLiteral l
  82
  83 let add_quantifiers quant body =
  84   List.fold_right (fun quants b -> match quants with
  85                                    Qa l -> list_mk_forall (var_map l,b)
  86                                    | Qe l -> list_mk_exists (var_map l,b)
  87                   )
  88     quant body
  89
  90 let readTerms ins =
  91   match stripPreamble ins with
  92     Some _ ->
  93       let lex = (Genlex.make_lexer ["EOF";"e";"a"] ins) in
  94       let (quant,var) = read_quant lex in
  95       ( match getTerms lex [var] with
  96         Some body -> Some (add_quantifiers quant body)
  97         | None -> None )
  98   | None     -> None
  99
 100 let readQDimacs filename =
 101   let inf          = open_in filename in
 102   let ins          = Stream.of_channel inf in
 103   let term         = readTerms ins in
 104   (close_in inf;
 105    match term with Some t -> t | None -> raise Read_dimacs_error)
 106