mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
parent
d2108ad043
commit
918846a97e
|
@ -468,6 +468,10 @@ namespace simplex {
|
|||
g.reset();
|
||||
row_iterator it = row_begin(r), end = row_end(r);
|
||||
for (; it != end && !m.is_one(g); ++it) {
|
||||
if (!m.is_int(it->m_coeff)) {
|
||||
g = numeral(1);
|
||||
break;
|
||||
}
|
||||
if (m.is_zero(g)) g = it->m_coeff;
|
||||
else m.gcd(g, it->m_coeff, g);
|
||||
}
|
||||
|
|
|
@ -52,6 +52,7 @@ namespace opt {
|
|||
if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) {
|
||||
m_params.m_relevancy_lvl = 0;
|
||||
}
|
||||
m_params.m_arith_auto_config_simplex = false;
|
||||
// m_params.m_auto_config = false;
|
||||
}
|
||||
|
||||
|
@ -65,6 +66,7 @@ namespace opt {
|
|||
m_dump_benchmarks = p.dump_benchmarks();
|
||||
m_params.updt_params(_p);
|
||||
m_context.updt_params(_p);
|
||||
m_params.m_arith_auto_config_simplex = false;
|
||||
}
|
||||
|
||||
solver* opt_solver::translate(ast_manager& m, params_ref const& p) {
|
||||
|
@ -437,6 +439,11 @@ namespace opt {
|
|||
smt::theory_dense_smi& th = dynamic_cast<smt::theory_dense_smi&>(opt);
|
||||
return th.mk_ge(m_fm, v, val);
|
||||
}
|
||||
|
||||
if (typeid(smt::theory_dense_mi) == typeid(opt)) {
|
||||
smt::theory_dense_mi& th = dynamic_cast<smt::theory_dense_mi&>(opt);
|
||||
return th.mk_ge(m_fm, v, val);
|
||||
}
|
||||
|
||||
IF_VERBOSE(0, verbose_stream() << "WARNING: unhandled theory " << typeid(opt).name() << "\n";);
|
||||
return expr_ref(m.mk_true(), m);
|
||||
|
|
|
@ -473,7 +473,7 @@ namespace sat {
|
|||
VERIFY(ENABLE_TERNARY);
|
||||
bool reinit = false;
|
||||
if (m_config.m_drat) m_drat.add(c, c.is_learned());
|
||||
TRACE("sat", tout << c << "\n";);
|
||||
TRACE("sat_verbose", tout << c << "\n";);
|
||||
SASSERT(!c.was_removed());
|
||||
m_watches[(~c[0]).index()].push_back(watched(c[1], c[2]));
|
||||
m_watches[(~c[1]).index()].push_back(watched(c[0], c[2]));
|
||||
|
|
|
@ -302,12 +302,6 @@ namespace smt {
|
|||
if (m_manager.proofs_enabled()) {
|
||||
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
|
||||
}
|
||||
else if (!m_params.m_arith_auto_config_simplex && is_dense(st)) {
|
||||
if (!st.m_has_rational && !m_params.m_model && st.arith_k_sum_is_small())
|
||||
m_context.register_plugin(alloc(smt::theory_dense_smi, m_manager, m_params));
|
||||
else
|
||||
m_context.register_plugin(alloc(smt::theory_dense_mi, m_manager, m_params));
|
||||
}
|
||||
else {
|
||||
if (m_params.m_arith_auto_config_simplex || st.m_num_uninterpreted_constants > 4 * st.m_num_bool_constants
|
||||
|| st.m_num_ite_terms > 0 /* theory_rdl and theory_frdl do not support ite-terms */) {
|
||||
|
|
Loading…
Reference in a new issue