mirror of
https://github.com/Z3Prover/z3
synced 2025-04-04 16:44:07 +00:00
testing! disable gomory cut in int_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
5e2d000369
commit
a62d664ae4
|
@ -126,6 +126,7 @@ namespace lp {
|
|||
}
|
||||
|
||||
bool all_columns_are_integral() const {
|
||||
return true; // otherwise it never returns true!
|
||||
for (lpvar j = 0; j < lra.number_of_vars(); j++)
|
||||
if (!lra.column_is_int(j))
|
||||
return false;
|
||||
|
|
|
@ -34,6 +34,7 @@ void lp::lp_settings::updt_params(params_ref const& _p) {
|
|||
m_nlsat_delay = p.arith_nl_delay();
|
||||
m_dio_eqs = p.arith_lp_dio_eqs();
|
||||
m_dio_enable_gomory_cuts = p.arith_lp_dio_cuts_enable_gomory();
|
||||
m_dio_enable_hnf_cuts = p.arith_lp_dio_cuts_enable_hnf();
|
||||
m_dio_branching_period = p.arith_lp_dio_branching_period();
|
||||
m_dump_bound_lemmas = p.arith_dump_bound_lemmas();
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue