-
Notifications
You must be signed in to change notification settings - Fork 2
/
buddy.mli
291 lines (214 loc) · 12.3 KB
/
buddy.mli
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
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
(**************************************************************************)
(* Copyright (C) 2008 Akihiko Tozawa and Masami Hagiya. *)
(* Copyright (C) 2009 2010 Pietro Abate <[email protected] *)
(* *)
(* This library is free software: you can redistribute it and/or modify *)
(* it under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 3 of the *)
(* License, or (at your option) any later version. A special linking *)
(* exception to the GNU Lesser General Public License applies to this *)
(* library, see the COPYING file for more information. *)
(**************************************************************************)
(** documentation from http://buddy.sourceforge.net/manual/modules.html *)
type bdd
type bddpair
type var = int
type value = False | True | Unknown
type solution = SAT | UNSAT | UNKNOWN
val value_of_var : var -> value
val string_of_value : value -> string
(** reordering strategy used by [bdd_autoreorder] *)
type reorder_strategy =
|Win2 (** Reordering using a sliding window of size 2. This algorithm swaps
two adjacent variable blocks and if this results in more nodes then the two
blocks are swapped back again. Otherwise the result is kept in the variable
order. This is then repeated for all variable blocks *)
|Win2ite (** The same as above but the process is repeated until no further
progress is done. Usually a fast and efficient method. *)
|Win3 (** The same as above but with a window size of 3. *)
|Win3ite (** The same as above but with a window size of 3. *)
|Sift (** Reordering where each block is moved through all possible positions.
The best of these is then used as the new position. Potentially a very slow
but good method. *)
|Siftite (** The same as above but the process is repeated until no further
progress is done. Can be extremely slow. *)
|Random (** Mostly used for debugging purpose, but may be usefull for others.
Selects a random position for each variable. *)
exception EmptyBdd
external bdd_compare : bdd -> bdd -> int = "wrapper_bdd_compare"
(** Initializes the bdd package. The [nodenum] parameter sets the initial number
of BDD nodes and [cachesize] sets the size of the caches used for the BDD
operators (not the unique node table).
Good initial values are :
* Small test examples: nodenum = 1000, cachesize = 100 (default)
* Small examples: nodenum = 10000, cachesize =1000
* Medium sized examples: nodenum = 100000, cachesize = 10000
* Large examples: nodenum = 1000000, cachesize = variable
*)
val bdd_init : ?nodenum : int -> ?cachesize : int -> unit -> unit
(** Resets the bdd package. *)
val bdd_done : unit -> unit
(** Set the number of used bdd variables. After the initialization a call must be
done to bdd_setvarnum to define how many variables to use in this session.
This number may be increased later on either by calls to setvarnum.
*)
external bdd_setvarnum : int -> unit = "wrapper_bdd_setvarnum"
(** Returns the number of defined variables. *)
external bdd_varnum : unit -> int = "wrapper_bdd_varnum"
(** {2 BDD operations} *)
(** Return a fresh variable. Increment the number of variables available in this
session if needed *)
val bdd_newvar : unit -> var
(** [bdd_pos x] Returns the bdd representing the variable [x]. Alias of [ithvar] *)
val bdd_pos : var -> bdd
(** [bdd_neg x] Returns the bdd representing the negation of the variable [x].
Alias of [nithvar] *)
val bdd_neg : var -> bdd
(** Returns the constant true bdd. *)
val bdd_true : bdd
(** Returns the constant false bdd. *)
val bdd_false : bdd
(** The logical negation of a bdd. *)
external bdd_not : bdd -> bdd = "wrapper_bdd_not"
(** The logical 'and' of two bdds. *)
external bdd_and : bdd -> bdd -> bdd = "wrapper_bdd_and"
(** The logical 'or' of two bdds. *)
external bdd_or : bdd -> bdd -> bdd = "wrapper_bdd_or"
(** The logical 'xor' of two bdds. *)
external bdd_xor : bdd -> bdd -> bdd = "wrapper_bdd_xor"
(** The logical 'implication' of two bdds. *)
external bdd_imp : bdd -> bdd -> bdd = "wrapper_bdd_imp"
(** The logical 'bi-implication' of two bdds. *)
external bdd_biimp : bdd -> bdd -> bdd = "wrapper_bdd_biimp"
(** Returns a bdd representing the i'th variable. The BDDs returned from
bdd_ithvar can then be used to form new BDDs by calling bdd_OP where
OP may be bddop_and or any of the other operators
*)
external bdd_ithvar : int -> bdd = "wrapper_bdd_ithvar"
(** Returns a bdd representing the negation of the i'th variable. *)
external bdd_nithvar : int -> bdd = "wrapper_bdd_nithvar"
(** If-then-else operator. Calculates the BDD for the expression
$(f \land g) \lor (\lnot f \land h)$ more efficiently than doing
the three operations separately.
*)
external bdd_ite : bdd -> bdd -> bdd -> bdd = "wrapper_bdd_ite"
external bdd_exist : bdd -> bdd -> bdd = "wrapper_bdd_exist"
external bdd_forall : bdd -> bdd -> bdd = "wrapper_bdd_forall"
val bdd_diff : bdd -> bdd -> bdd
val bdd_bigor : bdd list -> bdd
val bdd_bigand : bdd list -> bdd
external bdd_appex : bdd -> bdd -> int -> bdd -> bdd = "wrapper_bdd_appex"
external bdd_appall : bdd -> bdd -> int -> bdd -> bdd = "wrapper_bdd_appall"
(** Finds all satisfying variable assignments. [bdd_allsat r handler] iterates
through all legal variable assignments (those that make the BDD come true)
for the bdd [r] and calls the callback handler [handler] for each of them. *)
val bdd_allsat : ((var * value) list -> unit) -> bdd -> unit
(** [bdd_satone r] Finds one satisfying variable assignment. Finds a BDD with
at most one variable at each level. This BDD implies [r] and is not false
unless [r] is false. *)
external bdd_satone : bdd -> bdd = "wrapper_bdd_satone"
(** [bdd_satoneset r var pol] Finds one satisfying variable assignment. The
[var] argument is a variable list that defines a set of variables that
must be mentioned in the result. The polarity of these variables in
result --- in case they are undefined in [r] --- are defined by the
[pol] parameter. If pol is false then the variables will be in negative
form, and otherwise they will be in positive form. *)
val bdd_satoneset : ?pol:bool -> bdd -> var list -> bdd
(** [bdd_makeset: l] Builds a bdd variable set from an var list. The BDD
variable set is represented as the conjunction of all the variables
in their positive form and may just as well be made that way by the user. *)
external bdd_makeset : var list -> bdd = "wrapper_bdd_makeset"
external bdd_simplify : bdd -> bdd -> bdd = "wrapper_bdd_restrict"
(** [bdd_var r] gets the top level variable of the [r]. *)
external bdd_var : bdd -> var = "wrapper_bdd_var"
(** [bdd_low r] gets the true branch of the top level variable of [r]. *)
external bdd_high : bdd -> bdd = "wrapper_bdd_high"
(** [bdd_low r] gets the false branch of the top lelve variable of [r]. *)
external bdd_low : bdd -> bdd = "wrapper_bdd_low"
(* [bdd_restrict r var] restricts the variables in [r] to constant true or false. How
this is done depends on how the variables are included in the variable set
var. If they are included in their positive form then they are restricted to
true and vice versa. In other words, for each variable in var, it selects
either the true or false branch of [r] wrt the polarity. *)
external bdd_restrict : bdd -> bdd -> bdd = "wrapper_bdd_restrict"
(** Returns the variable support of a bdd. [bdd_support r] finds all the
variables that r depends on. That is the support of r. *)
external bdd_support : bdd -> bdd = "wrapper_bdd_support"
external bdd_nodecount : bdd -> int = "wrapper_bdd_nodecount"
external bdd_newpair : unit -> bddpair = "wrapper_bdd_newpair"
external bdd_setpair : bddpair -> int -> int -> int = "wrapper_bdd_setpair"
external bdd_replace : bdd -> bddpair -> bdd = "wrapper_bdd_replace"
(** Add a variable block for all variables. *)
external bdd_varblockall : unit -> unit = "wrapper_bdd_varblockall"
(** Add a new variable block for reordering. *)
external bdd_addvarblock : bdd -> int -> int = "wrapper_bdd_addvarblock"
(** Add a new variable block for reordering. *)
external bdd_intaddvarblock : int -> int -> int -> int = "wrapper_bdd_intaddvarblock"
(** Start dynamic reordering. *)
val bdd_reorder : ?strategy : reorder_strategy -> unit -> unit
(** Enable automatic reordering. *)
val bdd_autoreorder : ?strategy : reorder_strategy -> unit -> unit
(** set a specific variable order. if the variable list (x1, ..., xn) is a
subset of the bdd variables (y1 ... ym), then the order will be as
(x1, ..., xn, 1 ... m) *)
val bdd_setvarorder : int list -> unit
val bdd_getvarorder : unit -> int list
(** Enables automatic reordering. *)
external bdd_enable_reorder : unit -> unit = "wrapper_bdd_enable_reorder"
(** Disable automatic reordering. *)
external bdd_disable_reorder : unit -> unit = "wrapper_bdd_disable_reorder"
(** Enables verbose information about reorderings. *)
external bdd_reorder_verbose : int -> int = "wrapper_bdd_reorder_verbose"
(** Prints the current order to [out_channel] *)
external bdd_fprintorder : out_channel -> unit = "wrapper_bdd_fprintorder"
(** Fetch the level of a specific bdd variable. *)
external bdd_level2var : int -> int = "wrapper_bdd_level2var"
(** Fetch the variable number of a specific level. *)
external bdd_var2level : int -> int = "wrapper_bdd_var2level"
external bdd_setmaxincrease : int -> int = "wrapper_bdd_setmaxincrease"
external bdd_setminfreenodes : int -> int = "wrapper_bdd_setminfreenodes"
external bdd_setcacheratio : int -> int = "wrapper_bdd_setcacheratio"
external bdd_fprinttable : out_channel -> bdd -> unit = "wrapper_bdd_fprinttable"
external bdd_fprintdot : out_channel -> bdd -> unit = "wrapper_bdd_fprintdot"
external bdd_fprintset : out_channel -> bdd -> unit = "wrapper_bdd_fprintset"
external bdd_load : in_channel -> bdd = "wrapper_bdd_load"
external bdd_save : out_channel -> bdd -> unit = "wrapper_bdd_save"
(** create a conjunction of positive variables *)
external bdd_createset : (int -> bool) -> bdd = "wrapper_bdd_createset"
val bdd_relprod : (int -> bool) -> bdd -> bdd -> bdd
(* [bdd_setfold f d a] fold through a certain set satisfying [d] *)
val bdd_setfold : (int -> 'a -> 'a) -> bdd -> 'a -> 'a
(** {2 FDD operations} *)
(** Adds another set of finite domain blocks. *)
external fdd_extdomain : int -> int = "wrapper_fdd_extdomain"
(** Combine two fdd blocks into one. *)
external fdd_overlapdomain : int -> int -> int = "wrapper_fdd_overlapdomain"
(** Clear all allocated fdd blocks. *)
external fdd_clearall : unit -> unit = "wrapper_fdd_clearall"
(** Number of defined finite domain blocks. *)
external fdd_domainnum : unit -> int = "wrapper_fdd_domainnum"
(** Real size of a finite domain block. *)
external fdd_domainsize : int -> int = "wrapper_fdd_domainsize"
(** Binary size of a finite domain block. *)
external fdd_varnum : int -> int = "wrapper_fdd_varnum"
(** All bdd variables associated with a finite domain block. *)
external fdd_vars : int -> int array = "wrapper_fdd_vars"
(** The bdd for the i'th fdd set to a specific value. *)
external fdd_ithvar : int -> int -> bdd = "wrapper_fdd_ithvar"
(** The variable set for the i'th finite domain block. *)
external fdd_ithset : int -> bdd = "wrapper_fdd_ithset"
(** Bdd encoding of the domain of a fdd variable. *)
external fdd_domain : int -> bdd = "wrapper_fdd_domain"
(** Returns a bdd setting two fdd variables equal. *)
external fdd_equals : int -> int -> bdd = "wrapper_fdd_equals"
(** Prints a bdd for a finite domain block to stdout. *)
external fdd_printset : bdd -> unit = "wrapper_fdd_printset"
(** Adds a new variable block for reordering. *)
external fdd_intaddvarblock : int -> int -> int -> int = "wrapper_fdd_intaddvarblock"
(** Defines a pair for two finite domain blocks. *)
external fdd_setpair : bddpair -> int -> int -> int = "wrapper_fdd_setpair"
(** Finds all satisfying variable assignments. [fdd_allsat handler r vars]
iterates through all assignments to the fdd variables [vars] satisfying
the relation [r] and calls the callback handler [handler] for each of
them. *)
val fdd_allsat : (int list -> unit) -> bdd -> int list -> unit