mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity
7715 commits 23 branches 48 tags 157 MiB
Commit graph

7715 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
81ec5bae95 fix #1377 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-27 11:02:48 -08:00
Nikolaj Bjorner
36e5d4dec9 fix #1377 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-27 11:01:44 -08:00
Nikolaj Bjorner
2b3ee995ff fix #1375 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-27 09:03:52 -08:00
Nikolaj Bjorner
bfe6260c58 fix #1376 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-27 08:39:20 -08:00
Nikolaj Bjorner
4520fafa8c fix #1368 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-26 19:13:35 -08:00
Nikolaj Bjorner
7d693a5f9f fix different bug reported on #1366 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-25 20:01:14 -08:00
Nikolaj Bjorner
841c48e04d fix break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-25 18:24:45 -08:00
Nikolaj Bjorner
77b74ddb88 fix #1366 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-25 17:55:20 -08:00
Nikolaj Bjorner
1c5f798cbe expose extra symbols for logic ALL, requested in #1364 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-25 12:03:47 -08:00
Nikolaj Bjorner
441c0de3c8 Merge branch 'master' of https://github.com/z3prover/z3 2017-11-23 11:17:58 -08:00
Nikolaj Bjorner
357b4b20fd fix #1365. Filter MBQI instantiations for as-array terms that lead the array theory to return unknown and therefore block further instantiations. as-array terms are at this point almost always created from internal model values so quantifier instantiations with these have little value, other than instantiations of other paraameters that may indepdendently help 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-23 11:17:41 -08:00
Nikolaj Bjorner
56cc0a9018 remove redundant argument #1364 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-21 15:47:27 -08:00
Nikolaj Bjorner
2597ac6756 fix argument validation to new overflow/underflow functions #1364 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-21 15:44:15 -08:00
Nikolaj Bjorner
18200f55ed add bit-vector over/underflow checks to Python API, #1364 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-21 15:14:49 -08:00
Nikolaj Bjorner
d520557ad9 fix #1233 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-21 11:52:15 -08:00
Nikolaj Bjorner
c5f231acdf debugging #1233 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-21 08:16:41 -08:00
Nikolaj Bjorner
33e8113c9e adding instrumentation to debug #1233 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-20 16:51:17 -08:00
Nikolaj Bjorner
14714f2803 Merge branch 'master' of https://github.com/z3prover/z3 2017-11-19 20:42:11 -08:00
Nikolaj Bjorner
620bd81269 avoid rationals for addition in checked_int64 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-19 20:41:42 -08:00
Christoph M. Wintersteiger
0194df611c Merge branch 'master' of https://github.com/Z3Prover/z3 2017-11-17 21:15:36 +00:00
Christoph M. Wintersteiger
f5ff9fae34 Fixed bug check in bv2fpa converter. Fixes #1291. 2017-11-17 21:15:30 +00:00
Nikolaj Bjorner
d380db8068
Merge pull request #1360 from levnach/dev 
avoid a warning
 2017-11-16 13:48:28 -08:00
Lev Nachmanson
62cf6aace7 avoid a warning 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2017-11-16 10:20:21 -08:00
Nikolaj Bjorner
a68d5131c7 add bvsmod 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-16 09:00:14 -08:00
Nikolaj Bjorner
2be466f51e Merge branch 'master' of https://github.com/z3prover/z3 2017-11-16 08:55:51 -08:00
Nikolaj Bjorner
2efcd5b789 additional bit-vector operators over C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-16 08:55:40 -08:00
Nikolaj Bjorner
07031798ec fix occurs function used in qe_lite #1241 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-16 01:43:35 -08:00
Nikolaj Bjorner
2e6ae8cfd2 fix crash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 23:06:05 -08:00
Nikolaj Bjorner
c3364f17fa fix infinite loop in traversing equivalence class, #1274, still requires addressing MBQI 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 21:19:22 -08:00
Nikolaj Bjorner
c3f67f3b5f fix infinite loop in traversing equivalence class, #1274, still requires addressing MBQI 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 21:17:00 -08:00
Nikolaj Bjorner
f47671931f Merge branch 'master' of https://github.com/z3prover/z3 2017-11-15 20:32:45 -08:00
Nikolaj Bjorner
58be777307 fix #1358 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 20:32:37 -08:00
Nikolaj Bjorner
63eeb40081 Merge branch 'master' of https://github.com/z3prover/z3 2017-11-15 16:39:13 -08:00
Nikolaj Bjorner
cde41cf16c fix slicer for unsoundness. #1304 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 16:39:09 -08:00
Nikolaj Bjorner
61d149a724 fix java build problem with bool arrays 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 16:18:18 -08:00
Nikolaj Bjorner
7f13cf13f2 clean up bv_numeral code and fix bug in how they are initialized 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 15:00:11 -08:00
Nikolaj Bjorner
795e0c641a add method to create bit-vectors directly from an array of Booleans 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 14:44:59 -08:00
Nikolaj Bjorner
2c97eb1393 include information whether rule is reachable in del_rule model converter for simpler model presentation #1241 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 11:46:28 -08:00
Nikolaj Bjorner
2cab1cccc9 Merge branch 'master' of https://github.com/z3prover/z3 2017-11-15 09:12:23 -08:00
Nikolaj Bjorner
100d9e3edb insert total relations in model converter. #1241 2017-11-15 09:12:10 -08:00
Nikolaj Bjorner
2d0d9d462d Merge branch 'master' of https://github.com/z3prover/z3 2017-11-15 09:10:23 -08:00
Nikolaj Bjorner
116094022f insert total relations in model converter. #1291 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 09:10:15 -08:00
Nikolaj Bjorner
9ef54d7a16
Merge pull request #1355 from delcypher/cmake_api_doc_pass_build 
[CMake] When invoking `mk_api_doc.py` pass the build directory.
 2017-11-13 19:56:09 -08:00
Dan Liew
1a0bff7480 [CMake] When invoking mk_api_doc.py pass the build directory. 
This change was requested by @wintersteiger as an alternative way
to unbreak the TravisCI builds.
 2017-11-13 22:31:05 +00:00
Nikolaj Bjorner
195d81ebef fix rewriter loop reported in #1354 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-13 13:49:03 -08:00
Nikolaj Bjorner
dbb35b951c make .NET and Java bindings for optimization use Expr instead of ArithExpr to accomodate bit-vector optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-13 08:51:16 -08:00
Christoph M. Wintersteiger
7c63a5cc1d Fixed MSYS/MinGW build. Fixes #1335. 2017-11-11 16:38:53 +00:00
Christoph M. Wintersteiger
45975bec65 Improved support for MSYS/MINGW. Fixes #969. 2017-11-11 15:11:54 +00:00
Christoph M. Wintersteiger
d44d918414 API doc build fix. Related to #1350. 2017-11-11 14:19:38 +00:00
Christoph M. Wintersteiger
a173b0faf7 Fixed API doc build 2017-11-09 13:34:32 +00:00