Lev Nachmanson
|
d8247027e6
|
produce more literals but creating sat lemmas
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:14 -10:00 |
|
Lev Nachmanson
|
951a2af9f9
|
adding ir_ord
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:14 -10:00 |
|
Lev Nachmanson
|
1c4b28def1
|
fixing factoring and hitting NOT_IMPLEMENTED on ir_ord
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:14 -10:00 |
|
Lev Nachmanson
|
7f7658cc52
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:14 -10:00 |
|
Lev Nachmanson
|
eb6758bd6f
|
comment
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
d57c0444f7
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
14cdad13cd
|
add parameter to suppress/enable levelwise
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
425213ab18
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
3b82d4cb9e
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
8ae92cad74
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
fbbbc68a34
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
c0336e7836
|
remove a parameter
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
25ee8b36bd
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
ece8a27c29
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
0ef3d0cdd4
|
introdure mk_prop
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
b2649e1959
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
ef75f48824
|
got a section
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
765f5c2503
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
d2894366e8
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
9fd172d28d
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
2474e53951
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
31ae46f7a9
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
5b78ec0a8c
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
f94578ceb0
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
3c73c8936a
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
8193f67b84
|
ignore holds properties
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
4e4e24fbe1
|
remove erase_from_Q
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
76b7acaf2b
|
simplify
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
30b3a156b8
|
simplify
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
6e10b93952
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
6e8dea6023
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
cf1bea1d59
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
402680f340
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
533f568775
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
97535c5a7c
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
48ceea699d
|
add a display method
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
70d54ef175
|
refactor and assert _irreducible
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
9d6dd07f33
|
debug
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
fbd9ba73f9
|
simplify
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
3d1a4bbb32
|
simplify
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
f3a2de12bd
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
ad143d4bac
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
59645d1055
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
5819ceb184
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
55c986c2fe
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
55086950e2
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
a33820aa71
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
037f4b82b0
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
bb4cefd1e1
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|
Lev Nachmanson
|
fd41daf6ef
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-14 07:45:13 -10:00 |
|