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 |
|
Lev Nachmanson
|
28556ce625
|
cleanup
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
862dc91cb2
|
work on incremental dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
fd3bd088a4
|
remove some warnings
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
9a96aa94e6
|
test
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
bef313f7a0
|
test
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
7ecac27335
|
fix a bug in dio
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
b0383da8f2
|
fix a bug in dio
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
7fe703e229
|
simplify column
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
8d747865ae
|
cosmetics
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
deac00ada3
|
persist dio handler
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
2c8a6f83e4
|
change int_solver to call find_cube and hnf_cut, conditionally
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
39da4f6dbd
|
remove an assert
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
28d41783b8
|
fix the build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
397fdf657d
|
fix the build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
63980f3bfd
|
fixes in dio branching
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
6bc7662580
|
passes z3test
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
174185582a
|
collect the explanation correctly
|
2025-02-11 12:23:00 -10:00 |
|
Lev Nachmanson
|
bc0fdfe158
|
remove dead code
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-11 12:23:00 -10:00 |
|