mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-05 08:30:50 +00:00
Code Activity
22233 commits 107 branches 58 tags 215 MiB
Commit graph

61 commits

Author SHA1 Message Date
Copilot
a5e1078172
Silence GCC false positives in bound propagation and mpz sign-cell paths (#9530) 
Recent GCC builds report two warning classes in core codepaths: a
possible uninitialized read in `bound_propagator::relevant_bound`, and
repeated `-Warray-bounds` diagnostics in `mpz_manager::get_sign_cell`
when materializing small integers into a reserved `mpz_cell`.

- **Warning cleanup in bound propagation**
- Initialize `interval_size` at declaration in
`src/ast/simplifiers/bound_propagator.cpp` so the compiler can prove
safety across templated `LOWER/UPPER` instantiations using `std::clamp`.
- Preserves existing control flow and refinement heuristics (`bounded`
remains the gate for interval-based logic).

- **Warning cleanup in mpz small-value cell materialization**
- In `src/util/mpz.h`, replace direct writes through `cell->m_digits[0]`
with writes via a derived digits pointer
(`reinterpret_cast<digit_t*>(cell + 1)`), avoiding zero-length
trailing-array indexing diagnostics.
- Keeps memory layout and semantics unchanged for the stack-reserved
`sign_cell` buffer.

- **Representative change**
  ```cpp
  cell = reserve;
  cell->m_size = 1;
  digit_t* cell_digits = reinterpret_cast<digit_t*>(cell + 1);
  cell_digits[0] = a.value() < 0 ? -a.value() : a.value();
  ```

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-05-13 17:24:13 -04: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
Nikolaj Bjorner
3a4200ae5f null -> nullptr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 18:32:03 -07:00
Nikolaj Bjorner
ace4dbe32b fix memory leak exposed by tan.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 18:15:39 -07:00
Nikolaj Bjorner
4e657b5b7e rename mpz_ptr to mpz_large 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 15:29:57 -07:00
Lev Nachmanson
40a363d249 Nikolaj's changes in rationals 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-28 16:22:40 -07:00
Lev Nachmanson
c2f3428373 name change 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-28 15:02:23 -07:00
Lev Nachmanson
9ba4026bc6 avoid going creating hnf_cuts if all involved vars have integral values 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

add explanations to hnf cuts

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

nits and virtual methods (#68)

* local

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* virtual method in bound propagator

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

cleanup from std::cout

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

handle the case when the number of terms is greater than the number of variables in hnf

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

method name's fix

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

restore hnf_cutter to work with m_row_count <= m_column_count

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

tune addition of rational numbers (#70)

* log quantifiers only if present

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge and fix some warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* set new arith as default for LIA

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* local

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* virtual method in bound propagator

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* prepare for mixed integer-real

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix default tactic usage

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

give shorter explanations, call hnf only when have a not integral var

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

overhaul of mpq (#71)

* log quantifiers only if present

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge and fix some warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* set new arith as default for LIA

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* local

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* virtual method in bound propagator

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* prepare for mixed integer-real

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix default tactic usage

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* overhaul of mpz/mpq

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disabled temporary setting

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove prints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

fix for 32 bit build (#72)

* log quantifiers only if present

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge and fix some warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* set new arith as default for LIA

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* local

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* virtual method in bound propagator

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* prepare for mixed integer-real

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix default tactic usage

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* overhaul of mpz/mpq

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disabled temporary setting

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove prints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* customize for 64 bit

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

yes (#74)

* log quantifiers only if present

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge and fix some warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* set new arith as default for LIA

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* local

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* virtual method in bound propagator

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* prepare for mixed integer-real

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix default tactic usage

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* overhaul of mpz/mpq

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disabled temporary setting

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove prints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* customize for 64 bit

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* customize for 64 bit

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more refactor

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

fix the merge

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

fixes in maximize_term untested

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

fix compilation (#75)

* log quantifiers only if present

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge and fix some warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* set new arith as default for LIA

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* local

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* virtual method in bound propagator

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* prepare for mixed integer-real

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix default tactic usage

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* overhaul of mpz/mpq

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disabled temporary setting

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove prints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* customize for 64 bit

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* customize for 64 bit

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more refactor

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* relax check

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* change for gcc

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-27 12:16:58 -07:00
Bruce Mitchener
2fa304d8de Remove int64, uint64 typedefs in favor of int64_t / uint64_t. 2018-03-31 14:45:04 +07:00
Bruce Mitchener
76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Bruce Mitchener
ae8027e594 Fix typos. 2018-02-01 19:39:43 +07:00
Nuno Lopes
d1c13f17b0 remove noexcept since MSVC 2012 doest support it 2017-10-16 00:54:30 +01:00
Nuno Lopes
27e84c5ffc mpz.h: fix typo in previous commit (found by Nikolaj) 2017-10-16 00:54:29 +01:00
Nuno Lopes
9b54b4e784 fix vector<> to support non-POD types 
adjust code to std::move and avoid unnecessary/illegal
 2017-10-16 00:54:29 +01: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