Lev Nachmanson
|
f2b05af67e
|
test
|
2025-02-03 13:33:28 -10:00 |
|
Lev Nachmanson
|
000fab630c
|
fix a bug in dio
|
2025-02-03 13:33:27 -10:00 |
|
Lev Nachmanson
|
a737483ba0
|
fix a bug in dio
|
2025-02-03 13:33:26 -10:00 |
|
Lev Nachmanson
|
c112df5d41
|
simplify column
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:26 -10:00 |
|
Lev Nachmanson
|
0958806d4a
|
cosmetics
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:26 -10:00 |
|
Lev Nachmanson
|
90dbc623fd
|
persist dio handler
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:26 -10:00 |
|
Lev Nachmanson
|
7d8e192344
|
change int_solver to call find_cube and hnf_cut, conditionally
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:26 -10:00 |
|
Lev Nachmanson
|
44d75da7a5
|
remove an assert
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:26 -10:00 |
|
Lev Nachmanson
|
28bafa301e
|
fix the build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:25 -10:00 |
|
Lev Nachmanson
|
b933a0d6e0
|
fix the build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:25 -10:00 |
|
Lev Nachmanson
|
e32ebf109b
|
fixes in dio branching
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:25 -10:00 |
|
Lev Nachmanson
|
781471aa6f
|
passes z3test
|
2025-02-03 13:33:25 -10:00 |
|
Lev Nachmanson
|
f336b0d599
|
collect the explanation correctly
|
2025-02-03 13:33:24 -10:00 |
|
Lev Nachmanson
|
ada3be2679
|
remove dead code
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:24 -10:00 |
|
Lev Nachmanson
|
6af8fbb629
|
cancel bugs fixes
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:24 -10:00 |
|
Lev Nachmanson
|
7f7dc8750f
|
solving regressions/smt2/b1.smt2
|
2025-02-03 13:33:24 -10:00 |
|
Lev Nachmanson
|
08a1ddf79f
|
work on incremental version
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:24 -10:00 |
|
Lev Nachmanson
|
b47a2687ad
|
use var_register in dioph_eq
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:23 -10:00 |
|
Lev Nachmanson
|
cdb18ac685
|
document dioph_eq
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:23 -10:00 |
|
Lev Nachmanson
|
eb0aeab2a3
|
remove a global debug variable
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:22 -10:00 |
|
Lev Nachmanson
|
b99439599b
|
remove redundant m_row_index from entry
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:22 -10:00 |
|
Lev Nachmanson
|
12ceb1ef26
|
take dependencies from open_ml
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:22 -10:00 |
|
Lev Nachmanson
|
2a81a1f043
|
fixes in tigthening
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:21 -10:00 |
|
Lev Nachmanson
|
bb77ff537b
|
check feasibility immediately after tightening a bound
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:21 -10:00 |
|
Lev Nachmanson
|
0077a689bd
|
implement explain()
|
2025-02-03 13:33:21 -10:00 |
|
Lev Nachmanson
|
1eecedf8cb
|
add missing explanations
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:20 -10:00 |
|
Lev Nachmanson
|
143f22e0a5
|
fix the build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:20 -10:00 |
|
Lev Nachmanson
|
472306c0b2
|
use fixed vars to explain tightening
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:33:20 -10:00 |
|
Lev Nachmanson
|
24aeaed50a
|
test that pivoting is correct in dioph_eq.cpp
|
2025-02-03 13:33:14 -10:00 |
|
Lev Nachmanson
|
09ec973998
|
print output file name
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:43 -10:00 |
|
Lev Nachmanson
|
594fa7423f
|
fix the build
|
2025-02-03 13:30:42 -10:00 |
|
Lev Nachmanson
|
a3b81b54db
|
init m_e_matrix on terms instead of the tableau
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-02-03 13:30:42 -10:00 |
|
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 |
|