Lev Nachmanson
|
f2c1fd4c14
|
try markovich number
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
cec8dc2e6e
|
try markovich number
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
3f2d2e8348
|
test
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
b6701d57f9
|
try another sort in tightening
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
5b0b224a5c
|
try sorting terms before tightening
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
dcd5783232
|
remove the fresh definition when removing its column
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
17d68c18aa
|
comment change
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
d90b94d0e2
|
stricter is_in_sync paying attenion to m_row2fresh_defs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
134bed826a
|
throttle the branching in dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
bd8cf29df7
|
ignore large changed_columns
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
3ac11cd136
|
fix assert
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
cf4e402a0f
|
avoid usisg indexed_vector for term operations
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
440d78f237
|
disallow duplicates in a queue
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
7e02dfe484
|
add stats on m_dio_branching_conflicts
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
0bf3ca87e7
|
call normalize_e_by_gcd() only when moving an entry from F to S
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
99538567a7
|
rebase with master
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
a19e10912f
|
make dio less aggressive, allow other cuts
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
fee707842d
|
register m_added_terms in m_changed_terms
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
21f67ef942
|
out of bounds fixes
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
3b3d8cee03
|
use m_chandedNterms to tighten terms
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
65bdd58d3e
|
remove struct entry
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
a9098a5785
|
optimise l terms addition
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
3e7e903d19
|
use the trail to undo add_term
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
9c510018b3
|
fix the debug build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
058b9e4a6d
|
optimise rewrite_eqs to avoid fresh variables
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
ed3df333b3
|
make rewrite_eq boolean, and relax an ASSERT
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
ca7c128d3f
|
clean up fresh definitions on a pop
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
b027761845
|
debug dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
bb869fd020
|
don't store fresh definitions in m_e_matrix
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
e5ffc3cfae
|
cleanup
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
d7de7eb732
|
remove recalculated entries from S
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
ef55de1646
|
fix out of bounds bug
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
3990df6d91
|
substitute variables with a queue on the recalculated entries
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
78d91f3794
|
simplify dio handler by using bijection m_k2s
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
33f5e303f8
|
use entry_status for FRESH entries
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
0e71adfa35
|
fix some warnings
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
7bba8bc0c9
|
fix some warnings
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
abac52e1d7
|
remove var_register_dio.h
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
89eec4cc80
|
test dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
5a72117528
|
debug dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
0027ae21e8
|
bug fixes
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
5158797233
|
refine trail iterations with lar.m_terms
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
9a9ccf19c5
|
introdure lar_term.ext_coeffs(), dio passes some tests
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
083926c658
|
debug dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
a0ece6dd2c
|
cleanup
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
ceeece6770
|
debug dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
ac5c50f179
|
fix ubuntu build in dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
c1ece49694
|
track changed columns in dio\
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
008e9229a5
|
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-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
57b665d075
|
work on incremental dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|