File: NEWS

package info (click to toggle)
boolector 1.5.118.6b56be4.121013-1
  • links: PTS
  • area: main
  • in suites: bullseye, buster, jessie, jessie-kfreebsd, stretch
  • size: 2,220 kB
  • sloc: ansic: 47,665; sh: 422; cpp: 173; makefile: 155
file content (93 lines) | stat: -rw-r--r-- 2,972 bytes parent folder | download | duplicates (2)
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
news for release 1.5.118 since 1.5.116
--------------------------------------
* '--solver=...' command line option and 'boolector_set_sat_solver'
* delayed Lingeling preprocessing using 'simpdelay'

news for release 1.5.116 since 1.5.115
--------------------------------------
* examples compilable again
* fixed assertions in 'booolector.c'
* support for new reentrant PicoSAT API (since PicoSAT version 953)

news for release 1.5.115 since 1.5.13
------------------------------------
* added 'bvcomp'
* boolean top-level skeleton simplification
* use of 'lglclone' in incremental mode
* added some more rewriting
* removed 3VL code
* removed PrecoSAT, basicbtor
* in-depth, look-ahead, interval
* incremental SMTLIB1 interface
* added MiniSAT support
* rebuilding AIGs / Expressions
* more compact SMTLIB1 parsing
* symbolic lemmas instead of direct CNF encoding
* more compact AIG to CNF translation
* gzip/bzip2/7z compressed input files
* time out option
* SMTLIB 2 support

news for release 1.5.13 since 1.4.1
----------------------------------
* new incremental mode for multiple formulas in SMT benchmarks
* integration of MiniSAT
* SMT parser demotes logic if possible
* better control of best suitable solver in main application
* generic incremental SAT glue logic
* integration of Lingeling

news for release 1.4.1 since 1.4
--------------------------------
* MacOS port
* disabled unconstrained optimization

news for release 1.4 since 1.3
------------------------------
* hid API change in 'picosat_add' for older version of PicoSAT
* fixed EOF issue reading an empty file from stdin
* removed old license references

news for release 1.3 since 1.2
------------------------------
* first source code release
* fixed a rewriting bug by uncommenting simplification code

news for release 1.2 since 1.1
------------------------------
* improved rewriting 
* PrecoSAT now standard solver for non-incremental usage, 
  PicoSAT used otherwise

news for release 1.1 since 1.0
------------------------------
* improved handling of unconstrained variables and arrays
* improved rewriting engine
* removed command line switch for refinement limit
* fixed bug where Boolector could report 'unknown' in regular (non-bmc) mode
* fixed minor caching problem on AIG layer 
* fixed other bugs

news for release 1.0 since 0.7
------------------------------
* public C API
* documentation and examples
* improved SMT parser (:formula can now be an fvar).

news for release 0.7 since 0.6
------------------------------
* fixed model generation bugs
* improved under-approximation
* added support for bvcomp (SMT-LIB)

news for release 0.6 since 0.5
------------------------------
* fixed model generation bugs
* fixed rewriting bug
* support for new under-approximation techniques

news for release 0.5 since 0.4
------------------------------
* faster model generation
* support for array models
* support for under-approximation techniques for bit-vector variables and reads