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

3449 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nuno Lopes
c2ef566ddc Merge pull request #81 from ahorn/opt 
Fix g++ compile-time error
 2015-05-12 10:44:28 +01:00
U-EUROPE\t-alexh
b882a94f6a Fix g++ compile-time error 
Signed-off-by: U-EUROPE\t-alexh <t-alexh@microsoft.com>
 2015-05-12 10:23:25 +01:00
Nikolaj Bjorner
4d3d9f7602 include compression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-11 20:32:39 -07:00
Nikolaj Bjorner
c96c4c7af7 Merge branch 'opt' of https://github.com/Z3Prover/z3 into opt 2015-05-11 17:12:04 -07:00
Nikolaj Bjorner
bf6ab3fc03 local state 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-11 17:11:52 -07:00
Nikolaj Bjorner
e53462c1c1 update ddnf experiment code 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-11 17:11:21 -07:00
Nikolaj Bjorner
2e627e78bc filter tactic on proofs and cores 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-10 14:55:28 -07:00
Nikolaj Bjorner
1a4e8f89bd fix release build failure 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-10 14:53:05 -07:00
Nikolaj Bjorner
5063a2cdb6 add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-10 11:53:36 -07:00
Nikolaj Bjorner
6163085ff8 add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-10 10:02:44 -07:00
Nikolaj Bjorner
f5c048775b add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-10 09:42:11 -07:00
Nikolaj Bjorner
c807ad0927 add ddnf tests, add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-09 21:28:26 -07:00
Nikolaj Bjorner
e5716501e8 add ddnf tests, add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-09 19:47:00 -07:00
Nikolaj Bjorner
839e3fbb7c add ddnf tests, add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-09 19:40:34 -07:00
Nikolaj Bjorner
9377779e58 merge with unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-30 10:40:03 -07:00
Nikolaj Bjorner
a0f0b53686 fixes to #52, #53 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-28 14:48:59 -07:00
Christoph M. Wintersteiger
1abeb825a3 Fixed python 3.x problems. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-04-28 14:58:58 +01:00
Nikolaj Bjorner
620c11932b type check distinct operator. fixes #62 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-27 11:10:37 -07:00
Nuno Lopes
f7d9438e7b add failing test for issue #62 (mk_distinct doesnt type check) 
Signed-off-by: Nuno Lopes <nlopes@MSRC-3617536.europe.corp.microsoft.com>
 2015-04-27 17:44:38 +01:00
Christoph M. Wintersteiger
abe73db702 FP: bugfix for get_some_value which couldn't produce rounding-mode values. 2015-04-25 15:19:48 +01:00
Christoph M. Wintersteiger
4768a360f8 FP: Fix for conversion functions from non-FP 0 to +0.0 even when the rounding mode is ToNegative. 2015-04-25 15:01:20 +01:00
Christoph M. Wintersteiger
b58d3f4335 Bugfix for MPF unpacking 2015-04-25 14:26:18 +01:00
Christoph M. Wintersteiger
8c3fc574d1 comments fix 2015-04-24 15:37:45 +01:00
Nikolaj Bjorner
ffc3a36dcb checked ite-expressions as shared for bounds detection 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-23 19:59:33 +02:00
Ken McMillan
9bff93279f merging into unstable 2015-04-20 12:31:16 -07:00
Ken McMillan
5f37b1d32f fixed interp api bug (github issue #47) 2015-04-20 12:30:15 -07:00
Nikolaj Bjorner
6c1a5390ef fix big-int bug for shift amounts, github issue 44, reported by Dejan 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-20 10:20:06 +02:00
Nikolaj Bjorner
7d88d04514 fix crash reported by Jojanovich, github issue 45' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-20 00:55:30 +02:00
Christoph M. Wintersteiger
7e6ab736c0 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-04-17 16:10:13 +01:00
Christoph M. Wintersteiger
f1a1267d4c Added missing notes on fpToIEEEBV in Python. 2015-04-17 16:08:53 +01:00
Ken McMillan
af444beb2e re-indenting interp and duality 2015-04-15 12:22:50 -07:00
Christoph M. Wintersteiger
e1303e1eab Python API: Fixed expression types for floating point conversion functions. 
Partially fixes #39
 2015-04-15 12:07:53 +01:00
Nikolaj Bjorner
80a13977fc fix race condition from cancellation exposed by build regression tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-15 05:44:10 +01:00
Christoph M. Wintersteiger
a5036769b3 ML API doc fix 2015-04-13 17:46:18 +01:00
Christoph M. Wintersteiger
2948e47240 Java API doc fix 2015-04-13 17:43:29 +01:00
Christoph M. Wintersteiger
bf00723d37 Updated links in the documentation 2015-04-13 17:37:58 +01:00
Christoph M. Wintersteiger
f993d3df15 Documentation generator bugfixes and updates. 2015-04-13 17:33:26 +01:00
Nikolaj Bjorner
3ba2e712b2 merge with unstable branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-12 15:54:52 -07:00
Christoph M. Wintersteiger
dd0d0a9075 Merge branch 'unstable' of https://github.com/wintersteiger/z3 into unstable 2015-04-09 14:53:00 +01:00
Christoph M. Wintersteiger
8862cb4833 Java example: Removed throws declarations for Z3Exception. 2015-04-09 14:52:50 +01:00
Christoph M. Wintersteiger
3cd018bd6c Java API: Removed throws declarations for Z3Exception. 2015-04-09 14:46:59 +01:00
Christoph M. Wintersteiger
b7bb53406f Turned Z3Exception into a RuntimeException such that throws declarations are not needed anymore. Thanks to codeplex user steimann for this suggestion. 2015-04-08 13:16:32 +01:00
Christoph M. Wintersteiger
2f4c923216 Bugfix; InterpolationContext deleted Z3_config objects (inconsistent with non-Interpolation mk_context). 
Fixes #25
 2015-04-08 13:09:27 +01:00
Christoph M. Wintersteiger
03020b9f96 Build system bugfixes. 
Partially fixes #27
 2015-04-08 12:09:14 +01:00
Christoph M. Wintersteiger
ba066ff899 Bugfix for build scripts. 
Partially fixes #27
 2015-04-08 11:54:25 +01:00
Christoph M. Wintersteiger
0e8d314a2a Fixed Java API installation targets. Fixes #28 2015-04-08 11:02:56 +01:00
Christoph M. Wintersteiger
d7e6ca763f Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-04-07 13:49:07 +01:00
Christoph M. Wintersteiger
0ad97022a1 Added (un)install targets for the Java API 2015-04-07 13:48:34 +01:00
Christoph M. Wintersteiger
4a3abbfe0f Added (un)install targets for the Java API 2015-04-07 13:47:34 +01:00
Nikolaj Bjorner
841c1c2290 scope precedence of ||, github issue 24 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-03 12:06:31 -07:00