mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-27 09:49:23 +00:00
Code Activity
4586 commits 45 branches 52 tags 177 MiB
Commit graph

4586 commits

This branch
This branch
All branches
Author SHA1 Message Date
George Karpenkov
529b9d6833 The locking field should be final. 2016-01-06 11:19:38 +01:00
George Karpenkov
8bb0010dc3 Javadoc and indentation fixes 
- A proper way to refer to the function in the same class is "#funcName"

- There is no point in "@param p" declaration if no description follows
it.
 2016-01-06 11:19:26 +01:00
George Karpenkov
54e5bf2422 Remove redundant cast 2016-01-06 11:18:22 +01:00
George Karpenkov
93ad8d32b9 Remove redundant "throw" statement which has no effect. 2016-01-06 11:17:32 +01:00
George Karpenkov
d0d7a5b712 Consistent Sort#equals 2016-01-06 11:16:45 +01:00
George Karpenkov
a816b4895c Logic simplifications 
There is no point in writing "boolean ? true : false" instead of
"boolean"
 2016-01-06 11:16:30 +01:00
George Karpenkov
52fdf73178 IDisposable is effectively an abstract class. 2016-01-06 11:15:11 +01:00
George Karpenkov
c435bc379b Added braces 
Lack of braces on multi-line statements is considered very scary in
Java.
 2016-01-06 11:14:53 +01:00
George Karpenkov
ccd88a63a5 No need to call "new String()" 2016-01-06 11:12:33 +01:00
George Karpenkov
27c684f743 AST#hashCode bugfix 
Previous implementation always returned zero.
I can only assume that it wanted to cache it as well,
but I haven't implemented that to keep the changes light.
 2016-01-06 11:11:01 +01:00
George Karpenkov
4d3675cb4e Consistent #equals() implementation 
Also dropped #hashCode(), as it just calls the parent class
implementation.
 2016-01-06 11:10:03 +01:00
George Karpenkov
1dcaddbec7 Adding @Override declarations 
They are important, as they prevent miss-spelling the parent method  and
/or arguments name.
 2016-01-06 11:07:48 +01:00
George Karpenkov
a3a8ba40e7 "static final" does not do anything 2016-01-06 10:25:52 +01:00
George Karpenkov
56db1867ef Proper idiomatic isEquals implementation. 2016-01-06 10:24:00 +01:00
George Karpenkov
92bb984305 catch/throw is redundant. 2016-01-06 10:19:44 +01:00
Nikolaj Bjorner
da63ac809e Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-05 10:16:12 -08:00
Nikolaj Bjorner
fafdbfaf0e reset out_bits when blasting multiplication of bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-05 10:16:02 -08:00
Christoph M. Wintersteiger
8b8dc95986 Merge pull request #398 from wintersteiger/jan4 
Improvements for the FPA API.
 2016-01-05 18:08:05 +00:00
Nikolaj Bjorner
9dfcaaa01d reset out_bits when blasting multiplication of bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-05 10:07:44 -08:00
Christoph M. Wintersteiger
de3cb7e5dc More FPA exponent/siginficand order consistency 2016-01-05 18:05:21 +00:00
Christoph M. Wintersteiger
1610e4fbd0 Merge branch 'master' of https://github.com/Z3Prover/z3 into jan4 2016-01-05 17:45:35 +00:00
Nikolaj Bjorner
ee157e47e4 fix crash caused by recycling variable names. Stackoverflow segfault-in-bv-rewritermk-mul-eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-05 09:19:21 -08:00
Nikolaj Bjorner
65de39f403 disabling mk_const_case_multiplier until debugged 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-05 08:45:10 -08:00
Christoph M. Wintersteiger
d176c8714a Merge branch 'master' of https://github.com/Z3Prover/z3 into jan4 2016-01-05 16:38:12 +00:00
Nikolaj Bjorner
752a973e53 missing files? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-05 08:32:48 -08:00
Nikolaj Bjorner
b0d244c1e0 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-05 08:23:50 -08:00
Nikolaj Bjorner
af758dea4a tuning for seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-05 08:23:44 -08:00
Nuno Lopes
465d28e160 seq_decl: fix build with stricter compilers 
get rid of 32 rellocations as a nice side-effect
 2016-01-05 14:57:41 +00:00
Christoph M. Wintersteiger
b3a1aa27ee Merge branch 'master' of https://github.com/Z3Prover/z3 into jan4 2016-01-05 14:48:52 +00:00
Christoph M. Wintersteiger
13cbd19411 FPA Python API cleanup. 2016-01-05 14:48:42 +00:00
Christoph M. Wintersteiger
3e000d7525 build fix for libz3.vcxproj 2016-01-05 14:40:31 +00:00
Nuno Lopes
bc123dc79b fix build with c++98 compilers 2016-01-05 14:10:32 +00:00
Christoph M. Wintersteiger
097552768f Merged Python API changes. 2016-01-05 11:51:28 +00:00
Christoph M. Wintersteiger
bd8a5982ad Added new items to .NET project file 2016-01-05 11:37:34 +00:00
Christoph M. Wintersteiger
8b47a84598 Merge branch 'master' of https://github.com/Z3Prover/z3 into jan4 2016-01-05 11:34:35 +00:00
Christoph M. Wintersteiger
4c29d4d007 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-05 03:31:43 -08:00
Christoph M. Wintersteiger
a06f754683 tabs 2016-01-05 03:31:21 -08:00
Nikolaj Bjorner
a2fb4fc589 remove tabs, fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-04 22:49:28 -08:00
Nikolaj Bjorner
c008c2c274 fix indentation error 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-04 22:36:50 -08:00
Nikolaj Bjorner
b079ff1dae Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-04 22:35:08 -08:00
Nikolaj Bjorner
f6be76aec5 Merge pull request #396 from NikolajBjorner/master 
Basic Sequence/String and regular expression support, congruence propagation for bit-vectors, tuned bit-vector multiplier encodings for small numerals.
 2016-01-04 22:33:08 -08:00
Nikolaj Bjorner
55452e1680 Merge pull request #394 from kenmcmil/issue393 
issue #393 -- removed debugging assert
 2016-01-04 22:28:46 -08:00
Nikolaj Bjorner
3f040dbd23 remove std::cout usage 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-04 22:26:54 -08:00
Nikolaj Bjorner
2f9fda45c3 fix tabs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-04 22:14:45 -08:00
Nikolaj Bjorner
2c1d2aad44 seq, API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-04 22:06:32 -08:00
Nikolaj Bjorner
62e1c525c0 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-04 20:42:14 -08:00
Nikolaj Bjorner
fbee36d035 remove debug asserts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-04 20:42:07 -08:00
Nikolaj Bjorner
d7dcd022b9 seq, API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-04 18:49:21 -08:00
Nikolaj Bjorner
c1ebf6b4fc seq + API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-04 18:01:48 -08:00
Christoph M. Wintersteiger
4915f2da04 Added facilities for generating a libz3.vcxproj next to z3.vcxproj for simplified DLL build in VS. 2016-01-04 21:53:24 +00:00