mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-09 10:35:36 +00:00
Code Activity
20480 commits 46 branches 56 tags 170 MiB
Commit graph

20480 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson
90971bc356 align with SMT-RAT 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-15 10:13:12 -10:00
Lev Nachmanson
22a7c50e0c toward more like SMT-RAT split 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-15 09:06:45 -10:00
Lev Nachmanson
57d1763809 ignore const non-null witnesses 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-15 06:58:04 -10:00
Lev Nachmanson
8dc0e5bef1 Revert "cache the polynomial roots" 
This reverts commit aefcd16aaa.
 2026-01-14 19:04:22 -10:00
Lev Nachmanson
aefcd16aaa cache the polynomial roots 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 15:30:44 -10:00
Lev Nachmanson
ec05852805 refactor 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:15 -10:00
Lev Nachmanson
2ac311c174 refactor 2026-01-14 07:45:15 -10:00
Lev Nachmanson
6698721f24 refactor 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
7d9000664d discard a discriminant only in the section case 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
87535daf7e try optimizing build_interval_and_relation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
1bd32ab02a avoid a compare call 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
0e38c6c543 use std_vector more 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
ca7d3ca90a omit some disc 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
326963bb69 avoid ldcf with the projective theorem 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
623c5363d8 efficient sort of root functions 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
6c64d271c8 restore choose_non_zero_coeff 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
f0c6336606 simple choice of non-vanishing 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
a75f878c4a fix a bug with non-adding ldcf 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
60507d5692 introduce isolate_root_closest 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
d87d1d009f hook up different relation build strategies for lws 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
946f209b4c t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
29d306ec66 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
8661b68380 t 2026-01-14 07:45:14 -10:00
Lev Nachmanson
84bef9c5b5 simplify by removing back propagation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
27c319327c t 2026-01-14 07:45:14 -10:00
Lev Nachmanson
f6dde3e5f9 fix the duplicate bug 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
5ee9262cdb with resultant calculation ignore one of p and q with a common root 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
66c0aae3df index bug 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
af16e7e143 better sort of root functions 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
8e3a28ac82 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
da74549d9d cleanup and more caching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
4a05e82e7a t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
7c14b5eebb Revert "make normalize optional" 
This reverts commit c80cfb0b8e.
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
cc56749e84 make normalize optional 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
e542a5e520 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
aa436bd5dd optimizations by using cached psc 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
8a90e2c0d8 handle the zero case in add_ord_inv_resultant 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
cf52acb2ce unsound state 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
107b4027d2 unsound state 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
239d3981ef use the cache consistently 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
5a69942895 try not to fail in add_sgn_inv_leading_coeff_for 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
52476bf1d7 normalize polynomials 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
daf4e70f47 t 2026-01-14 07:45:14 -10:00
Lev Nachmanson
cca6f44b11 canonicalize polynomials in nlsat 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
f7400649d2 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
fed3bec7d7 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
33928b0cad canonicalize polinomals in todo_set 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
6837c44be3 do not refactor again multivariate polynomials 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
548888cc99 use polynomial_ref instead of poly* 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00
Lev Nachmanson
5985f9bd34 cosmetics 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:14 -10:00