1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
open String
let read_from_file filename =
let lines = ref "" in
let chan = open_in filename in
try
while true; do
let line = input_line chan in
if (length line>0)&&(not ((line.[0]) = 'c')) then
lines := (!lines)^"\n"^line
done; ""
with End_of_file ->
close_in chan;
!lines
let latexescaped = function
| '%' | '{' | '}' as c -> "\\"^Char.escaped c
| c -> Char.escaped c
let rec list_from_string s list_so_far n =
if (n>=length s) then List.rev list_so_far
else
match s.[n] with
| ' ' | '\n' | '\t' -> list_from_string s list_so_far (n+1)
| '-' -> list_from_string s ("-"::list_so_far) (n+1)
| _ ->
let rec word_from_string s word_so_far n =
if (n>=length s) then List.rev (word_so_far::list_so_far)
else
begin
match s.[n] with
| ' '| '\n' | '\t' -> list_from_string s (word_so_far::list_so_far) n
| c -> word_from_string s (word_so_far^(latexescaped c)) (n+1)
end
in
word_from_string s "" n
let rec _print_list = function
| [] -> ()
| s::l -> print_string (s^" "); _print_list l
module PairLit = struct
type t = bool*int
let _negation (b,s) = (not b,s)
end
let rec parse_cnf cnf_so_far: string list -> PairLit.t list list = function
| [] -> List.rev cnf_so_far
| "0"::l -> parse_cnf (cnf_so_far) l
| l -> let rec parse_clause clause_so_far ispos = function
| [] -> parse_cnf ((List.rev clause_so_far)::cnf_so_far) []
| "0"::l -> parse_cnf ((List.rev clause_so_far)::cnf_so_far) l
| "-"::l -> parse_clause clause_so_far false l
| s::l -> parse_clause ((ispos,int_of_string s)::clause_so_far) true l
in parse_clause [] true l
let parse_cnf_file l =
let aux _nbvar = function
| "p"::"cnf"::nbvar::_nbclauses::l -> parse_cnf [] l, int_of_string nbvar
| _ -> assert false
in
aux 0 l
type t = (bool * int) list list * int
let (parse: string -> t) = fun x -> try
list_from_string (read_from_file x) [] 0
|> parse_cnf_file
with _e -> failwith (Printf.sprintf "Is file %s a valid dimacs file?" x)
let (print: t -> string) = fun (pll,_) ->
let p_to_str (b,n) = if b then string_of_int n else "not("^string_of_int n^")" in
let pl_to_str pl =
List.fold_left
(fun acc p -> Printf.sprintf "%s or %s" acc (p_to_str p))
(p_to_str (List.hd pl))
(List.tl pl)
in
List.fold_left
(fun acc pl -> Printf.sprintf "%s and \n%s" acc (pl_to_str pl))
(pl_to_str (List.hd pll))
(List.tl pll)
let make_var i = Var.make "" ((string_of_int i)) Type.BoolT Var.Output
let (gen_vars : int -> Exp.var list) = fun size ->
let rec aux acc i =
if i > size then acc else aux ((make_var i)::acc) (i+1)
in
aux [] 1
let (to_formula : t -> Exp.var list * Exp.formula) = fun (pll, size) ->
let p_to_bdd (b,n) =
let v = Exp.Bvar (make_var n) in
if b then v else Exp.Not(v)
in
let pl_to_bdd pl =
List.fold_left
(fun acc p -> Exp.Or (acc, (p_to_bdd p)))
(p_to_bdd (List.hd pl))
(List.tl pl)
in
let f =
List.fold_left
(fun acc pl -> Exp.And (acc, (pl_to_bdd pl)))
(pl_to_bdd (List.hd pll))
(List.tl pll)
in
let vl = gen_vars size in
vl, f