mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-12 08:10:32 +00:00
Code Activity
20803 commits 63 branches 58 tags 225 MiB
Commit graph

74 commits

Author SHA1 Message Date
Nuno Lopes
bd993ca963 fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
9448f67d21 fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
1c5cbcbe92 fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
67ce05c1f5 fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
10f986ee1a fix 2026-02-17 09:50:48 +00:00
Nuno Lopes
8562788ad8 fixes 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
9bf691f8bd Refactor decompose function and consolidate value()/value64() into single value() returning int64_t 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
5edef9e9a0 Remove nonsensical assertion and revert to simpler shift for SMALL_INT constants 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
dcfeb559fe Add assertion to set() method and simplify get_sign_cell by removing redundant SMALL_INT_MIN case 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
4dc74e2e30 Fix undefined behavior in SMALL_INT_MAX/MIN constants by using unsigned arithmetic 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
b8ed45bfac Revert deallocation in set methods and restore indentation in gcd function 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:48 +00:00
copilot-swe-agent[bot]
6faaf86dca Implement proper bounds checking for small integers based on platform pointer size 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:47 +00:00
copilot-swe-agent[bot]
cb3b8603eb Fix syntax errors in mpz.h 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-17 09:50:47 +00:00
Nuno Lopes
ac1bef0053 mpz: use pointer tagging to save space (#8447) 
Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com>
 2026-02-17 09:50:47 +00:00
Nikolaj Bjorner
c269421942 Revert "mpz: use pointer tagging to save space (#8447)" 
This reverts commit 2f4abe2ce6.
 2026-02-08 14:48:21 -08:00
Copilot
2f4abe2ce6
mpz: use pointer tagging to save space (#8447) 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-08 11:55:14 +00:00
Nuno Lopes
09370d7782 optimize has_sign_bit and mod2k to not compute powers of two 
this is very useful for bitvectors of large bitwidths
 2026-01-31 10:38:41 +00:00
Nuno Lopes
5f835dd99c fix build 2026-01-30 16:29:30 +00:00
Nuno Lopes
095b2bdf59 code simplifications 2026-01-30 15:26:21 +00:00
Nuno Lopes
70a03c7784 constify a constant 
shrinks binary size by 4KB
 2026-01-30 15:01:53 +00:00
Nikolaj Bjorner
573c2cb8f7 micro tuning perfect square test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-13 20:10:43 -07:00
Nikolaj Bjorner
a2993f7457 encapsulate mpz a bit more 2024-01-20 12:59:58 -08:00
Bruce Mitchener
50e0fd3ba6
Use noexcept more. (#7058) 2023-12-16 12:14:53 +00:00
Nikolaj Bjorner
e580c384b8 import updates to rational from polysat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-09 12:46:06 -08:00
Bruce Mitchener
886c3abec1 Remove remnants of _MP_MSBIGNUM checks. 2022-08-02 09:28:57 +03:00
Jakob Rath
6eae27ffad numeral helper functions 2022-08-01 18:37:11 +03:00
Nikolaj Bjorner
2fef6dc502 more scaffolding 2021-03-21 11:31:14 -07:00
Nikolaj Bjorner
4d41db3028 adding euf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-31 14:36:16 -07:00
Nikolaj Bjorner
c7704ef9af pass algebraic manager to arith-plugin mk-numeral because rational check may overwrite the argument using the current manager deals with crash as part of #4532 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-26 17:52:28 -07:00
Nuno Lopes
f30e8ccec3 fix crashes due to my last commit 2020-07-12 19:53:22 +01:00
Nuno Lopes
bb26f219fe remove unneeded constructors (last round) 2020-07-12 17:41:57 +01:00
Nuno Lopes
7ac2791482 remove a bunch of constructors to avoid copies 
still not enough to guarantee that vector::expand doesnt copy (WIP)
 2020-06-03 17:09:27 +01:00
Nuno Lopes
98b5abb1d4 buffer: require a move constructor to avoid copies 
remove unneded copy constructors from several classes
 2020-06-03 11:57:49 +01:00
Nikolaj Bjorner
c2a59a89af thanks to https://github.com/Z3Prover/z3/pull/4382#issuecomment-630468832_ 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-18 15:32:23 -07:00
Nikolaj Bjorner
801eb47fae remove thread dependency in symbol.cpp on single thread #4382 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-18 15:16:08 -07:00
Nikolaj Bjorner
f4472927c0 play nice with sanitizers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 17:39:22 -07:00
Nikolaj Bjorner
abbee32ddc fixup use of SYNC/SYNCH for mpz 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-01 11:18:36 -08:00
Nikolaj Bjorner
5f89ead54b adding t-smt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-31 17:08:53 -08:00
Nikolaj Bjorner
5f2720562b adding threads to smt core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-31 17:08:53 -08:00
Nuno Lopes
a53ff6f21c turn locks into no-ops when compiled with -DSINGLE_THREAD 2019-06-05 12:11:27 +01:00
Nikolaj Bjorner
9262908ebb mux 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 09:06:17 +01:00
nilsbecker
a8586746be cleanup for pull request 2019-02-23 02:47:33 +01:00
nilsbecker
6d2cf4f464 smt-like logging of theory specific meaning of constants 2018-12-10 22:49:08 +01:00
Nikolaj Bjorner
e8a78ec696 remove std::max for #1752 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-03 10:24:01 -07:00
Nikolaj Bjorner
d74978c277 fix #1762, #1764, #1768 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-26 20:29:26 +01:00
Nuno Lopes
b88596283f don't use mp[zq] synchronized mode if OpenMP mode is disabled 2018-07-14 20:44:35 +01:00
Nikolaj Bjorner
dfdf7a0e4a update mpz for NO_GMP 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-03 18:31:05 -07:00
Nikolaj Bjorner
cb7fb524b2 fix NO_GMP compilation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-03 16:22:29 -07:00
Nikolaj Bjorner
a4dfde4671 fix pointer deref 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-03 06:56:37 -07:00
Nikolaj Bjorner
810d63c246 put mpz_cell under ifdef _NO_GMP 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-03 06:54:50 -07:00