mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity
4950 commits 23 branches 48 tags 157 MiB
Commit graph

4950 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner aec5a38b14 fix memory leak in SAT solver exposed by regression tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-06 11:44:55 -08:00
George Karpenkov f93c41b1be Since classes are non-final "instanceof" check is better in #equals 2016-01-06 11:27:58 +01:00
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