mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 08:17:37 +00:00
Code Activity
20526 commits 65 branches 58 tags 180 MiB
Commit graph

1461 commits

Author SHA1 Message Date
Lev Nachmanson
6bce4c2b81 Fix memory leak in undo_fixed_column for big numbers 
The undo_fixed_column struct is region-allocated via trail_stack, so its
destructor is never called. When m_fixed_val contains a big number (one
that doesn't fit in a small int), the heap-allocated memory for the mpq
numerator/denominator was never freed.

Fix by calling m_fixed_val.reset() in undo() to explicitly free the
heap memory before the region deallocates the struct.

Verified with macOS leaks tool:
- Before: 126 leaks (6048 bytes) on convert-jpg2gif-query-1584.smt2
- After: 0 leaks on normal completion, 10 leaks on timeout (unfinished trail)
 2026-02-18 20:57:54 -08:00
Copilot
5af6446c95 [WIP] Find and update std::optional usage in code base (#8272) 
* Initial plan

* Add try_get_value for std::map and use it in var_register.h and dioph_eq.cpp

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add try_get_value overload for unordered_map with custom hash and use in lar_solver.cpp

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Remove redundant try_get_value template overload

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Remove std::map include and try_get_value overload from lp_utils.h

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:57:51 -08:00
Copilot
054a83e925 Adopt std::optional for try_get_value and try_get_size functions (#8268) 
* Initial plan

* Convert try_get_value and try_get_size to use std::optional

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add unit tests for std::optional conversions and fix compilation error

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Address code review comments - improve readability and reduce code duplication

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:57:50 -08:00
Copilot
671faf8f1c Migrate codebase to std::string_view (except z3++.h) (#8266) 
* Initial plan

* Update z3 codebase to use std::string_view (except z3++.h)

- Updated params.cpp/h to use string_view internally for parameter descriptions
- Updated trace.h/cpp to accept string_view for trace tag functions
- Updated hash.h/cpp to use string_view for string_hash function
- Updated all callers of string_hash to use string_view
- Properly handled nullptr to empty string_view conversions
- All tests passing

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add missing string_view includes to headers

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:57:50 -08:00
copilot-swe-agent[bot]
0115b7cadc Fix segfault in dioph_eq.cpp by adding bounds check 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:57:32 -08:00
Copilot
11970f9203 Fix 13 compiler warnings: sign-comparison and unused parameters (#8215) 
* Initial plan

* Fix 13 compiler warnings: sign-comparison and unused parameters

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:57:31 -08:00
Copilot
317dd92105 Standardize for-loop increments to prefix form (++i) (#8199) 
* Initial plan

* Convert postfix to prefix increment in for loops

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix member variable increment conversion bug

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Update API generator to produce prefix increments

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:57:29 -08:00
Copilot
a6c1d32074 Replace empty destructors with = default for compiler optimization (#8189) 
* Initial plan

* Replace empty destructors with = default

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:57:12 -08:00
Copilot
0cc16b63c2 Replace custom util/optional with std::optional (#8162) 
* Initial plan

* Replace optional with std::optional in source files

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix array_map contains() and remove optional_benchmark test

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Address code review feedback - simplify array_map and test

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:57:09 -08:00
Copilot
d68837693c Adopt C++17 structured bindings for map/pair iteration (#8159) 
* Initial plan

* Adopt structured bindings for map iteration

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix DEBUG_CODE macro issue with structured bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:57:09 -08:00
Lev Nachmanson
482ece11a8 when deleting the last row from m_e_matrix go over fresh variables defined for this row and mark the rows depending on them as changed 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:57:04 -08:00
Lev Nachmanson
a49d2b2067 add a check in entry_invariant() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:57:04 -08:00
Lev Nachmanson
0da98c1378 catch a conflict with a fractional sum of fixed variables in a term 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:57:04 -08:00
Lev Nachmanson
cf287e6a64 cosmetics 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:57:04 -08:00
Nikolaj Bjorner
c495cf42b6 fix #8099 (again) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:03 -08:00
Lev Nachmanson
5279c7993d assert entry_invariant only when all changes are done 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:57:03 -08:00
Nikolaj Bjorner
85c8c6bd6b fix #8092 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:00 -08:00
Nikolaj Bjorner
208c5b1b73 fix #8054 
inherit denominators when evaluating polynomials
 2026-02-18 20:56:57 -08:00
Nikolaj Bjorner
e4697fe18e remove set cardinality operators from array theory. Make final-check use priority levels 
Issue #7502 shows that running nlsat eagerly during final check can block quantifier instantiation.
To give space for quantifier instances we introduce two levels for final check such that nlsat is only applied in the second and final level.
 2026-02-18 20:56:51 -08:00
Nikolaj Bjorner
0c1ff55adf fix warnings in nla_pp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:02 -08:00
Nikolaj Bjorner
2fd89c5921 fix warnings in nra_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:02 -08:00
Nikolaj Bjorner
66141dfdfa apply gcd test also before saturation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:00 -08:00
Nikolaj Bjorner
64439a8134 factor out coi, use polynomial elaboration for nlsat solver (#8039) 
* factor out coi, use polynomial elaboration for nlsat solver

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

* remove unused functionality

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

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:55:57 -08:00
Lev Nachmanson
a15b21bc62 try exponential delay in grobner 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-26 15:35:25 +01:00
Nikolaj Bjorner
bda98d8da4 fix #7948 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-28 12:52:20 +03:00
Nikolaj Bjorner
b7eb21efed fix #7948 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-28 12:52:19 +03:00
Nikolaj Bjorner
6173a0d025 propagate value initialization to atoms 2025-09-24 11:01:24 +03:00
Nikolaj Bjorner
eae4de075b fix latent bug in factorization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-23 10:47:24 +03:00
Nikolaj Bjorner
dcdae5a61c add smt debug output for nla_core 2025-09-21 19:24:13 +03:00
Nikolaj Bjorner
a8ae52bfbf fix missing call change to cross-nested. Prepare for lower-bound and upper-bound cardinality constraints 2025-09-19 18:57:50 -07:00
Nikolaj Bjorner
2517b5a40a port improvements from ilana branch to master regarding nla 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-19 12:28:31 -07:00
Nikolaj Bjorner
0d0dd0315a evaluate unhandled arithmetic operators based on an initialized model #7876 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-14 06:45:36 -07:00
Nikolaj Bjorner
866393a842 update defaults for new grobner featuers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-05 14:34:03 -07:00
Nikolaj Bjorner
d7718623a4 handle case where all variables are bounded 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-04 12:58:03 -07:00
Nikolaj Bjorner
98a9a34f2b add option to reduce pseudo-linear monomials 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-04 11:04:12 -07:00
Nikolaj Bjorner
e0c315bc3e filter pseudo-linear monomials 2025-09-03 17:51:12 -07:00
Nikolaj Bjorner
a382ddbd8a add rewrite for mod over negation, refine axioms for grobner quotients 2025-09-02 18:26:22 -07:00
Nikolaj Bjorner
e2235d81d3 add option for gcd-test to grobner 2025-09-01 16:37:21 -07:00
Nikolaj Bjorner
49703f8bba remove debug out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-31 17:41:42 -07:00
Nikolaj Bjorner
4c0c199e32 take into account integer coefficients 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-31 16:07:37 -07:00
Nikolaj Bjorner
e91e432496 add option to propagation quotients 
for equations x*y + z = 0,
with x, y, z integer, enforce that x divides z
It is (currently) enabled within Grobner completion
and applied partially to x a variable, z linear, and
only when |z| < |x|.
 2025-08-31 14:41:23 -07:00
Nikolaj Bjorner
91b4873b79 categorize lp stats 2025-08-29 17:06:13 -07:00
Nikolaj Bjorner
c75b8ec752 add option to control epsilon #7791 
#7791 reports on using model values during lex optimization that break soft constraints.
This is an artifact of using optimization where optimal values can be arbitrarily close to a rational.
In a way it is by design, but we give the user now an option to control the starting point for epsilon when converting infinitesimals into rationals.
 2025-08-17 16:51:00 -07:00
Nikolaj Bjorner
1a488bb67a indentation 2025-07-25 11:00:30 -07:00
Nikolaj Bjorner
a28f55a3bc log scope level of lemma 2025-07-01 14:14:30 -07:00
Nikolaj Bjorner
bfed237a6c expose scope level 2025-07-01 14:14:16 -07:00
Lev Nachmanson
28d0b471ff following the review comments 2025-06-27 19:48:51 -07:00
Lev Nachmanson
d717dae3ac remove the parameter for throttling nla lemmas 2025-06-26 16:33:16 -07:00
Lev Nachmanson
2b6c73af82 add stats for throttling 2025-06-26 16:33:16 -07:00
Lev Nachmanson
899677e626 fix a warning 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-06-26 16:33:16 -07:00