mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-20 23:44:41 +00:00
Code Activity
20388 commits 53 branches 58 tags 179 MiB
Commit graph

1453 commits

Author SHA1 Message Date
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
Lev Nachmanson
9e52a38580 add throttling to generate_plane1/2 2025-06-26 16:33:16 -07:00
Lev Nachmanson
ac34dbd030 consolidate throttling 2025-06-26 16:33:16 -07:00
Lev Nachmanson
727dfd2d8d use the new throttle in order lemmas 2025-06-26 16:33:16 -07:00
Lev Nachmanson
832cfb3c41 consolidate throttling 2025-06-26 16:33:16 -07:00
Lev Nachmanson
f32066762c remove debug_location parameter 2025-06-26 16:33:16 -07:00
Lev Nachmanson
5caa7f1a29 throttle lemmas in nla_solver untested 2025-06-26 16:33:16 -07:00
Lev Nachmanson
46319156b8 a version of key 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-06-26 16:33:16 -07:00
Lev Nachmanson
20fb830682 filter out empty lemmas from nla_solver on consumption 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-06-26 16:33:16 -07:00