forked from agra-uni-bremen/metaSMT
-
Notifications
You must be signed in to change notification settings - Fork 1
/
ChangeLog
35 lines (26 loc) · 1009 Bytes
/
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
ChangeLog
===========
metaSMT 2 -> 3
----------------
* Better integration with CMake find_package
* Extended API support
* SymbolTable: Custom names for variables (SMT2 output)
* AssignRandomBits: select a random subset of bits from BitVector
variables and assign a random value
* SAT API (add_clause): directly add clauses to the backend
* Type Descriptors and TypedSymbols (Boolean, BitVector)
* Preliminary support for QF_UF (only unary functions)
* Portfolio and Priority Multi-Threaded solving
* toolbox example N-Queens using cardinality constraints
* toolbox contains a CNF solver
metaSMT 1 -> 2
----------------
Bugfixes:
* Fixed 2 bug in BitBlast constant handling (wrong bit order, overflow)
* Fixed memory leak in Boolector backend
* Disabled Copy Constructor of DirectSolver
Other changes:
* further work on the FMI frontend
* Refactored assertion, assumption to use "command"-API, moved to separate
headers
* fixes and enhancements to the build system and bootstrap script