forked from flerda/MiniSat-ocaml
-
Notifications
You must be signed in to change notification settings - Fork 2
/
solver.ml
149 lines (136 loc) · 3.5 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
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
(* To use printf without referencing the model name *)
(* open Printf
open Minisat
*)
(*
* Returns the string obtained from [str] by dropping the first
* [n] characters. [n] must be smaller than or equal to the length
* of the string [str].
*)
let drop str n =
let l = String.length str in
String.sub str n (l - n)
(*
* Returns the first [n] characters of the string [str] as a string.
* [n] must be smaller than or equal to the length of the string [str].
*)
let take str n = String.sub str 0 n
(*
* Splits a string [str] whenever a character [ch] is encountered.
* The returns value is a list of strings.
*)
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 []
;;
(*
* Processes the content of [file], adds the variables and clauses to Minisat
* and returns a mapping between names and Minisat variables.
*)
let process_file solver 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 = solver#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 =
Array.map (fun (sign, name) ->
let var = Hashtbl.find vars name in
if sign then
Minisat.pos_lit var
else
Minisat.neg_lit var
) (Array.of_list lits)
in
ignore(solver#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
;;
(* Reads a given file and solves the instance. *)
let solve file =
let solver = new Minisat.solver in
let vars = process_file solver file in
if solver#solve then begin
Printf.printf "sat\n";
let model = solver#model in
Hashtbl.iter
(fun name v ->
Printf.printf "%d%!\n" v;
Printf.printf " %s=%s\n" name (Minisat.string_of_lbool model.(v))
)
vars
end
else begin
Printf.printf "unsat\n";
Array.iter (fun lit ->
Printf.printf "%d%s "
(Minisat.lit_to_var lit) (if Minisat.lit_sign lit then "" else "-")
) (solver#conflict)
end
;;
(*
* Solve the files given on the command line, or read one from standard
* input if none is given.
*)
let main () =
let argc = Array.length Sys.argv in
if argc = 1 then
solve stdin
else
Array.iter
(fun fname ->
try
Printf.printf "Solving %s...\n" fname;
solve (open_in fname)
with Sys_error msg ->
Printf.printf "ERROR: %s\n" msg
)
(Array.sub Sys.argv 1 (argc-1))
;;
main () ;;