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
|
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 |
|
Lev Nachmanson
|
a39d8cf12d
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
5ebb2fcd8d
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
ae171dfee2
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
79899e1b52
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
3cd49d0e54
|
introdure mk_prop
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
a8226b04f2
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
73741fecfe
|
got a section
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
05d5669e21
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
d0e340afe4
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
282ee84223
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
014d02d180
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
1aab5cf37f
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
52a76af764
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
415bd451c2
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
191a4f6e0f
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
b55508ce95
|
ignore holds properties
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
9c7b91a68e
|
remove erase_from_Q
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
605a24b169
|
simplify
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
6daf2c26dd
|
simplify
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
13abcbaa4e
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
516a906393
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
97692ac0b8
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
696cb57278
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
a2e05443f1
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
f51083fd99
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
ade559e762
|
add a display method
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
3d6c3a6cb0
|
refactor and assert _irreducible
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
668064c39e
|
debug
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
458fb58b50
|
simplify
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
78c1b08c4c
|
simplify
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
e83e5d03ae
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
2271c6d038
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
4dbd3725d1
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
6633eaf671
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
4ee6650d90
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
f443f7716b
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:26 -10:00 |
|
Lev Nachmanson
|
747e415110
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:25 -10:00 |
|
Lev Nachmanson
|
2eaba91b99
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:25 -10:00 |
|
Lev Nachmanson
|
d31380416f
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:25 -10:00 |
|