mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity
5469 commits 23 branches 48 tags 157 MiB
Commit graph

5469 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger e3a41d0d98 Merge pull request #645 from martin-neuhaeusser/cross-mingw64 
Extend build scripts to support MinGW64 cross-compilation on Windows.
 2016-06-24 13:42:10 +01:00
Christoph M. Wintersteiger d90a575981 Merge pull request #646 from martin-neuhaeusser/ocaml-c89 
Make C-layer of OCaml bindings C89 compatible.
 2016-06-24 13:40:50 +01:00
Martin R. Neuhäußer 5845e63396 Make cmake not emit -fPIC to mingw64 for Windows builds. 
This patch detects a mingw64 build of the shared library and does not emit -fPIC to the compiler.
This is necessary to avoid a warning message, as Windows native code DLLs are generally relocatable
and not position independent.
 2016-06-24 12:40:16 +02:00
Nikolaj Bjorner 98a34ca51f Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-23 21:39:34 -07:00
Nikolaj Bjorner c72ed3e6b4 update core minimization code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-23 21:39:28 -07:00
Christoph M. Wintersteiger 0a575936d0 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-23 19:31:08 +01:00
Christoph M. Wintersteiger 8bde7b8a4c Added facilities for dumping smt_params for debugging purposes 2016-06-23 19:31:00 +01:00
Nikolaj Bjorner 41edf5f91e Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-22 20:25:55 -07:00
Nikolaj Bjorner 5b497b6249 reduce set of mainly verbose warnings raised by -Wmaybe-uninitialized and unused variable warnings from release mode builds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-22 20:25:47 -07:00
Christoph M. Wintersteiger fad1dffbf0 Added PATH info to successful build message 2016-06-22 19:03:42 +01:00
Christoph M. Wintersteiger 89b1d7d8da Fixed test case 2016-06-22 18:52:40 +01:00
Christoph M. Wintersteiger 8c191781e7 Fixed warning message 2016-06-22 18:52:30 +01:00
Nikolaj Bjorner fa6f9b4a37 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-20 16:39:08 -07:00
Nikolaj Bjorner 9c099d6b1b fix mb maximization logic, so far not accessible 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-20 16:39:03 -07:00
Nikolaj Bjorner bfe26390f0 fix bug introduced when hiding unused variables in 96e157e, reported by Mikolas Janota 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-14 08:12:32 -07:00
Nikolaj Bjorner 8da0146318 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-14 08:10:21 -07:00
Nikolaj Bjorner 9253ca9d86 make use of warning_msg safe for formatting. Thanks to Scott McPeak for reporting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-14 08:10:10 -07:00
Christoph M. Wintersteiger c8c262fb93 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-14 13:14:30 +01:00
Christoph M. Wintersteiger 3ea71b4b25 Fixed SMT2 scanner to allow 0xFF characters. 
Thanks to Santiago Zanella-Beguelin for reporting this issue.
 2016-06-14 12:49:48 +01:00
Nikolaj Bjorner b11f9050e3 fix bugs exposed from bad indentation warnings, #650 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-13 18:20:25 -07:00
Nikolaj Bjorner 16ad33bf39 add collection of statistics #652 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-13 18:17:49 -07:00
Nikolaj Bjorner c7ff05cc78 enable core minimization with qsat in case it turns out to be useful 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-12 15:58:12 -07: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