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

263 commits

Author SHA1 Message Date
Copilot
bbf984f182 [WIP] Refactor NLSAT solver to use structured bindings for variable bounds (#8425) 
* Initial plan

* Refactor NLSAT solver to use structured bindings for variable bounds

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:59 -08:00
Lev Nachmanson
cec23dcc78 revive nlsat check_lemma() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:57:54 -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
Lev Nachmanson
1200c0bd0c remove unused *_signed_project() methods 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:56:57 -08:00
Nikolaj Bjorner
08babfff60 fix build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:02 -08:00
Lev Nachmanson
f8ce742890 try reordering before analyzing bounds 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:56:00 -08:00
Lev Nachmanson
79f83154a3 parameter correct order experiment 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:56:00 -08:00
Lev Nachmanson
80acfbeea3 remove the debug print 2026-02-18 20:56:00 -08:00
Lev Nachmanson
b582b2f32e disable add_zero_disc(disc) by default 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:56:00 -08:00
Lev Nachmanson
1f3d61b6f4 optionally call add_zero_assumption on a vanishing discriminant 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:56:00 -08:00
Lev Nachmanson
a94373981a restart projection when found a non-trivial nullified polynomial, and remove is_square_free 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:56:00 -08:00
Lev Nachmanson
7909e2498a refactoring 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
c9add31da7 remove unused code 2026-02-18 20:55:59 -08:00
Lev Nachmanson
d2dd7f9df5 remve add_zero_assumption from pcs() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
8f97785498 improve logging 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
82958565ed handle the case with no roots in add_zero_assumption 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
08ca76533a improve log_lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
b088b3e7c0 log for smtrat 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
0179ed855d use indexed root expressions id add_zero_assumption 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
50e4452e62 add coefficients from the elim_vanishing to m_todo 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
f0b292dd16 remove unused method 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
d088bd669e t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
5dd3034000 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
f60d62794a t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
905210b165 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
50d8a8049a t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
37a5df8d95 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
602e7e906b t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
235c9b5d5a t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
5bb0bf94c9 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
a9c84c7950 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
b4850019f2 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
4e38c440bd t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
b2a1293fe2 better state 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
d93caa9c7f unsound lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
07501f7c1f change logic NRA->ALL in log_lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:55 -08:00
Lev Nachmanson
e980f92a9e enable always add all coeffs in nlsat 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-26 15:35:25 +01:00
Lev Nachmanson
351c0401fb restore the method behavior 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-26 15:32:21 +01:00
Lev Nachmanson
d9ca739499 restore single cell 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-26 15:32:21 +01:00
Nikolaj Bjorner
2337e68169 fix #7822 2025-08-27 09:17:55 -07:00
Lev Nachmanson
cf8a17a6ae restore the square-free check 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-08-11 13:16:37 -07:00
Lev Nachmanson
e33dc47d83 remove unused square-free check 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-08-11 07:24:42 -07:00
Lev Nachmanson
8598a74cca rename add_lcs to add_lc 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-08-08 11:02:30 -07:00
Lev Nachmanson
88293bf45b get the finest factorizations before project 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-08-08 11:02:30 -07:00
Lev Nachmanson
d2990e2f68 use usize to suppress the data loss warnings 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-07-02 14:42:55 -07:00
Nikolaj Bjorner
f544dd4ab2 deal with warnings 
@levnach - there are some additional warnings.
You could revert the change to std_vector or use usize() that I added to vector.h. Look at build logs from the pipelines or actions or figure out how to add a continuous AI script to fixup build warnings (I tried a few times earlier on but the features available to do this were not for laymen).
 2025-07-02 10:59:56 -07:00
Lev Nachmanson
8f88bf9998 use is_square_free_at_sample instead of is_well_oriented 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-06-17 07:22:03 -07:00
Lev Nachmanson
f2912b25a2 remove debug output 2025-06-17 07:22:03 -07:00
Lev Nachmanson
0e71a9d11c comment and restore 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-06-17 07:22:03 -07:00
Lev Nachmanson
84c8a93ca5 renaming 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-06-17 07:22:03 -07:00