z3
Z3 is a Satisfiability Modulo Theories (SMT) solver and integrates several decision procedures: Linear real and integer arithmetic, fixed-size bit vectors, uninterpreted functions, extensional arrays, quantifiers and model generation.
- Devel package for openSUSE:Factory
-
1
derived packages
- Links to openSUSE:Factory / z3
- Download package
-
Checkout Package
osc -A https://api.opensuse.org checkout devel:tools:statica/z3 && cd $_ - Create Badge
Refresh
Refresh
Source Files
| Filename | Size | Changed |
|---|---|---|
| _link | 0000000124 124 Bytes | |
| z3-4.11.0.tar.gz | 0005392300 5.14 MB | |
| z3.changes | 0000065125 63.6 KB | |
| z3.spec | 0000003166 3.09 KB |
Revision 88 (latest revision is 101)
Jiri Slaby (jirislaby)
accepted
request 999657
from
Matthias Eliasson (elimat)
(revision 88)
- update to 4.11.0:
* remove Z3_bool, Z3_TRUE, Z3_FALSE from the API. Use bool, true, false instead.
* z3++.h no longer includes <sstream> as it did not use it.
* add solver.axioms2files
- prints negated theory axioms to files. Each file should be unsat
* add solver.lemmas2console
- prints lemmas to the console.
* remove option smt.arith.dump_lemmas. It is replaced by solver.axioms2files
* add option smt.bv.reduce_size.
- it allows to apply incremental pre-processing of bit-vectors by identifying ranges that are known to be constant.
This rewrite is beneficial, for instance, when bit-vectors are constrained to have many high-level bits set to 0.
* add feature to model-based projection for arithmetic to handle integer division.
* add fromString method to JavaScript solver object.
Comments 0