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

20663 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson
4234d6ad8c Refactor levelwise: consolidate partition indices into m_l_rf/m_u_rf 
Replace scattered local l_index/u_index parameters and m_partition_boundary
with two impl members:
- m_l_rf: position of lower bound in m_rel.m_rfunc
- m_u_rf: position of upper bound in m_rel.m_rfunc (UINT_MAX in section case)

This simplifies the code by:
- Removing parameter passing through multiple function calls
- Removing redundant m_partition_boundary from relation_E
- Making the partition state explicit in impl

Also clean up nlsat_explain.cpp to trust root_function_interval invariants:
- Section case: assert l and l_index are valid instead of defensive check
- Sector bounds: !l_inf()/!u_inf() implies valid polynomial and index

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
 2026-01-31 15:56:43 -10:00
Lev Nachmanson
3e52fbb33d Cache partition boundary to avoid repeated algebraic number comparisons 
Store the partition boundary (index of first root > sample) in
relation_E after sorting root functions. Use this cached value
in compute_omit_lc_sector_chain() and compute_omit_lc_section_chain()
instead of recomputing via algebraic number comparisons.

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
 2026-01-31 15:56:43 -10:00
Lev Nachmanson
6b7576c3e0 Restrict noDisc optimization to section_lowest_degree only 
Match SMT-RAT behavior: noDisc (discriminant omission for leaves
connected only to section polynomial) is only applied for
sectionHeuristic == 3 (lowest_degree), not for biggest_cell or chain.

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
 2026-01-31 15:56:43 -10:00
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