3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-17 09:56:39 +00:00
Commit graph

31 commits

Author SHA1 Message Date
Nuno Lopes
737c2208fa delete more default constructors
reduces code size by 0.1%
2024-09-23 12:59:04 +01:00
Nikolaj Bjorner
7f149a36d7 refining model update rules for del_rule #5865 #5866 2022-02-25 08:03:46 -08:00
Nikolaj Bjorner
6be0a66b38 fix #5863 2022-02-22 13:00:20 -08:00
Nikolaj Bjorner
4a6083836a call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
Nikolaj Bjorner
397bf2dec6 move windows dependencies down 2020-04-30 19:31:11 -07:00
Nikolaj Bjorner
4651bffafc fix #3831
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-09 17:45:05 -07:00
Nikolaj Bjorner
9c6722bea8 fix #3791
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-06 18:37:39 -07:00
Nikolaj Bjorner
520ce9a5ee integrate lambda expressions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-26 07:23:04 -07:00
Nikolaj Bjorner
f525f43e43 merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-30 09:30:43 -07:00
Nikolaj Bjorner
b5f067bec5 fix #1592 #1587
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-25 11:18:24 +02:00
Nikolaj Bjorner
97cee7d0a4 fix #1576, hopefully
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-18 07:30:26 -07:00
Nikolaj Bjorner
098bce0f46 fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-14 08:44:20 -07:00
Nikolaj Bjorner
d939c05e72 fix build warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-14 08:27:40 -07:00
Bruce Mitchener
2fa304d8de Remove int64, uint64 typedefs in favor of int64_t / uint64_t. 2018-03-31 14:45:04 +07:00
Nikolaj Bjorner
c513f3ca09 merge with master
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-25 14:57:01 -07:00
Nikolaj Bjorner
718e5a9b6c add unit extraction
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-06 01:08:17 -08:00
Bruce Mitchener
76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Bruce Mitchener
7167fda1dc Use override rather than virtual. 2018-02-10 09:56:33 +07:00
Nikolaj Bjorner
2853558bc2
Merge pull request #1466 from waywardmonkeys/reduce-copying
Use const refs to reduce copying.
2018-02-05 16:37:44 -08:00
Bruce Mitchener
6d6b614924 Use char version of rfind.
There is only a single character involved, so use the char version.

This was found via `clang-tidy`.
2018-01-30 21:45:12 +07:00
Bruce Mitchener
177414c0ee Use const refs to reduce copying.
These are things that have been found by `clang-tidy`.
2018-01-30 21:43:56 +07:00
Nikolaj Bjorner
4bbece6616 re-organize proof and model converters to be associated with goals instead of external
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-11-18 16:33:54 -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
3de8c193ea implementing model updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-30 16:11:51 -05:00
Nikolaj Bjorner
b19f94ae5b make include paths uniformly use path relative to src. #534
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-31 13:24:11 -07:00
Matthias Schlaipfer
c82319b358 Refactor count_vars and count_rule_vars
ast_manager m was not used
2015-05-14 17:04:38 +01:00
Nikolaj Bjorner
c09903288f have free variable utility use a class for more efficient re-use
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-15 16:14:22 -07:00
Nikolaj Bjorner
d6de73a2d1 fix model converter in inliner. Bug reported by Sagar Chaki
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-07-06 18:11:57 +02:00
Nikolaj Bjorner
1496333e5b fix mint64 build errors
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-09-09 09:22:45 -07:00
Nikolaj Bjorner
716663b04a avoid creating full tables when negated variables are unitary, add lazy table infrastructure, fix coi_filter for relations, reduce dependencies on fixedpoing_parameters.hpp header file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-09-08 05:52:18 -07:00
Nikolaj Bjorner
e4338f085b re-organization of muz
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-08-28 22:11:33 -07:00
Renamed from src/muz/dl_util.cpp (Browse further)