Lev Nachmanson
|
2bda4d1674
|
throttle dioph equalities
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:42 -10:00 |
|
Lev Nachmanson
|
727ac149a7
|
change type of m_e_matrix
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:42 -10:00 |
|
Lev Nachmanson
|
282edcfadf
|
add a template instantiotion
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:42 -10:00 |
|
Lev Nachmanson
|
4710260ede
|
handle empty rows in m_e_matrix
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:42 -10:00 |
|
Lev Nachmanson
|
b0be4d58c7
|
vector access bugs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:42 -10:00 |
|
Lev Nachmanson
|
f5f4c848ec
|
bug fixes with tableau
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:42 -10:00 |
|
Lev Nachmanson
|
9c2ec9b47d
|
bug fixes
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:42 -10:00 |
|
Lev Nachmanson
|
9434847ce7
|
bug fixes
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:42 -10:00 |
|
Lev Nachmanson
|
bc2c67c7ea
|
debug dio with static matrix
|
2025-02-03 13:30:42 -10:00 |
|
Lev Nachmanson
|
df577eecd6
|
unifying vectors into eprime_entry
|
2025-02-03 13:30:42 -10:00 |
|
Lev Nachmanson
|
f3b33888ab
|
dio with static_matrix initial setup
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:41 -10:00 |
|
Lev Nachmanson
|
60a38cdd22
|
do not use conflicts with fresh vars to create branches
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:41 -10:00 |
|
Lev Nachmanson
|
dc15dbfc31
|
remove disabling return
|
2025-02-03 13:30:41 -10:00 |
|
Lev Nachmanson
|
5f0077626e
|
remove more warnings
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:41 -10:00 |
|
Lev Nachmanson
|
fdae46fb60
|
remove a warning
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:41 -10:00 |
|
Lev Nachmanson
|
2c7c708848
|
fix ubuntu's build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:41 -10:00 |
|
Lev Nachmanson
|
fa907c5e8c
|
prepare using fresh vars in cuts
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:41 -10:00 |
|
Lev Nachmanson
|
110593f086
|
use cuts from proofs, remove gcc warnings
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:41 -10:00 |
|
Lev Nachmanson
|
4e381609db
|
enable cuts from proofs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:41 -10:00 |
|
Lev Nachmanson
|
c30600c2ef
|
fixes in dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:41 -10:00 |
|
Lev Nachmanson
|
5f70eb0524
|
do not eliminate fresh variables when tightening
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:41 -10:00 |
|
Lev Nachmanson
|
1769c6059e
|
fixed dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:41 -10:00 |
|
Lev Nachmanson
|
2ca7b31d13
|
comment out global_max_change
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:40 -10:00 |
|
Lev Nachmanson
|
f05d1abccc
|
debug dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:40 -10:00 |
|
Lev Nachmanson
|
8d8ee99db3
|
test tightening with S
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:40 -10:00 |
|
Lev Nachmanson
|
7d8212646d
|
handle sat with tightening
|
2025-02-03 13:30:40 -10:00 |
|
Lev Nachmanson
|
9118abebc7
|
cosmetics
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:40 -10:00 |
|
Lev Nachmanson
|
e0185121c5
|
use u_dependency in eprime_pair
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:40 -10:00 |
|
Lev Nachmanson
|
b20566a488
|
work on tighten_with_S
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:40 -10:00 |
|
Lev Nachmanson
|
a1a9825e43
|
remove a throw
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:40 -10:00 |
|
Lev Nachmanson
|
a75eff6525
|
bug fix
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:40 -10:00 |
|
Lev Nachmanson
|
0c6dcfedb8
|
small optimization
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:40 -10:00 |
|
Lev Nachmanson
|
9ec55de5c6
|
optimize dio changes
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:40 -10:00 |
|
Lev Nachmanson
|
7c9cb44c94
|
less eager dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:40 -10:00 |
|
Lev Nachmanson
|
4fea4259ec
|
fix the build
|
2025-02-03 13:30:40 -10:00 |
|
Lev Nachmanson
|
1a99fa56cb
|
handle zero rows correctly
|
2025-02-03 13:30:40 -10:00 |
|
Lev Nachmanson
|
178411ad0c
|
dio passes regression\smt2 tests with limited functionality
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:39 -10:00 |
|
Lev Nachmanson
|
dcd80ac95b
|
fix term_o init
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:39 -10:00 |
|
Lev Nachmanson
|
c29d04dc3c
|
debug dio
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:39 -10:00 |
|
Lev Nachmanson
|
1cb71b4648
|
debug dio
|
2025-02-03 13:30:39 -10:00 |
|
Lev Nachmanson
|
db899fd670
|
fix in substitution of fresh variables, clean column.h
|
2025-02-03 13:30:39 -10:00 |
|
Lev Nachmanson
|
5f71604198
|
bug fix in init and getting explanations
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:39 -10:00 |
|
Lev Nachmanson
|
0814fa40b0
|
create a conflict explanation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:39 -10:00 |
|
Lev Nachmanson
|
53605d4e0a
|
a version with less pointers: got a conflict
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:00 -10:00 |
|
Lev Nachmanson
|
876cbc527d
|
in the middle
|
2025-02-03 13:24:33 -10:00 |
|
Lev Nachmanson
|
778db5e763
|
use std::list
|
2025-02-03 13:24:33 -10:00 |
|
Lev Nachmanson
|
c1e577e932
|
fix the crash
|
2025-02-03 13:24:33 -10:00 |
|
Lev Nachmanson
|
484af98af6
|
crash
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:24:33 -10:00 |
|
Lev Nachmanson
|
0eeef3b806
|
fix the build
|
2025-02-03 13:24:33 -10:00 |
|
Lev Nachmanson
|
0b9b1c4472
|
move some functionality from int_solver to int_solver::imp
|
2025-02-03 13:24:33 -10:00 |
|