mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
7845 commits 49 branches 53 tags 182 MiB
Commit graph

7845 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
a83af22841 include special functionality in parsers for solvers and opt for additional file formats 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-03 20:00:45 +01:00
Nikolaj Bjorner
5ee30a3cd9 include special functionality in parsers for solvers and opt for additional file formats 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-03 20:00:24 +01:00
Nikolaj Bjorner
187998ae4d
Merge pull request #1381 from NikolajBjorner/smt2 
remove smtlib1 dependencies
 2017-12-02 10:24:02 -08:00
Nikolaj Bjorner
0bfea99cff fix issues found in parsing examples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 14:43:52 -08:00
Nikolaj Bjorner
274279b251 Merge branch 'smt2' of https://github.com/nikolajbjorner/z3 into smt2 2017-12-01 09:00:01 -08:00
Nikolaj Bjorner
a9ebda105c remove assertion that gets violated on exception path (declaration of datatypes are not getting removed) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 08:59:36 -08:00
Nikolaj Bjorner
8357210d3c fix lack of warning/error for unbounded objectives in context of quantifiers #1382 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 01:07:41 -08:00
Nikolaj Bjorner
c31ad14747 fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 00:52:32 -08:00
Nikolaj Bjorner
4bb0e9b633 fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 00:52:06 -08:00
Nikolaj Bjorner
b96dacfff2 set version, fix build of test files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-30 08:42:01 -08:00
Nikolaj Bjorner
c18d60a9c5 fix java 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-29 20:56:36 -08:00
Nikolaj Bjorner
ab58723ffc fix dotnet example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-29 20:52:19 -08:00
Nikolaj Bjorner
9f567a6215 fix example file to be smt2 format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-29 19:38:47 -08:00
Murphy Berzish
b581ab70ed Merge remote-tracking branch 'upstream/master' into develop 2017-11-29 17:10:53 -05:00
Nikolaj Bjorner
0a67f6ee9b fix maxsat compilation for maxsat example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-29 09:00:37 -08:00
Nikolaj Bjorner
09dc773658 fix maxsat compilation for maxsat example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-29 08:50:35 -08:00
Nikolaj Bjorner
2749e547cf fix c example, remove more smtlib1 printing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 18:14:24 -08:00
Nikolaj Bjorner
b8e5fc9f43 remove SMTLIB1 printing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 15:08:28 -08:00
Nikolaj Bjorner
d1ee5431a7 Update version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 14:19:30 -08:00
Nikolaj Bjorner
eeee77889b add parser error 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 11:58:58 -08:00
Nikolaj Bjorner
161b6a9983 increase minor version, update java/.net apis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 11:51:37 -08:00
Nikolaj Bjorner
92b4b9e7a7 fix error messaging for parsers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 11:14:00 -08:00
Nikolaj Bjorner
89971e2a98 remove smtlib1 dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 10:37:30 -08:00
Nikolaj Bjorner
d7042c234f fix #1371 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 09:34:44 -08:00
Nikolaj Bjorner
5a35d00766 remove std::cout 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 08:55:45 -08:00
Nikolaj Bjorner
103ce78c29 save model from level 0, fix #1380 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 08:53:06 -08:00
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