mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
6151 commits 49 branches 53 tags 182 MiB
Commit graph

6151 commits

This branch
This branch
All branches
Author SHA1 Message Date
George Karpenkov
2a347f04bf Java API: FuncInterp.Entry should be an inner static class 
...as it does not use any fields of the outer FuncInterp object.
 2016-06-12 21:00:51 +02:00
George Karpenkov
5657399d55 Bugfix for incorrect order of operations. 2016-06-12 20:39:54 +02:00
George Karpenkov
495ef0f055 Java bindings with no finalizers 
Replacing finalizers with PhantomReferences, required quite a lot of
changes to the codebase.
 2016-06-12 20:27:01 +02:00
George Karpenkov
dfc80d3b69 Do not needlessly catch exceptions in Java bindings 
A lot of existing code in Java bindings catches exceptions just to
silence them later.

This is:
a) Unnecessary: it is OK for a function to throw a RuntimeException
without declaring it.
b) Highly unidiomatic and not recommended by Java experts (see Effective
Java and others)
c) Confusing as has the potential to hide the existing bugs and have
them resurface at the most inconvenient/unexpected moment.
 2016-06-12 14:14:11 +02:00
Nikolaj Bjorner
3ac4709992 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-11 10:39:31 -07:00
Nikolaj Bjorner
ea201a776d enable qsat-opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-11 10:39:27 -07:00
Nikolaj Bjorner
9f5a117443 move mus to solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-10 16:24:14 -07:00
martin-neuhaeusser
f069b1c0e9 Make C-layer of OCaml bindings C89 compatible. 
This patch ensures that the C code generated for the OCaml stubs complies with C89. It is needed to compile Z3 with OCaml support with Visual Studio versions older than VS2013.
 2016-06-10 16:49:06 +02:00
Martin R. Neuhäußer
22097efd4a Extend build scripts to support MinGW64 cross-compilation on Windows. 2016-06-10 16:43:57 +02:00
Nikolaj Bjorner
19f98547f7 fix memory leak Issue #643 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-09 21:59:10 -07:00
Christoph M. Wintersteiger
bd187e0989 Bugfix for fp.min/fp.max in fpa2bv converter; hide BV UFs from FP models. 
Fixes #642
 2016-06-09 17:51:31 +01:00
