/
NEWS
460 lines (425 loc) · 17.7 KB
/
NEWS
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
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
news since 3.2.3
news for release 3.2.3 since 3.2.2
--------------------------------------------------------------------------------
+ new API calls
- boolector_get_value
+ fix printing of constant arrays for get-value
+ build PyPi packages for Python version <=3.12
news for release 3.2.2 since 3.2.1
--------------------------------------------------------------------------------
+ fix issues in btormc
+ fix issue with get-value for Boolean variables
+ fix issue with get_failed_assumptions in combination with push/pop
+ fix get-unsat-assumptions printing
+ export enums for setting options (option values)
+ get-model is now SMT-LIB standard compliant
+ PyPi packages for Boolector
+ remove obsolete CL option --smt2-model (use -m --output-format=smt2 instead)
news for release 3.2.1 since 3.2.0
--------------------------------------------------------------------------------
+ initial version of Dockerfile for Boolector
(thanks to Andrew V. Jones)
+ fix issue with infinite recursion in Python API
(thanks to Andrew V. Jones)
+ fix issue with dumping constant arrays
+ fix issue with reset assumptions and checking of failed assumptions
+ fix witness printing in btormc
news for release 3.2.0 since 3.1.0
--------------------------------------------------------------------------------
+ new dumper CNF printer (enable with CLI option -dd and API option
BTOR_OPT_PRINT_DIMACS)
+ fix issue with model construction for constant arrays
+ boolector_sat is not automatically called on smt2 input anymore, must be
explicitly called via (check-sat) in the input file
+ smt2:
- support for parsing constant arrays
- support for :global-declarations
+ API changes:
- boolector_ror and boolector_rol now allow same bit-width for both operands
+ new API calls
- boolector_roli
- boolector_rori
news for release 3.1.0 since 3.0.0
--------------------------------------------------------------------------------
+ build system:
- requires now cmake >= 3.3
- exports library interface for using find_package(Boolector) in cmake projects
+ support for custom abort callback function
(called on abort instead of actually aborting)
+ Python API now throws Python exceptions on abort conditions
(e.g., when underlying C API is misused)
+ command line options that previously expected integer values denoting enum
values are now configured with strings denoting the particular modes that
can be selected; -<opt>=help and --<opt>=help allow to print detailed help
messages for these modes
+ fixed issue in SMT2 parser to correctly print echo commands
(thanks to Dominik Klumpp)
+ fixed race condition in Cython dependencies
(thanks to Marco Gario)
+ patches and documentation for building Boolector on Windows
(thanks to Andrew V. Jones)
+ support/use termination function feature of CaDiCaL
(thanks to Andrew V. Jones)
+ various fixes to contrib dependecy scripts
(thanks to Serge Bazanski)
+ new API calls
- boolector_copy_sort
- boolector_min_signed
- boolector_max_signed
- boolector_is_bv_const_zero
- boolector_is_bv_const_one
- boolector_is_bv_const_ones
- boolector_is_bv_const_min_signed
- boolector_is_bv_const_max_signed
+ CaDiCaL is now default SAT engine
+ support for constant arrays
+ support for GMP as bit-vector implementation
+ support for CyproMiniSat
- supports multi-threading via option --sat-engine-n-threads
+ switched to Google test as testing framework
+ CLI options changed (replaced ':' with a '-')
+ BtorMC improvements (HWMCC'19 version)
- k-induction engine with simple path constraints
+ Poolector Python script used in SMT-COMP'19
news for release 3.0.0 since 2.4.1
--------------------------------------------------------------------------------
+ new build system, requires cmake >= 2.8
- setup-*.sh scripts for dependencies (btor2parser, SAT solvers) in contrib
+ support for quantified bit-vectors (BV)
+ new bounded model checker BtorMC
+ support for new format BTOR2
+ support for CaDiCaL as SAT back-end
+ name of the Python module changed to pyboolector
+ SMT2 support for:
- echo
- declare-const
- check-sat-assuming
- get-unsat-assumptions
- set-option :produce-unsat-assumptions
- set-option :produce-assertions
- set-logic ALL
+ new API calls
- boolector_constd
- boolector_consth
- boolector_copyright
- boolector_exists
- boolector_forall
- boolector_get_failed_assumptions
- boolector_repeat
- boolector_pop
- boolector_push
- boolector_version
+ removed obsolete API calls
- boolector_set_sat_solver_lingeling
- boolector_set_sat_solver_minisat
- boolector_set_sat_solver_picosat
+ changes in API calls
- boolector_srl, boolector_sll and boolector_sra now supports operands with
the same bit-width (SMT-LIB v2 compatible)
+ various improvements and extensions of btormbt
news for release 2.4.1 since 2.4.0
--------------------------------------------------------------------------------
+ sequential portfolio combination of bit-blasting and SLS engine
(option --fun:presls) analogous to combination with PROP engine
(option --fun:preprop)
+ fixed: dumping smt2 nodes in incremental mode
news for release 2.4.0 since 2.3.1
--------------------------------------------------------------------------------
+ refactored, extended and improved btormbt
+ new API functions:
- boolector_is_uf
+ dumping smt2 nodes in incremental mode is now also possible if Boolector
compiled with assertions
+ fixed another issue with get-value
(thanks to Praveen Gundaram)
+ refactored model printing
+ command line option changes:
- --incremental-all -> --incremental-smt1
+ optimized lemma generation of function solver
news for release 2.3.1 since 2.3.0
--------------------------------------------------------------------------------
* fixed an issue with model printing (get-value)
(thanks to Levent Erkok)
news for release 2.3.0 since 2.2.0
--------------------------------------------------------------------------------
* new QF_BV engines
+ SLS engine
+ PROP engine
+ AIGPROP engine
* fixed an issue with model generation and lambda extraction
(thanks to Tim Blazytko)
* fixed an issue in boolector_int
(thanks to Niklas)
* fixed issue with printing BTOR models
* improved and extended option handling
+ boolector_get_opt_val -> boolector_get_opt
* many under-the-hood changes, refactoring, improvements
* API changes:
+ boolector_*_opt* now takes enum BtorOption instead of char* as argument
+ renamed:
- boolector_get_opt_val -> boolector_get_opt
+ the following functions now take BoolectorSort:
instead of int as argument:
- boolector_zero,
- boolector_ones,
- boolector_one,
- boolector_int,
- boolector_array,
- boolector_param
+ the following functions now return uint32_t instead of int:
- boolector_get_width
- boolector_get_index_width
- boolector_get_fun_arity
- boolector_get_opt (was boolector_get_opt_val)
- boolector_get_opt_min
- boolector_get_opt_max
- boolector_get_opt_dflt
+ the following functions now return bool instead of int:
- boolector_is_const
- boolector_is_var
- boolector_is_array
- boolector_is_array_var
- boolector_is_param
- boolector_is_bound_param
- boolector_is_fun
- boolector_is_equal_sort
- boolector_failed
+ the following options now return BtorOption instead of const char *
- boolector_first_opt
- boolector_next_opt
* new API functions:
+ boolector_unsigned_int
+ boolector_get_sort
+ boolector_fun_get_domain_sort
+ boolector_fun_get_codomain_sort
+ boolector_match_node_by_symbol
+ boolector_is_array_sort
+ boolector_is_bitvec_sort
+ boolector_is_fun_sort
+ boolector_has_opt
* dumping: new behavior:
+ boolector_dump_* does not simplify the formula before dumping anymore
(call boolector_simplify prior to dumping explicitely if necessary)
+ when dumping via the CL, the observable dumping behavior did not change
(formula is simplified prior to dumping)
news for release 2.2.0 since 2.1.1
--------------------------------------------------------------------------------
* refactored a lot of code
+ refactored and extended btormbt
+ refactored and improved array/lambda engine
+ refactored and extended lambda extraction
* removed SMT1 dumper (parsing SMT1 still supported)
* fixed push/pop support in SMT2 with model generation enabled
(thanks to James Bornholt)
* fixed an issue with model generation (thanks to Mikoláš Janota)
* fixed issues with failed assumptions
* API changes:
+ boolector_get_bits now requires to free returned bit strings via
boolector_free_bits (analogous to boolector_bv_assignment)
+ removed boolector_dump_smt1 and boolector_dump_smt1_node
+ removed deprecated functions boolector_enable_model_gen,
boolector_generate_model_for_all_reads, boolector_enable_inc_usage,
boolector_set_rewrite_level, boolector_set_verbosity,
boolector_set_loglevel, boolector_get_symbol_of_var
news for release 2.1.1 since 2.0.7
--------------------------------------------------------------------------------
* added support for array extensionality
* added lambda extraction (enabled by default)
* added model based testing tools btormbt and btoruntrace
* reduced memory footprint
* improved performance of cloning
* added support for push/pop in SMT-LIBv2 parser
* added support for :print-success in SMT-LIBv2 parser
* added support for dumping BV formulas in AIGER format (replaces synthebtor)
* API changes/additions:
+ added boolector_fixate_assumptions
+ added boolector_reset_assumptions
+ added boolector_dump_aiger_ascii
+ added boolector_dump_aiger_binary
+ changed boolector_*_sort
- now takes BoolectorSort instead of BoolectorSort* as arguments
* adpated and updated Python API to support new API
- Assert(), Assume(), and Failed() now support variable number of arguments
news for release 2.0.7 since 2.0.6
--------------------------------------------------------------------------------
* added option to (en|di)sable use of Boolector exit codes
* fixed help message issues
* fixed option handling issues
* fixed caching bug in model generation
* fixed issues with lambda hashing
* improved SMT dumpers
news for release 2.0.6 since 2.0.5
--------------------------------------------------------------------------------
* fixed printing issues in interactive SMT2 mode
* SMT2 parser now exits immediately after (exit) command was read
news for release 2.0.5 since 2.0.4
--------------------------------------------------------------------------------
* add support for termination callbacks (C and python API)
* smt2 parser: added option :regular-output-channel
* fixed smt2 interactivity issues
* fixed issue in Python API with Python 2.7 compatibility (__div__)
* fixed segmentation fault in SMT2 model printer
news for release 2.0.4 since 2.0.3
--------------------------------------------------------------------------------
* fixed bug in compare function for pointer hashing
* fixed performance issues when computing scores for don't care reasoning
* added smt2 models (get-value, get-model)
* fixed some issues in the Python API (thanks to Ryan Goulden)
* improved dumping of SMT2 formulas
news for release 2.0.3 since 2.0.1
--------------------------------------------------------------------------------
* fixed segmentation fault in back annotation for 'synthebtor'
* reenabled verbosity output for SAT solvers during search
* removed stale empty lines in triple verbose output
* fixed compilation issues with gcc/g++ 4.4
news for release 2.0.1 since 2.0.0
--------------------------------------------------------------------------------
* fixes bug in model generation
news for release 2.0.0 since 1.6.0
--------------------------------------------------------------------------------
* General:
+ Boolector python API
+ cloning support
+ support for uninterpreted functions
+ new improved model generation, supports two modes now:
- --model-gen=1 or -m:
generate model for all asserted expressions
(same as model generation in previous versions)
- --model-gen=2 or -m -m:
generate model for all created expressions
+ fixed several rewriting bugs
+ refactored a lot of code
+ new output format for models
* Optimizations:
+ re-enabled and fixed unconstrained optimization
+ don't care reasoning on bit vector skeleton
- dual propagation optimization
- justification optimization
* API changes:
+ API functions return node of type BoolectorNode instead of BtorNode
+ new option handling
+ can be set via environment variables
+ set options via boolector_set_opt
+ new options
- for a complete list of options please refer to the documentation of
boolector_set_opt
+ deprecated functions:
- boolector_get_symbol_of_var
-> use boolector_get_symbol (...)
the following functions are obsolete with boolector_set_opt
- boolector_enable_model_gen
-> use boolector_set_opt ("model_gen", 1)
- boolector_generate_model_for_all_reads
-> use boolector_set_opt ("model_gen", 2)
- boolector_enable_inc_usage
-> use boolector_set_opt ("incremental", 1)
- boolector_set_rewrite_level
-> use boolector_set_opt ("rewrite_level", ...)
- boolector_set_verbosity
-> use boolector_set_opt ("verbosity", ...)
- boolector_set_loglevel
-> use boolector_set_opt ("loglevel", ...)
+ new API functions to create uninterpreted functions
- boolector_uf
- boolector_bool_sort
- boolector_bitvec_sort
- boolector_fun_sort
+ limited boolector_sat calls
- set lemmas on demand limit
- set conflict limit for SAT solver
* Notes:
+ If uninterpreted functions occur in the formula it is not possible to
dump the formula to BTOR 1.2 format (this will be fixed with BTOR 2.0).
news for release 1.6.0 since 1.5.119
--------------------------------------------------------------------------------
* extensionality support disabled
* support for macros and lambdas
* model based testing 'btormbt'
* API tracing and untracing with 'btoruntrace'
* improved quality of SMT2 parse error messages
* added missing semantic checks in SMT2 parser
news for release 1.5.119 since 1.5.118
--------------------------------------------------------------------------------
* fixed '{boolector,btor}_set_sat_solver
(if MiniSAT and/or PicoSAT are not not enabled at compile time)
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