forked from backtracking/ocaml-bdd
-
Notifications
You must be signed in to change notification settings - Fork 0
/
CHANGES
34 lines (28 loc) · 1.31 KB
/
CHANGES
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
o new functions `mk_exists` and `mk_forall` for quantifier elimination
o new function `print` to print a BDD as nested "if..then..else"
o new function `print_compact` to print a BDD in a compact form using
conjunction and disjunction when possible, and falling back to
"if..then..else" otherwise
o new function `extract_known_values` to retrieve from a bdd the set of
variables whose Boolean value is entailed by the bdd.
o new function `count_sat_int`
November 13, 2018 (VERSION 0.4)
-------------------------------
o no more set_max_var -> a functor Make and a function 'make' instead
o new function restrict
o new functions constrain and restriction
o extend print_to_dot and display with optional print_var argument
All this contributed by Timothy Bourke (tbrk@github)
February 2, 2010 (version 0.3)
------------------------------
o new function random_sat
o new example in tiling.ml (tiling the 8x8 chessboard with 2x1 dominoes *)
o init removed and subsumed by set_max_var
o improved efficiency (one node table for each variable)
July 16, 2009 (version 0.2)
---------------------------
o fixed bug in count_sat (unused variables below the top variable where not
taken into account)
June 7, 2008 (version 0.1)
--------------------------
o LGPL license, with special exception for linking (see LICENSE)