mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-21 20:18:50 +00:00
Code Activity
21714 commits 71 branches 58 tags 206 MiB
Commit graph

1499 commits

Author SHA1 Message Date
Valentin Promies
8f9c527444 Merge branch 'master' into nl2lin 2026-02-20 12:55:51 +01:00
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
Lev Nachmanson
a6f44f8c88 Merge branch 'master' into nl2lin 
# Conflicts:
#	src/math/lp/nla_coi.cpp
#	src/math/lp/nla_coi.h
#	src/math/lp/nla_core.cpp
#	src/math/lp/nla_grobner.cpp
#	src/math/lp/nla_grobner.h
#	src/math/lp/nla_pp.cpp
#	src/math/lp/nra_solver.cpp
#	src/nlsat/nlsat_explain.h
#	src/smt/theory_lra.cpp
 2025-12-16 11:47:13 -10: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
Lev Nachmanson
caec692706 add forgotten files 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-25 06:16:08 -10: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
Lev Nachmanson
ddba2cc381 integrating changes from master related to work with polynomials 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 13:00:43 -10: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
Lev Nachmanson
6cbc6f4f84 create polynomials with integer coefficients, use the hook to create new monomials 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-06 11:53:06 -07:00
Nikolaj Bjorner
f8942dfdee simplify 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-02 20:17:29 -07:00
Lev Nachmanson
84a9b38ec8 debug the setup, still not working 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-02 17:25:48 -07:00
Nikolaj Bjorner
874e8b3cfa call setup_assignment_solver instead of setup_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-02 08:58:15 -07:00
Nikolaj Bjorner
ba378ed341 fixup backtranslation to not use roots 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-02 08:55:27 -07:00
Nikolaj Bjorner
fe8f721600 add internalization routine that uses macro-expanded polynomial representation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-02 08:37:14 -07:00
Nikolaj Bjorner
3e47d1099d add internalization routine that uses macro-expanded polynomial representation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-02 08:36:39 -07:00
Lev Nachmanson
1adfa94823 add a hook to add new multiplication definitions in nla_core 2025-09-30 16:47:49 -07:00
Lev Nachmanson
d79d43355f remove a comment 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-09-29 13:23:20 -07:00
Lev Nachmanson
5de0b8a87f do not set use_nra_model to true 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-09-29 13:20:46 -07:00
Lev Nachmanson
cc957011f2 remove the too early return 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-09-29 13:12:15 -07:00