mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-16 19:06:17 +00:00
Code Activity

use same defaults as unstable branch for difference logic configuration

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
This commit is contained in:
Nikolaj Bjorner 2015-04-02 15:22:32 -07:00
parent fc36d861a7
commit dca0fb77c2
1 changed files with 0 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/smt_setup.cpp
View file

@ -362,9 +362,6 @@ namespace smt {
m_context.register_plugin(alloc(smt::theory_dense_i, m_manager, m_params)); m_context.register_plugin(alloc(smt::theory_dense_i, m_manager, m_params));
} }
else if (!m_params.m_arith_auto_config_simplex && !is_dense(st)) {
m_context.register_plugin(alloc(smt::theory_idl, m_manager, m_params));
}
else { else {
// if (st.m_arith_k_sum < rational(INT_MAX / 8)) { // if (st.m_arith_k_sum < rational(INT_MAX / 8)) {
// TRACE("setup", tout << "using small integer simplex...\n";); // TRACE("setup", tout << "using small integer simplex...\n";);
@ -416,15 +413,6 @@ namespace smt {
return; return;
} }
} }
#if 0
switch (m_params.m_arith_mode) {
case AS_DIFF_LOGIC:
case AS_DENSE_DIFF_LOGIC:
case AS_UTVPI:
setup_arith();
return;
}
#endif
m_params.m_arith_eq_bounds = true; m_params.m_arith_eq_bounds = true;
m_params.m_phase_selection = PS_ALWAYS_FALSE; m_params.m_phase_selection = PS_ALWAYS_FALSE;
m_params.m_restart_strategy = RS_GEOMETRIC; m_params.m_restart_strategy = RS_GEOMETRIC;