Lev Nachmanson
|
470ea5ea59
|
remove the fresh definition when removing its column
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-06 16:50:24 -10:00 |
|
Lev Nachmanson
|
67318e238f
|
comment change
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-06 13:41:14 -10:00 |
|
Lev Nachmanson
|
df88e3aa4a
|
stricter is_in_sync paying attenion to m_row2fresh_defs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-06 13:16:42 -10:00 |
|
Lev Nachmanson
|
28cc740c39
|
throttle the branching in dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-06 14:28:11 -08:00 |
|
Lev Nachmanson
|
f64edb6c74
|
ignore large changed_columns
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-06 05:45:50 -10:00 |
|
Lev Nachmanson
|
78fea66703
|
fix assert
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-05 18:24:00 -10:00 |
|
Lev Nachmanson
|
46a7ad689b
|
avoid usisg indexed_vector for term operations
|
2025-02-05 17:54:58 -10:00 |
|
Lev Nachmanson
|
30064d4bcb
|
disallow duplicates in a queue
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-05 15:41:24 -08:00 |
|
Lev Nachmanson
|
e419e58ce8
|
add stats on m_dio_branching_conflicts
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-05 10:42:33 -10:00 |
|
Lev Nachmanson
|
f5150ec589
|
call normalize_e_by_gcd() only when moving an entry from F to S
|
2025-02-04 12:38:16 -10:00 |
|
Lev Nachmanson
|
4a953eb1e4
|
rebase with master
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 19:21:24 -10:00 |
|
Lev Nachmanson
|
a38c9be60d
|
make dio less aggressive, allow other cuts
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:39:09 -10:00 |
|
Lev Nachmanson
|
993e12de24
|
register m_added_terms in m_changed_terms
|
2025-02-03 13:39:08 -10:00 |
|
Lev Nachmanson
|
2ed8cd0b9a
|
out of bounds fixes
|
2025-02-03 13:39:08 -10:00 |
|
Lev Nachmanson
|
bdfa6bed61
|
use m_chandedNterms to tighten terms
|
2025-02-03 13:39:08 -10:00 |
|
Lev Nachmanson
|
34eb121bfe
|
remove struct entry
|
2025-02-03 13:39:06 -10:00 |
|
Lev Nachmanson
|
49e3dd6731
|
optimise l terms addition
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:39:06 -10:00 |
|
Lev Nachmanson
|
78694eb07e
|
use the trail to undo add_term
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:39:06 -10:00 |
|
Lev Nachmanson
|
fb6d10078c
|
fix the debug build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:39:06 -10:00 |
|
Lev Nachmanson
|
d8f332b8a7
|
optimise rewrite_eqs to avoid fresh variables
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:39:05 -10:00 |
|
Lev Nachmanson
|
3c4954d18e
|
make rewrite_eq boolean, and relax an ASSERT
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:39:05 -10:00 |
|
Lev Nachmanson
|
179e602c1e
|
clean up fresh definitions on a pop
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:39:05 -10:00 |
|
Lev Nachmanson
|
81bcb58db7
|
debug dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:39:04 -10:00 |
|
Lev Nachmanson
|
43dc43e5cd
|
don't store fresh definitions in m_e_matrix
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:38:56 -10:00 |
|
Lev Nachmanson
|
a3747f5bc9
|
cleanup
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:38:01 -10:00 |
|
Lev Nachmanson
|
f5ef569875
|
remove recalculated entries from S
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:38:00 -10:00 |
|
Lev Nachmanson
|
8e071bcf3c
|
fix out of bounds bug
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:38:00 -10:00 |
|
Lev Nachmanson
|
ff6f7ed854
|
substitute variables with a queue on the recalculated entries
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:38:00 -10:00 |
|
Lev Nachmanson
|
634e541648
|
simplify dio handler by using bijection m_k2s
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:37:59 -10:00 |
|
Lev Nachmanson
|
b208756769
|
use entry_status for FRESH entries
|
2025-02-03 13:37:59 -10:00 |
|
Lev Nachmanson
|
64d77d9cfe
|
fix some warnings
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:37:58 -10:00 |
|
Lev Nachmanson
|
c73e99ddf4
|
fix some warnings
|
2025-02-03 13:37:57 -10:00 |
|
Lev Nachmanson
|
16b41174a2
|
remove var_register_dio.h
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:37:56 -10:00 |
|
Lev Nachmanson
|
f11dfc5680
|
test dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:37:56 -10:00 |
|
Lev Nachmanson
|
3028465b32
|
debug dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:37:54 -10:00 |
|
Lev Nachmanson
|
8d72371778
|
bug fixes
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:37:54 -10:00 |
|
Lev Nachmanson
|
21268f9577
|
refine trail iterations with lar.m_terms
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:37:54 -10:00 |
|
Lev Nachmanson
|
55c983dffb
|
introdure lar_term.ext_coeffs(), dio passes some tests
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:37:47 -10:00 |
|
Lev Nachmanson
|
e8f806a2de
|
debug dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:31 -10:00 |
|
Lev Nachmanson
|
5cdcf3a372
|
cleanup
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:31 -10:00 |
|
Lev Nachmanson
|
c750edf073
|
debug dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:31 -10:00 |
|
Lev Nachmanson
|
039ce4f910
|
fix ubuntu build in dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:31 -10:00 |
|
Lev Nachmanson
|
c263b15924
|
track changed columns in dio\
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:31 -10:00 |
|
Lev Nachmanson
|
2c541924ef
|
use std_vector more and getting NOT_IMPLEMENTING in C:\dev\z3\src\math\lp\dioph_eq.cpp
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:30 -10:00 |
|
Lev Nachmanson
|
5e23e778f4
|
work on incremental dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:30 -10:00 |
|
Lev Nachmanson
|
b2964f8d1e
|
cleanup
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:30 -10:00 |
|
Lev Nachmanson
|
af857810e8
|
work on incremental dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:30 -10:00 |
|
Lev Nachmanson
|
4dd701a5b4
|
remove some warnings
|
2025-02-03 13:33:29 -10:00 |
|
Lev Nachmanson
|
0d3abbb5e0
|
test
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:29 -10:00 |
|
Lev Nachmanson
|
f2b05af67e
|
test
|
2025-02-03 13:33:28 -10:00 |
|