-
Notifications
You must be signed in to change notification settings - Fork 0
/
solver.ml
130 lines (117 loc) · 2.87 KB
/
solver.ml
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
124
125
126
127
128
129
open Printf
open Picosat
let drop str n =
let l = String.length str in
String.sub str n (l - n)
let take str n = String.sub str 0 n
let split str ch =
let rec split' str l =
try
let i = String.index str ch in
let t = take str i in
let str' = drop str (i+1) in
let l' = t::l in
split' str' l'
with Not_found ->
List.rev (str::l)
in
split' str []
let process_file file =
(* Mapping between variable names and indices. *)
let vars = Hashtbl.create 0 in
(* Processes a line containing a variable definition. *)
let process_var line =
let l = String.length line in
assert (l > 2);
assert (line.[1] = ' ');
let name = drop line 2 in
let v = Picosat.new_var () in
Hashtbl.add vars name v
in
(* Processes a line containing a clause. *)
let process_clause line =
let l = String.length line in
assert (l > 2);
assert (line.[1] = ' ');
let lits =
List.map
(fun lit ->
if lit.[0] = '-' then
(false, drop lit 1)
else
(true, lit)
)
(split (drop line 2) ' ')
in
let clause =
List.map
(fun (sign, name) ->
let var = Hashtbl.find vars name in
if sign then
Picosat.pos_lit var
else
Picosat.neg_lit var
)
lits
in
Picosat.add_clause clause
in
(* Read a new line and processes its content. *)
let rec process_line () =
try
let line = input_line file in
if line = "" then
()
else
(match line.[0] with
| 'v' -> process_var line
| 'c' -> process_clause line
| '#' -> ()
| _ -> assert false
);
process_line ()
with End_of_file ->
()
in
process_line ();
vars
let solve file =
Picosat.init ();
let vars = process_file file in
let revs =
let acc = Hashtbl.create (Hashtbl.length vars) in
Hashtbl.iter (fun name v -> Hashtbl.add acc v name) vars ;
acc
in
match Picosat.solve () with
| Picosat.UNKNOWN -> printf "Limit exausted\n"
| Picosat.UNSAT ->
begin
printf "unsat\nunsat core : %s\n"
(String.concat "," (List.map (fun i -> (Hashtbl.find revs i)) (Picosat.unsatcore ())))
end
| Picosat.SAT ->
begin
printf "sat\nmodel : \n";
List.iter (fun i ->
printf " %s=%s\n"
(Hashtbl.find revs i)
(Picosat.string_of_value (Picosat.value_of i))
) (Picosat.model ())
end
;;
let main () =
let argc = Array.length Sys.argv in
if argc = 1 then
solve stdin
else
Array.iter
(fun fname ->
try
printf "Solving %s...\n" fname;
solve (open_in fname)
with Sys_error msg ->
printf "ERROR: %s\n" msg
)
(Array.sub Sys.argv 1 (argc-1))
let () = main ()