Lev Nachmanson
|
89f35c95c8
|
Revert "make normalize optional"
This reverts commit c80cfb0b8e.
|
2025-12-18 10:47:40 -10:00 |
|
Lev Nachmanson
|
c80cfb0b8e
|
make normalize optional
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-18 10:02:51 -10:00 |
|
Lev Nachmanson
|
af2ef1c171
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-17 20:12:48 -10:00 |
|
Lev Nachmanson
|
0c0142d6bb
|
optimizations by using cached psc
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-17 15:34:05 -10:00 |
|
Lev Nachmanson
|
c37adafe12
|
handle the zero case in add_ord_inv_resultant
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-17 10:49:31 -10:00 |
|
Lev Nachmanson
|
9fc7e6cfe0
|
unsound state
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-16 09:17:21 -10:00 |
|
Lev Nachmanson
|
55150f36c5
|
unsound state
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-16 09:14:52 -10:00 |
|
Lev Nachmanson
|
2faf5cc138
|
use the cache consistently
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-13 05:59:11 -10:00 |
|
Lev Nachmanson
|
845c0bfff0
|
try not to fail in add_sgn_inv_leading_coeff_for
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-10 16:26:04 -10:00 |
|
Lev Nachmanson
|
1fe7359c7b
|
normalize polynomials
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-10 12:09:38 -10:00 |
|
Lev Nachmanson
|
653a4ece42
|
t
|
2025-12-10 08:29:38 -10:00 |
|
Lev Nachmanson
|
1cb0743e2b
|
canonicalize polynomials in nlsat
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-10 07:56:29 -10:00 |
|
Lev Nachmanson
|
3004222f15
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-09 20:05:13 -10:00 |
|
Lev Nachmanson
|
70ba990f27
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-08 14:45:35 -10:00 |
|
Lev Nachmanson
|
bf32a437c1
|
canonicalize polinomals in todo_set
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-08 11:33:31 -10:00 |
|
Lev Nachmanson
|
aa6dae8f5f
|
do not refactor again multivariate polynomials
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-08 09:58:32 -10:00 |
|
Lev Nachmanson
|
3db21b90f3
|
use polynomial_ref instead of poly*
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-05 18:51:45 -10:00 |
|
Lev Nachmanson
|
ff739d19dd
|
remove an out of place assert
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-05 10:55:30 -10:00 |
|
Lev Nachmanson
|
e895cfb4ae
|
cosmetics
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-05 06:13:37 -10:00 |
|
Lev Nachmanson
|
230ee01fe2
|
call levelwise on a correct set of polynomials
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-04 16:55:49 -10:00 |
|
Lev Nachmanson
|
fc11b7cb9e
|
remove debug instruction
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-04 11:39:29 -10:00 |
|
Lev Nachmanson
|
dffe5c1971
|
fix a bug in Rule 4.2
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-04 11:33:56 -10:00 |
|
Lev Nachmanson
|
e19913779f
|
catch and fail on an exception
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-04 09:54:48 -10:00 |
|
Lev Nachmanson
|
2cff9e277e
|
add stats to track levelwise calls
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 15:07:34 -10:00 |
|
Lev Nachmanson
|
2a6661846c
|
rebase with master
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:56:07 -10:00 |
|
Lev Nachmanson
|
09b2d19deb
|
relax an assert
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
f228565859
|
normalize before pushing
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
5f15bc8f93
|
create a better queue on properties
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
94edbcbf06
|
fix an assert statement
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
53c6b8b082
|
separate the lower and upper bound root functions
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
861bdbd4ed
|
filling the relation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
c721a70d63
|
prepare to fill the relation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
063f1885f4
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
48bd303093
|
debug
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
47e1bd6c12
|
remove a warning
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
a0cc40d9ed
|
process level 0 as well
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
7e038a330c
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
71cfb70f7e
|
add a guard on m_fail
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
ad2abb9028
|
create irreducible polynomials on init
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
9d15f30157
|
new file
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
5c0c278f9f
|
try iterative factoring
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
60726d879a
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
705a4b180d
|
produce more literals but creating sat lemmas
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
1f775195ed
|
adding ir_ord
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
e50fc3caf9
|
fixing factoring and hitting NOT_IMPLEMENTED on ir_ord
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
1f6453e7cc
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
bb05afcd70
|
comment
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
e2f5ceaa0e
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
a9d7a307ba
|
add parameter to suppress/enable levelwise
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
e7888b303b
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|