mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-18 14:44:21 +00:00
Code Activity
20749 commits 42 branches 57 tags 176 MiB
Commit graph

1472 commits

Author SHA1 Message Date
Copilot
20fef3f449
Eliminate unnecessary copy operations in function parameters and range-based loops (#8589) 2026-02-11 21:14:32 +00:00
Nuno Lopes
915ad35012 remove a few copies 2026-02-10 09:52:03 +00:00
Lev Nachmanson
f5b8dfc2f1 Revert "optionally throttle patch_basic_columns() especially useful in unsat cases" 
This reverts commit bee2b45743.
 2026-02-07 10:45:15 -10:00
Lev Nachmanson
73696725e4 Revert "try fixed int patch period" 
This reverts commit 3e2027ec11.
 2026-02-07 10:45:15 -10:00
Lev Nachmanson
3e2027ec11 try fixed int patch period 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-06 14:40:04 -10:00
Lev Nachmanson
bee2b45743 optionally throttle patch_basic_columns() especially useful in unsat cases 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-06 10:14:39 -10:00
Copilot
23c531a4c1
Remove redundant default constructors when they're the only constructor (#8461) 
* Initial plan

* Modernize C++ constructors to use C++11 default member initialization - Phase 1

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

* Fix theory_pb.h struct definition - move reset() back inside struct

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

* Modernize C++ constructors to use C++11 default member initialization - Phase 2

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

* Fix opt_solver.h - revert rational initialization (complex type)

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

* Modernize C++ constructors to use C++11 default member initialization - Phase 3

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

* Fix sparse_matrix.h - explicitly initialize union member in default constructor

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

* Remove unnecessary default constructors when they're the only constructor

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-01 16:51:26 -08:00
Copilot
97bf2a5145
Remove redundant non-virtual destructors with = default (#8462) 
* Initial plan

* Remove 6 non-virtual destructors with no code (= default)

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-01 15:22:58 -08:00
Lev Nachmanson
adac953e87 - When removing a fresh var xt, collect all fresh defs that transitively reference it 
- Remove them all from m_fresh_k2xt_terms and m_row2fresh_defs
    - Mark rows containing those vars in m_changed_rows for recalculation
    - Move remove_irrelevant_fresh_defs() before the recalculate loop so all affected rows get recalculated

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-29 06:17:14 -10:00
Nikolaj Bjorner
8a0207700c
Fix implicit conversion warnings: use UINT_MAX instead of -1 for unsi… (#8342) 
* Fix implicit conversion warnings: use UINT_MAX instead of -1 for unsigned variables

Replace implicit conversion from negative literal to unsigned type
with explicit UINT_MAX constant to eliminate compiler warnings.

Fixed 10 instances across 6 files:
- src/ast/rewriter/bv_rewriter.cpp: 1 instance
- src/ast/sls/sls_bv_tracker.h: 2 instances
- src/math/lp/dioph_eq.cpp: 3 instances
- src/math/lp/lp_primal_core_solver.h: 2 instances
- src/muz/transforms/dl_mk_array_instantiation.cpp: 1 instance
- src/muz/transforms/dl_mk_synchronize.cpp: 1 instance

These changes preserve the exact same runtime behavior (UINT_MAX
equals the wrapped value of -1 for unsigned types) while making
the code more explicit and warning-free.

* Update bv_rewriter.cpp

---------

Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com>
 2026-01-25 22:35:43 -08:00
Lev Nachmanson
b154667092 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-01-24 08:17:49 -10:00
Copilot
c392592831
[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-01-21 19:55:36 -08:00
Copilot
1bb471447e
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-01-21 12:41:50 -08:00
Copilot
2e7b700769
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-01-21 09:30:41 -08:00
Lev Nachmanson
d60373c5d5
Merge pull request #8218 from Z3Prover/copilot/fix-segmentation-fault-ufnira 2026-01-17 05:18:38 -10:00
copilot-swe-agent[bot]
522aa69e09 Fix segfault in dioph_eq.cpp by adding bounds check 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-17 00:04:21 +00:00
Copilot
36323f723b
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-01-16 16:00:42 -08:00
Copilot
2436943794
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-01-14 19:55:31 -08:00
Copilot
7377d28c30
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-01-13 10:50:10 -08:00
Copilot
4d188f07e9
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-01-11 19:47:39 -08:00
Copilot
31122b0c10
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-01-11 17:44:12 -08:00
Lev Nachmanson
623b32239c 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-01-02 11:56:35 -10:00
Lev Nachmanson
918722d2f6 add a check in entry_invariant() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-02 10:54:36 -10:00
Lev Nachmanson
17dffc67c9 catch a conflict with a fractional sum of fixed variables in a term 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-30 16:09:35 -10:00
Lev Nachmanson
58462938fa cosmetics 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-30 16:09:35 -10:00
Nikolaj Bjorner
c12425c86f fix #8099 (again) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-12-25 14:16:54 -08:00
Lev Nachmanson
ce2405aab6 assert entry_invariant only when all changes are done 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-25 11:33:32 -10:00
Nikolaj Bjorner
60926e0347 fix #8092 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-12-16 15:49:49 -08:00
Nikolaj Bjorner
a5488cf6e7 fix #8054 
inherit denominators when evaluating polynomials
 2025-11-30 07:51:06 -08:00
Nikolaj Bjorner
62b3668beb 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.
 2025-11-26 15:35:19 -08:00
Nikolaj Bjorner
d1272defeb fix warnings in nla_pp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-25 21:48:23 -08:00
Nikolaj Bjorner
324fb2194b fix warnings in nra_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-25 21:46:51 -08:00
Nikolaj Bjorner
40d8d5ad9a apply gcd test also before saturation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-24 18:08:30 -08:00
Nikolaj Bjorner
7395152632
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>
 2025-11-23 08:59:55 -08:00
Lev Nachmanson
58e64ea826 try exponential delay in grobner 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-22 17:00:16 -07: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