Lev Nachmanson
|
92577c39f6
|
rebase with master
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:42 -10:00 |
|
Lev Nachmanson
|
52d0a6d87c
|
relax an assert
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:42 -10:00 |
|
Lev Nachmanson
|
387bd49ae3
|
normalize before pushing
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:42 -10:00 |
|
Lev Nachmanson
|
38f15833ed
|
create a better queue on properties
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:42 -10:00 |
|
Lev Nachmanson
|
8a3e05e507
|
fix an assert statement
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:42 -10:00 |
|
Lev Nachmanson
|
eb7770a958
|
separate the lower and upper bound root functions
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:42 -10:00 |
|
Lev Nachmanson
|
3d44cb9024
|
filling the relation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:42 -10:00 |
|
Lev Nachmanson
|
927fe0c74e
|
prepare to fill the relation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:42 -10:00 |
|
Lev Nachmanson
|
aab881baa9
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:42 -10:00 |
|
Lev Nachmanson
|
4a2a18af31
|
debug
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:42 -10:00 |
|
Lev Nachmanson
|
bcb581ff0a
|
remove a warning
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:42 -10:00 |
|
Lev Nachmanson
|
e76f493e6a
|
process level 0 as well
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:42 -10:00 |
|
Lev Nachmanson
|
69f1cd53d9
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:42 -10:00 |
|
Lev Nachmanson
|
5119be4ad2
|
add a guard on m_fail
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:42 -10:00 |
|
Lev Nachmanson
|
dace878067
|
create irreducible polynomials on init
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
11c3643602
|
new file
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
ab9ced09e2
|
try iterative factoring
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
f8c5f74d05
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
7094cd4a99
|
produce more literals but creating sat lemmas
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
555614ff06
|
adding ir_ord
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
3cb6ed6227
|
fixing factoring and hitting NOT_IMPLEMENTED on ir_ord
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
f673fbf34d
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
093faafbf8
|
comment
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
f0dde9d3ee
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
5ac4b8d06d
|
add parameter to suppress/enable levelwise
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
1ff8cc24c8
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
7a0905fee9
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
da66586a9d
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
e9d0addb32
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
35fac9c578
|
remove a parameter
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
ee1dfd49c5
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
de4ae16be8
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
e2ee6ae59d
|
introdure mk_prop
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
d02633e60b
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
fe16edf973
|
got a section
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
996b0e2ebf
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
71950f059f
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
5f818916e7
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
b4143ac2b0
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
7d80e15efe
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
1b156d4da9
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
802b10eb13
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
20b20997dd
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
5317e0424b
|
ignore holds properties
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
46d1994a8e
|
remove erase_from_Q
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
40b777f1a5
|
simplify
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
b1675466bf
|
simplify
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
cb553da42d
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
6cf3528252
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
4a8bae812a
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|