-
Notifications
You must be signed in to change notification settings - Fork 2
/
CHANGELOG
44 lines (35 loc) · 2.64 KB
/
CHANGELOG
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
# Changelog
## [Unreleased]
### New
- added option '--verbose' for verbose output with multiple levels of verbosity using easylogging++ ('-v' is now for '--verbose', use '-V' for '--version')
- added implementation of initial BDD ordering of variables based on expected order of elimination (variables that are first to eliminate are on the lowest level)
- added option '--initial-ordering' that defines the initial ordering of BDD variables (1 is the new initial ordering based on order of elimination, 0 is the old one)
### Fixes
- (D)QCIR parser now expects '#QCIR-G14' at the beginning of the file, not '#QCIR-14' (and gives only warning instead of exception if it does not start with it)
## [1.3] - 20-04-2022
### New
- added parsing of non-cleansed prenex (D)QCIR format
- added two new options '--dqcir-output' and '--dqcir-output-cleansed' for printing parsed and possibly preprocessed input into given output file in non-cleansed or cleansed prenex DQCIR format (the option '--hqspre-dqcir-output' was removed, as '--dqcir-output-cleansed' with preprocessing turned on replaces it)
- quantifier trees used for localisation can now share subtrees, significantly reducing memory usage
## [1.2] - 09-04-2021
### Fixes
- added checks in DQDIMACS parser for errors and fixed parsing of free variables
- some solved instances by HQSpre during parsing were not caught, leading to a thrown exception
- the copies of universal variables (which DQBDD does not rename) will now not be taken into account for computing the conditions of pushing existential variables for disjunction
### New
- added parser for QBFs in prenex cleansed (D)QCIR format (prenex DQCIR is like prenex QCIR, where we can add quantifier depend(v, v1, ..., vn) which represents existential variable v with dependency set {v1, ..., vn})
- added an option to force file format (otherwise it is selected automatically by file type)
- DQBDD now works also on Mac
- changed how localisation is computed to save on memory/time
- added option '--hqspre-dqcir-output' which takes filename.dqdimacs file, preprocesses it with HQSpre and transforms the result (with gate extraction) into filename.dqcir
## [1.1] - 26-04-2020
### Fixes
- dynamic reordering is temporarily turned off during creation of existential dependency copies
### New
- added option to turn on/off dynamic reordering (turned on by default)
## [1.0] - 24-04-2020
- initial release
[1.3]: https://github.com/jurajsic/DQBDD/releases/tag/v1.3
[1.2]: https://github.com/jurajsic/DQBDD/releases/tag/v1.2
[1.1]: https://github.com/jurajsic/DQBDD/releases/tag/v1.1
[1.0]: https://github.com/jurajsic/DQBDD/releases/tag/v1.0