Christoph M. Wintersteiger
bfeab9cc15 Added facilities for hiding UFs in smt::model_generator 2016-06-09 17:49:45 +01:00
Christoph M. Wintersteiger
879363157f Bugfix for fpa2bv_converter 2016-06-09 12:09:53 +01:00
Nikolaj Bjorner
cb29c07f06 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-08 13:56:12 -07:00
Nikolaj Bjorner
5253f3a12b internalize unsupported operations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-08 13:56:01 -07:00
Christoph M. Wintersteiger
9b91e6ff0a Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-08 12:07:19 +01:00
Christoph M. Wintersteiger
a2eb824590 Added __nonzero__ and __bool__ functions to Python Z3 ASTs to enable use of Python lists (and similar). 
Thanks to Vlad Shcherbina for the recommendation (see http://stackoverflow.com/questions/37669576/converting-z3-cnf-formula-into-list-of-lists-representation-using-z3py/37679447?noredirect=1#comment62859886_37679447)!
 2016-06-08 12:07:13 +01:00
Nikolaj Bjorner
314eae50a4 Merge pull request #641 from kanigsson/master 
Take into account number of monomials for rlimit counting
 2016-06-07 19:27:06 -07:00
Johannes Kanig
9bfa73ee06 Take into account number of monomials for rlimit counting 
Should fix issue #611
 2016-06-08 11:17:26 +09:00
Nikolaj Bjorner
47f97dde89 Merge pull request #639 from MikolasJanota/master 
Adding translation to ackr_model_converter.
 2016-06-06 10:09:21 -07:00
Mikolas Janota
9df2a183d6 Adding translation to ackr_model_converter. 2016-06-06 18:06:45 +01:00
Nikolaj Bjorner
736f2bef46 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-04 20:08:26 -07:00
Nikolaj Bjorner
e8d85f91d7 disable filtering on negated tails. Issue #634 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-04 20:08:13 -07:00
Christoph M. Wintersteiger
f2a869fb58 std::unordered_map -> std::map 2016-06-04 11:01:46 +01:00
Christoph M. Wintersteiger
626b9160bf collect-statistics additions 2016-06-03 20:45:42 +01:00
Christoph M. Wintersteiger
b54ef3623b added collect-statistics tactic 2016-06-03 20:26:05 +01:00
Nikolaj Bjorner
19db0c5f2c Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-03 10:13:27 -07:00
Nikolaj Bjorner
219b47822b avoid qsat when formulas are quantifier-free. Go directly to SMT 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-03 10:13:16 -07:00
Christoph M. Wintersteiger
a94aff23e6 Added clearer FP conversion functions to the Python API. 
Implements #476
 2016-06-03 13:23:12 +01:00
Nikolaj Bjorner
e9e926d4d6 UINT32_MAX -> UINT_MAX 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-02 21:00:18 -07:00
Nikolaj Bjorner
21158ea03f Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-02 20:58:20 -07:00
Nikolaj Bjorner
eab5a84f62 fix issues with int.to.str and seq.len encodings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-02 20:57:52 -07:00
Christoph M. Wintersteiger
83ad5d65e4 Replaced fp.rem conversion to bit-vectors with an SMT-compliant one. 
Fixes #561
 2016-06-02 20:22:02 +01:00
Christoph M. Wintersteiger
b3b5c6226b MPF code simplification 2016-06-02 17:12:24 +01:00
Christoph M. Wintersteiger
ade2dbe15a Cache cleanup fix for bv_simplifier_plugin. 
Fixes #615
 2016-05-31 16:47:14 +01:00
Christoph M. Wintersteiger
47e75827ee theory_fpa refactoring 2016-05-31 16:22:48 +01:00
Christoph M. Wintersteiger
302c491535 theory_fpa refactoring 2016-05-31 16:22:24 +01:00
Christoph M. Wintersteiger
03f6b465b9 comment typos 2016-05-31 16:14:50 +01:00
Nikolaj Bjorner
39acd3594a test variants for seq_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-30 18:15:10 -07:00
Nikolaj Bjorner
f03032bd09 updated seq solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-29 14:01:05 -07:00
Nikolaj Bjorner
cddf8091b5 strengthen support for int.to.str and length reasoning. Issue #589 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-28 12:36:50 -07:00
Nikolaj Bjorner
c3f498a640 strengthen support for int.to.str and length reasoning. Issue #589 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-28 12:26:47 -07:00
Nikolaj Bjorner
8c99d3c431 tidy unbound compressor code, add invariant checks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-28 11:05:26 -07:00
Nikolaj Bjorner
3aea63edb1 check for cancellation before internalizing and during to avoid errors. Issue #625 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-27 17:27:37 -07:00
Nikolaj Bjorner
236f1c2a3e bypass stale rules as part of unbounded compression. Issue #624 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-27 10:31:28 -07:00
Nikolaj Bjorner
18a9b89e30 bypass stale rules as part of unbounded compression. Issue #624 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-27 09:38:23 -07:00
Nikolaj Bjorner
50d334e4e9 fix non-determinism bug in simple joins. Keys were normalized based on pointer equality not object identifier equality. Also some ptr hashtables were used with pointer hashes, and then traversed. reported in issue #619 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-27 07:51:02 -07:00
Nikolaj Bjorner
cfffb0b3c5 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-27 07:49:45 -07:00
Nikolaj Bjorner
84ff6fd62a fix non-determinism bug in simple joins. Keys were normalized based on pointer equality not object identifier equality. Also some ptr hashtables were used with pointer hashes, and then traversed 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-27 07:49:38 -07:00
Christoph M. Wintersteiger
18340b0e95 fix for pb2bv_model_converter 2016-05-26 18:42:57 +01:00