diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index b28b44b08..02ac07cc2 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -352,10 +352,14 @@ namespace smt { else if (!m_params.m_arith_auto_config_simplex && is_dense(st)) { TRACE("setup", tout << "using dense diff logic...\n";); m_params.m_phase_selection = PS_CACHING_CONSERVATIVE; + //m_context.register_plugin(alloc(smt::theory_idl, m_manager, m_params)); +#if 1 if (st.m_arith_k_sum < rational(INT_MAX / 8)) m_context.register_plugin(alloc(smt::theory_dense_si, m_manager, m_params)); else m_context.register_plugin(alloc(smt::theory_dense_i, m_manager, m_params)); +#endif + } else { // if (st.m_arith_k_sum < rational(INT_MAX / 8)) { diff --git a/src/smt/theory_dense_diff_logic.h b/src/smt/theory_dense_diff_logic.h index 355e38c0c..db29dc988 100644 --- a/src/smt/theory_dense_diff_logic.h +++ b/src/smt/theory_dense_diff_logic.h @@ -229,6 +229,8 @@ namespace smt { virtual void flush_eh(); virtual void reset_eh(); + bool dump_lemmas() const { return m_params.m_arith_dump_lemmas; } + virtual bool validate_eq_in_model(theory_var v1, theory_var v2, bool is_true) const; virtual void display(std::ostream & out) const; diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 21f1262ac..1febe4216 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -120,6 +120,7 @@ namespace smt { if (!m_non_diff_logic_exprs) { TRACE("non_diff_logic", tout << "found non diff logic expression:\n" << mk_pp(n, get_manager()) << "\n";); get_context().push_trail(value_trail(m_non_diff_logic_exprs)); + IF_VERBOSE(0, verbose_stream() << "(smt.diff_logic: non-diff logic expression " << mk_pp(n, get_manager()) << ")\n";); m_non_diff_logic_exprs = true; } } @@ -587,6 +588,11 @@ namespace smt { context & ctx = get_context(); region & r = ctx.get_region(); ctx.set_conflict(ctx.mk_justification(theory_conflict_justification(get_id(), r, antecedents.size(), antecedents.c_ptr()))); + + if (dump_lemmas()) { + ctx.display_lemma_as_smt_problem(antecedents.size(), antecedents.c_ptr(), false_literal, ""); + } + return; } diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h index b9578657c..e09b4f91e 100644 --- a/src/smt/theory_diff_logic.h +++ b/src/smt/theory_diff_logic.h @@ -170,6 +170,9 @@ namespace smt { eq_prop_info_set m_eq_prop_info_set; // set of existing equality prop infos ptr_vector m_eq_prop_infos; + app_ref_vector m_terms; + svector m_signs; + ptr_vector m_atoms; ptr_vector m_asserted_atoms; // set of asserted atoms unsigned m_asserted_qhead; @@ -217,6 +220,7 @@ namespace smt { m_util(m), m_arith_eq_adapter(*this, params, m_util), m_zero(null_theory_var), + m_terms(m), m_asserted_qhead(0), m_num_core_conflicts(0), m_num_propagation_calls(0), @@ -323,6 +327,10 @@ namespace smt { virtual void new_diseq_eh(theory_var v1, theory_var v2, justification& j); + bool decompose_linear(app_ref_vector& args, svector& signs); + + bool is_sign(expr* n, bool& sign); + bool is_negative(app* n, app*& m); void del_atoms(unsigned old_size); diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index e7167b2cd..eaa6696fb 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -177,7 +177,6 @@ bool theory_diff_logic::internalize_atom(app * n, bool gate_ctx) { bool is_ge = m_util.is_ge(n); bool_var bv; rational kr; - app * x, *y, *z; theory_var source, target; // target - source <= k app * lhs = to_app(n->get_arg(0)); app * rhs = to_app(n->get_arg(1)); @@ -191,25 +190,26 @@ bool theory_diff_logic::internalize_atom(app * n, bool gate_ctx) { } numeral k(kr); - bool is_add = m_util.is_add(lhs) && lhs->get_num_args() == 2; - - if (is_add) { - x = to_app(lhs->get_arg(0)); - y = to_app(lhs->get_arg(1)); + m_terms.reset(); + m_signs.reset(); + m_terms.push_back(lhs); + m_signs.push_back(true); + if (!decompose_linear(m_terms, m_signs)) { + found_non_diff_logic_expr(n); + return false; } - - if (is_add && is_negative(x, z)) { - target = mk_var(y); - source = mk_var(z); - } - else if (is_add && is_negative(y, z)) { - target = mk_var(x); - source = mk_var(z); + if (m_terms.size() == 2 && m_signs[0] != m_signs[1]) { + target = mk_var(m_terms[0].get()); + source = mk_var(m_terms[1].get()); + if (!m_signs[0]) { + std::swap(target, source); + } } else { target = mk_var(lhs); source = get_zero(); } + if (is_ge) { std::swap(target, source); k.neg(); @@ -378,6 +378,70 @@ void theory_diff_logic::del_atoms(unsigned old_size) { } +template +bool theory_diff_logic::decompose_linear(app_ref_vector& terms, svector& signs) { + for (unsigned i = 0; i < terms.size(); ++i) { + app* n = terms[i].get(); + if (m_util.is_add(n)) { + expr* arg = n->get_arg(0); + if (!is_app(arg)) return false; + terms[i] = to_app(arg); + for (unsigned j = 1; j < n->get_num_args(); ++j) { + arg = n->get_arg(j); + if (!is_app(arg)) return false; + terms.push_back(to_app(arg)); + signs.push_back(signs[i]); + } + --i; + continue; + } + expr* x, *y; + bool sign; + if (m_util.is_mul(n, x, y)) { + if (is_sign(x, sign) && is_app(y)) { + terms[i] = to_app(y); + signs[i] = (signs[i] == sign); + --i; + } + else if (is_sign(y, sign) && is_app(x)) { + terms[i] = to_app(x); + signs[i] = (signs[i] == sign); + --i; + } + continue; + } + if (m_util.is_uminus(n, x) && is_app(x)) { + terms[i] = to_app(x); + signs[i] = !signs[i]; + --i; + continue; + } + } + return true; +} + +template +bool theory_diff_logic::is_sign(expr* n, bool& sign) { + rational r; + expr* x; + if (m_util.is_numeral(n, r)) { + if (r.is_one()) { + sign = true; + return true; + } + if (r.is_minus_one()) { + sign = false; + return true; + } + } + else if (m_util.is_uminus(n, x)) { + if (is_sign(x, sign)) { + sign = !sign; + return true; + } + } + return false; +} template bool theory_diff_logic::is_negative(app* n, app*& m) {