mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

fix issues #240, #250

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-10-28 09:47:17 -07:00
parent 89b6589a37
commit 2a95a77706
1 changed files with 10 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/smt/smt_setup.cpp
View file

@ -721,22 +721,22 @@ namespace smt {
IF_VERBOSE(100, verbose_stream() << "(smt.collecting-features)\n";);
st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas());
IF_VERBOSE(1000, st.display_primitive(verbose_stream()););
m_params.m_arith_fixnum = st.arith_k_sum_is_small();
m_params.m_arith_int_only = !st.m_has_rational && !st.m_has_real;
bool fixnum = st.arith_k_sum_is_small();
bool int_only = !st.m_has_rational && !st.m_has_real;
switch(m_params.m_arith_mode) {
case AS_NO_ARITH:
m_context.register_plugin(alloc(smt::theory_dummy, m_manager.mk_family_id("arith"), "no arithmetic"));
break;
case AS_DIFF_LOGIC:
m_params.m_arith_expand_eqs = true;
if (m_params.m_arith_fixnum) {
if (m_params.m_arith_int_only)
if (fixnum) {
if (int_only)
m_context.register_plugin(alloc(smt::theory_fidl, m_manager, m_params));
else
m_context.register_plugin(alloc(smt::theory_frdl, m_manager, m_params));
}
else {
if (m_params.m_arith_int_only)
if (int_only)
m_context.register_plugin(alloc(smt::theory_idl, m_manager, m_params));
else
m_context.register_plugin(alloc(smt::theory_rdl, m_manager, m_params));
@ -744,14 +744,14 @@ namespace smt {
break;
case AS_DENSE_DIFF_LOGIC:
m_params.m_arith_expand_eqs = true;
if (m_params.m_arith_fixnum) {
if (m_params.m_arith_int_only)
if (fixnum) {
if (int_only)
m_context.register_plugin(alloc(smt::theory_dense_si, m_manager, m_params));
else
m_context.register_plugin(alloc(smt::theory_dense_smi, m_manager, m_params));
}
else {
if (m_params.m_arith_int_only)
if (int_only)
m_context.register_plugin(alloc(smt::theory_dense_i, m_manager, m_params));
else
m_context.register_plugin(alloc(smt::theory_dense_mi, m_manager, m_params));
@ -759,7 +759,7 @@ namespace smt {
break;
case AS_UTVPI:
m_params.m_arith_expand_eqs = true;
if (m_params.m_arith_int_only)
if (int_only)
m_context.register_plugin(alloc(smt::theory_iutvpi, m_manager));
else
m_context.register_plugin(alloc(smt::theory_rutvpi, m_manager));
@ -768,7 +768,7 @@ namespace smt {
m_context.register_plugin(alloc(smt::theory_inf_arith, m_manager, m_params));
break;
default:
if (m_params.m_arith_int_only)
if (m_params.m_arith_int_only && int_only)
m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
else
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));