mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-08 01:57:59 +00:00
Code Activity
20660 commits 49 branches 54 tags 169 MiB
Commit graph

20660 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson
aafc29d2fc Implement chain noLdcf optimization matching SMT-RAT 
Add find_partition_boundary() helper to locate the boundary between
lower and upper root partitions in m_rfunc.

Implement compute_omit_lc_sector_chain() and compute_omit_lc_section_chain()
following SMT-RAT's OneCellCAD.h logic:
- Omit ldcf for extreme of lower chain (index 0) if it appears on upper side
- Omit ldcf for extreme of upper chain (last index) if it appears on lower side

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
 2026-01-31 15:56:43 -10:00
Lev Nachmanson
3a08ee7433 disables some heuristics in section 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:43 -10:00
Lev Nachmanson
f0b939cbd4 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:43 -10:00
Lev Nachmanson
a5abf0c72a align with SMT-RAT 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:43 -10:00
Lev Nachmanson
3a84067075 toward more like SMT-RAT split 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:43 -10:00
Lev Nachmanson
e4976ef0a3 ignore const non-null witnesses 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
0b20411fba Revert "cache the polynomial roots" 
This reverts commit aefcd16aaa.
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
13e3b64068 cache the polynomial roots 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
00595d7a6a refactor 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
f534c15205 refactor 2026-01-31 15:56:42 -10:00
Lev Nachmanson
13ef7cc6f4 refactor 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
5bc7ad0c6c discard a discriminant only in the section case 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
895f7d5fde try optimizing build_interval_and_relation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
9104ee1b5b avoid a compare call 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
7022412f58 use std_vector more 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
6c8fcc8c31 omit some disc 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
bcf6eaec90 avoid ldcf with the projective theorem 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
5a7cc62420 efficient sort of root functions 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
3a011d7c5c restore choose_non_zero_coeff 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
a46261efe5 simple choice of non-vanishing 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
a35fe109ac fix a bug with non-adding ldcf 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
bbece87183 introduce isolate_root_closest 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
ae8262a9d1 hook up different relation build strategies for lws 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
ae8763d760 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
a75718fe2b t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
af01e7d76a t 2026-01-31 15:56:42 -10:00
Lev Nachmanson
fdbac21c28 simplify by removing back propagation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
005bce6397 t 2026-01-31 15:56:42 -10:00
Lev Nachmanson
80c69c9a96 fix the duplicate bug 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
7dc9dcc890 with resultant calculation ignore one of p and q with a common root 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
0861a5ad6e index bug 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
fe136e3ca2 better sort of root functions 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
9ee90b26bf t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
e1db01a5b2 cleanup and more caching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
2174cf5aaf t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
dcc39c59b1 Revert "make normalize optional" 
This reverts commit c80cfb0b8e.
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
b88b4211d7 make normalize optional 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
84fccbee4a t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
1cdb307a04 optimizations by using cached psc 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
a8bd37c56d handle the zero case in add_ord_inv_resultant 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
71bce13c25 unsound state 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
a7e75d1dd9 unsound state 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
c199751db8 use the cache consistently 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
3e29045b68 try not to fail in add_sgn_inv_leading_coeff_for 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
0281ffc905 normalize polynomials 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
3557a7f9c7 t 2026-01-31 15:56:42 -10:00
Lev Nachmanson
2bc13d0de1 canonicalize polynomials in nlsat 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
1e43c54f4b t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
0e56c7757e t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
c81b509fbc canonicalize polinomals in todo_set 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00