From ed19af4c4e7fc2d4387650c7c0087ccbfa5a7d63 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 Sep 2018 09:02:37 -0700 Subject: [PATCH 01/22] merge Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 1 + src/util/lp/gomory.cpp | 4 +++- src/util/lp/lp_core_solver_base.h | 6 +++--- 3 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index fd2dc0da2..f096d1dd5 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1629,6 +1629,7 @@ public: expr_ref term2expr(lp::lar_term const& term) { expr_ref t(m); expr_ref_vector ts(m); + ts.push_back(a.mk_numeral(term.m_v, true)); for (auto const& p : term) { lp::var_index wi = p.var(); if (m_solver->is_term(wi)) { diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp index 55098dccf..9974eda7f 100644 --- a/src/util/lp/gomory.cpp +++ b/src/util/lp/gomory.cpp @@ -168,11 +168,13 @@ public: mpq one_min_f0 = 1 - f0; for (const auto & p : m_row) { unsigned j = p.var(); +#if 1 if (column_is_fixed(j)) { m_ex.push_justification(column_lower_bound_constraint(j)); m_ex.push_justification(column_upper_bound_constraint(j)); continue; } +#endif if (j == m_inf_col) { lp_assert(p.coeff() == one_of_type()); TRACE("gomory_cut_detail", tout << "seeing basic var";); @@ -194,7 +196,7 @@ public: adjust_term_and_k_for_some_ints_case_gomory(lcm_den); lp_assert(m_int_solver.current_solution_is_inf_on_cut()); m_int_solver.m_lar_solver->subs_term_columns(m_t, m_k); - TRACE("gomory_cut", tout<<"gomory cut:"; m_int_solver.m_lar_solver->print_term(m_t, tout); tout << " <= " << m_k << std::endl;); + TRACE("gomory_cut", tout<<"gomory cut:"; m_int_solver.m_lar_solver->print_term(m_t, tout) << " <= " << m_k << std::endl;); return lia_move::cut; } imp(lar_term & t, mpq & k, explanation& ex, unsigned basic_inf_int_j, const row_strip& row, const int_solver& int_slv ) : diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h index 41b6fe31d..9a6549917 100644 --- a/src/util/lp/lp_core_solver_base.h +++ b/src/util/lp/lp_core_solver_base.h @@ -577,7 +577,7 @@ public: } void print_column_info(unsigned j, std::ostream & out) const { - out << "j = " << j << ", name = "<< column_name(j); + out << "j = " << j << ",\tname = "<< column_name(j) << "\t"; switch (m_column_types[j]) { case column_type::fixed: case column_type::boxed: @@ -596,11 +596,11 @@ public: lp_assert(false); } // out << "basis heading = " << m_basis_heading[j] << std::endl; - out << " x = " << m_x[j]; + out << "\tx = " << m_x[j]; if (m_basis_heading[j] >= 0) out << " base\n"; else - out << " nbas\n"; + out << " \n"; } bool column_is_free(unsigned j) const { return this->m_column_type[j] == free; } From dcda39e76e68fd2264e681c42fb3ae25e10e3ade Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 Sep 2018 17:12:32 -0700 Subject: [PATCH 02/22] merge Signed-off-by: Nikolaj Bjorner --- src/util/lp/gomory.cpp | 15 ++++++++++++--- src/util/lp/lar_solver.h | 4 +--- 2 files changed, 13 insertions(+), 6 deletions(-) diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp index 2dd349354..2136f5f3e 100644 --- a/src/util/lp/gomory.cpp +++ b/src/util/lp/gomory.cpp @@ -197,12 +197,21 @@ class gomory::imp { out << "(assert ( = ( +"; dump_row_coefficients(out) << ") 0))\n"; } + + void dump_declaration(std::ostream& out, unsigned v) const { + out << "(declare-const " << var_name(v) << (is_int(v) ? " Int" : " Real") << ")\n"; + } void dump_declarations(std::ostream& out) const { // for a column j the var name is vj for (const auto & p : m_row) { - out << "(declare-const " << var_name(p.var()) - << (is_int(p.var())? " Int" : " Real") << ")\n"; + dump_declaration(out, p.var()); + } + for (const auto& p : m_t) { + unsigned v = p.var(); + if (m_int_solver.m_lar_solver->is_term(v)) { + dump_declaration(out, v); + } } } @@ -298,7 +307,7 @@ public: lp_assert(m_int_solver.current_solution_is_inf_on_cut()); TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);); m_int_solver.m_lar_solver->subs_term_columns(m_t, m_k); - // TBD: validate result of subs_term_columns + TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);); TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t, tout << "gomory cut:"); tout << " <= " << m_k << std::endl;); return lia_move::cut; } diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 3c0ed4fbf..9e9edacc8 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -239,8 +239,7 @@ public: void analyze_new_bounds_on_row_tableau( unsigned row_index, - bound_propagator & bp - ); + bound_propagator & bp); void substitute_basis_var_in_terms_for_row(unsigned i); @@ -549,7 +548,6 @@ public: mpq v = it->second; t.m_coeffs.erase(it); t.m_coeffs[p.second] = v; - if (lt.m_v.is_zero()) continue; rs -= v * lt.m_v; } } From d75b6fd9c1536b9c8f98392ad292be7859e0ce63 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 20 Sep 2018 11:06:05 -0700 Subject: [PATCH 03/22] remove offsets from terms Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 128 +++++++++++++++++++------------ src/util/lp/bound_propagator.cpp | 4 - src/util/lp/gomory.cpp | 16 ++-- src/util/lp/int_solver.cpp | 51 ++++++------ src/util/lp/int_solver.h | 16 ++-- src/util/lp/lar_constraints.h | 2 +- src/util/lp/lar_solver.cpp | 69 ++++++----------- src/util/lp/lar_solver.h | 14 ++-- src/util/lp/lar_term.h | 12 ++- 9 files changed, 159 insertions(+), 153 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index f096d1dd5..ca59a2c27 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -55,7 +55,7 @@ std::ostream& operator<<(std::ostream& out, bound_kind const& k) { } class bound { - smt::bool_var m_bv; + smt::bool_var m_bv; smt::theory_var m_var; bool m_is_int; rational m_value; @@ -165,13 +165,13 @@ class theory_lra::imp { expr_ref_vector m_terms; vector m_coeffs; svector m_vars; - rational m_coeff; + rational m_offset; ptr_vector m_terms_to_internalize; internalize_state(ast_manager& m): m_terms(m) {} void reset() { m_terms.reset(); m_coeffs.reset(); - m_coeff.reset(); + m_offset.reset(); m_vars.reset(); m_terms_to_internalize.reset(); } @@ -197,7 +197,7 @@ class theory_lra::imp { expr_ref_vector& terms() { return m_st.m_terms; } vector& coeffs() { return m_st.m_coeffs; } svector& vars() { return m_st.m_vars; } - rational& coeff() { return m_st.m_coeff; } + rational& offset() { return m_st.m_offset; } ptr_vector& terms_to_internalize() { return m_st.m_terms_to_internalize; } void push(expr* e, rational c) { m_st.m_terms.push_back(e); m_st.m_coeffs.push_back(c); } void set_back(unsigned i) { @@ -216,6 +216,8 @@ class theory_lra::imp { svector m_term_index2theory_var; // reverse map from lp_solver variables to theory variables var_coeffs m_left_side; // constraint left side mutable std::unordered_map m_variable_values; // current model + lp::var_index m_one_var; + lp::var_index m_zero_var; enum constraint_source { inequality_source, @@ -331,6 +333,32 @@ class theory_lra::imp { } } + void add_const(int c, lp::var_index& var) { + if (var != UINT_MAX) { + return; + } + app_ref cnst(a.mk_int(c), m); + TRACE("arith", tout << "add " << cnst << "\n";); + enode* e = mk_enode(cnst); + theory_var v = mk_var(cnst); + var = m_solver->add_var(v, true); + m_theory_var2var_index.setx(v, var, UINT_MAX); + m_var_index2theory_var.setx(var, v, UINT_MAX); + m_var_trail.push_back(v); + add_def_constraint(m_solver->add_var_bound(var, lp::GE, rational(c))); + add_def_constraint(m_solver->add_var_bound(var, lp::LE, rational(c))); + } + + lp::var_index get_one() { + add_const(1, m_one_var); + return m_one_var; + } + + lp::var_index get_zero() { + add_const(0, m_zero_var); + return m_zero_var; + } + void found_not_handled(expr* n) { m_not_handled = n; @@ -375,7 +403,7 @@ class theory_lra::imp { expr_ref_vector & terms = st.terms(); svector& vars = st.vars(); vector& coeffs = st.coeffs(); - rational& coeff = st.coeff(); + rational& offset = st.offset(); rational r; expr* n1, *n2; unsigned index = 0; @@ -415,7 +443,7 @@ class theory_lra::imp { ++index; } else if (a.is_numeral(n, r)) { - coeff += coeffs[index]*r; + offset += coeffs[index]*r; ++index; } else if (a.is_uminus(n, n1)) { @@ -427,7 +455,6 @@ class theory_lra::imp { app* t = to_app(n); internalize_args(t); mk_enode(t); - theory_var v = mk_var(n); coeffs[vars.size()] = coeffs[index]; vars.push_back(v); @@ -738,7 +765,15 @@ class theory_lra::imp { } bool is_unit_var(scoped_internalize_state& st) { - return st.coeff().is_zero() && st.vars().size() == 1 && st.coeffs()[0].is_one(); + return st.offset().is_zero() && st.vars().size() == 1 && st.coeffs()[0].is_one(); + } + + bool is_one(scoped_internalize_state& st) { + return st.offset().is_one() && st.vars().empty(); + } + + bool is_zero(scoped_internalize_state& st) { + return st.offset().is_zero() && st.vars().empty(); } theory_var internalize_def(app* term, scoped_internalize_state& st) { @@ -771,13 +806,24 @@ class theory_lra::imp { if (is_unit_var(st)) { return st.vars()[0]; } + else if (is_one(st)) { + return get_one(); + } + else if (is_zero(st)) { + return get_zero(); + } else { init_left_side(st); theory_var v = mk_var(term); lp::var_index vi = m_theory_var2var_index.get(v, UINT_MAX); - TRACE("arith", tout << mk_pp(term, m) << " " << v << " " << vi << "\n";); + TRACE("arith", tout << mk_pp(term, m) << " v" << v << "\n";); if (vi == UINT_MAX) { - vi = m_solver->add_term(m_left_side, st.coeff()); + rational const& offset = st.offset(); + if (!offset.is_zero()) { + m_left_side.push_back(std::make_pair(offset, get_one())); + } + SASSERT(!m_left_side.empty()); + vi = m_solver->add_term(m_left_side); m_theory_var2var_index.setx(v, vi, UINT_MAX); if (m_solver->is_term(vi)) { m_term_index2theory_var.setx(m_solver->adjust_term_index(vi), v, UINT_MAX); @@ -806,6 +852,8 @@ public: m_has_int(false), m_arith_eq_adapter(th, ap, a), m_internalize_head(0), + m_one_var(UINT_MAX), + m_zero_var(UINT_MAX), m_not_handled(nullptr), m_asserted_qhead(0), m_assume_eq_head(0), @@ -879,7 +927,7 @@ public: } void internalize_eq_eh(app * atom, bool_var) { - expr* lhs = 0, *rhs = 0; + expr* lhs = nullptr, *rhs = nullptr; VERIFY(m.is_eq(atom, lhs, rhs)); enode * n1 = get_enode(lhs); enode * n2 = get_enode(rhs); @@ -1197,7 +1245,6 @@ public: m_todo_terms.pop_back(); if (m_solver->is_term(vi)) { const lp::lar_term& term = m_solver->get_term(vi); - result += term.m_v * coeff; for (const auto & i: term) { m_todo_terms.push_back(std::make_pair(i.var(), coeff * i.coeff())); } @@ -1234,7 +1281,6 @@ public: m_todo_terms.pop_back(); if (m_solver->is_term(wi)) { const lp::lar_term& term = m_solver->get_term(wi); - result += term.m_v * coeff; for (const auto & i : term) { if (m_variable_values.count(i.var()) > 0) { result += m_variable_values[i.var()] * coeff * i.coeff(); @@ -1481,8 +1527,8 @@ public: bool all_bounded = true; for (unsigned v = 0; v < nv; ++v) { lp::var_index vi = m_theory_var2var_index[v]; - if (vi == UINT_MAX) - continue; + if (vi == UINT_MAX) + continue; if (!m_solver->is_term(vi) && !var_has_bound(vi, true) && !var_has_bound(vi, false)) { lp::lar_term term; term.add_monomial(rational::one(), vi); @@ -1516,23 +1562,10 @@ public: theory_var v = mk_var(n); theory_var v1 = mk_var(p); theory_var v2 = mk_var(q); - rational r = get_value(v); rational r1 = get_value(v1); - rational r2 = get_value(v2); - rational r3; - if (r2.is_zero()) { - continue; - } - if (r1.is_int() && r2.is_int() && r == div(r1, r2)) { - continue; - } - if (r2.is_neg() || r1.is_neg()) { - // TBD - continue; - } + rational r2; - if (!r1.is_int() || !r2.is_int()) { - // std::cout << r1 << " " << r2 << " " << r << " " << expr_ref(n, m) << "\n"; + if (!r1.is_int() || r1.is_neg()) { // TBD // r1 = 223/4, r2 = 2, r = 219/8 // take ceil(r1), floor(r1), ceil(r2), floor(r2), for floor(r2) > 0 @@ -1542,16 +1575,18 @@ public: continue; } - if (a.is_numeral(q, r3)) { + if (a.is_numeral(q, r2) && r2.is_pos()) { + if (get_value(v) == div(r1, r2)) continue; - SASSERT(r3 == r2 && r2.is_int()); - SASSERT(r1.is_int() && r3.is_int()); rational div_r = div(r1, r2); // p <= q * div(r1, q) + q - 1 => div(p, q) <= div(r1, r2) // p >= q * div(r1, q) => div(r1, q) <= div(p, q) rational mul(1); rational hi = r2 * div_r + r2 - 1; rational lo = r2 * div_r; + + // used to normalize inequalities so they + // don't appear as 8*x >= 15, but x >= 2 expr *n1 = nullptr, *n2 = nullptr; if (a.is_mul(p, n1, n2) && is_numeral(n1, mul) && mul.is_pos()) { p = n2; @@ -1568,7 +1603,7 @@ public: all_divs_valid = false; TRACE("arith", - tout << r1 << " div " << r2 << " = " << r3 << "\n"; + tout << r1 << " div " << r2 << "\n"; literal_vector lits; lits.push_back(~p_le_r1); lits.push_back(n_le_div); @@ -1578,8 +1613,10 @@ public: ctx().display_literals_verbose(tout, lits) << "\n";); continue; } +#if 0 - + // TBD similar for non-linear division. + // better to deal with in nla_solver: all_divs_valid = false; @@ -1610,6 +1647,7 @@ public: lits[0] = pq_rhs; lits[1] = n_ge_div; ctx().display_literals_verbose(tout, lits) << "\n";); +#endif } return all_divs_valid; @@ -1629,7 +1667,6 @@ public: expr_ref term2expr(lp::lar_term const& term) { expr_ref t(m); expr_ref_vector ts(m); - ts.push_back(a.mk_numeral(term.m_v, true)); for (auto const& p : term) { lp::var_index wi = p.var(); if (m_solver->is_term(wi)) { @@ -1709,17 +1746,13 @@ public: TRACE("arith", tout << "idiv bounds check\n";); return l_false; } - lp::lar_term term; - lp::mpq k; - lp::explanation ex; // TBD, this should be streamlined accross different explanations - bool upper; m_explanation.reset(); - switch(m_lia->check(term, k, ex, upper)) { + switch (m_lia->check()) { case lp::lia_move::sat: return l_true; case lp::lia_move::branch: { TRACE("arith", tout << "branch\n";); - app_ref b = mk_bound(term, k, !upper); + app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper()); IF_VERBOSE(2, verbose_stream() << "branch " << b << "\n";); // branch on term >= k + 1 // branch on term <= k @@ -1732,13 +1765,13 @@ public: TRACE("arith", tout << "cut\n";); ++m_stats.m_gomory_cuts; // m_explanation implies term <= k - app_ref b = mk_bound(term, k, !upper); + app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper()); IF_VERBOSE(2, verbose_stream() << "cut " << b << "\n"); - TRACE("arith", dump_cut_lemma(tout, term, k, ex, upper);); + TRACE("arith", dump_cut_lemma(tout, m_lia->get_term(), m_lia->get_offset(), m_lia->get_explanation(), m_lia->is_upper());); m_eqs.reset(); m_core.reset(); m_params.reset(); - for (auto const& ev : ex.m_explanation) { + for (auto const& ev : m_lia->get_explanation().m_explanation) { if (!ev.first.is_zero()) { set_evidence(ev.second); } @@ -1753,7 +1786,7 @@ public: case lp::lia_move::conflict: TRACE("arith", tout << "conflict\n";); // ex contains unsat core - m_explanation = ex.m_explanation; + m_explanation = m_lia->get_explanation().m_explanation; set_conflict1(); return l_false; case lp::lia_move::undef: @@ -2922,7 +2955,7 @@ public: lp::lar_term const& term = m_solver->get_term(vi); TRACE("arith", m_solver->print_term(term, tout) << "\n";); scoped_anum r1(m_nra->am()); - rational c1 = term.m_v * wcoeff; + rational c1(0); m_nra->am().set(r1, c1.to_mpq()); m_nra->am().add(r, r1, r); for (auto const & arg : term) { @@ -3197,7 +3230,6 @@ public: coeffs.find(w, c0); coeffs.insert(w, c0 + ti.coeff() * coeff); } - offset += coeff * term.m_v; } app_ref coeffs2app(u_map const& coeffs, rational const& offset, bool is_int) { diff --git a/src/util/lp/bound_propagator.cpp b/src/util/lp/bound_propagator.cpp index c4fa2aefa..a5c7c976a 100644 --- a/src/util/lp/bound_propagator.cpp +++ b/src/util/lp/bound_propagator.cpp @@ -17,10 +17,6 @@ const impq & bound_propagator::get_upper_bound(unsigned j) const { } void bound_propagator::try_add_bound(mpq v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) { j = m_lar_solver.adjust_column_index_to_term_index(j); - if (m_lar_solver.is_term(j)) { - // lp treats terms as not having a free coefficient, restoring it below for the outside consumption - v += m_lar_solver.get_term(j).m_v; - } lconstraint_kind kind = is_low? GE : LE; if (strict) diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp index 2136f5f3e..96b3ab395 100644 --- a/src/util/lp/gomory.cpp +++ b/src/util/lp/gomory.cpp @@ -45,7 +45,7 @@ class gomory::imp { void int_case_in_gomory_cut(const mpq & a, unsigned j, mpq & lcm_den, const mpq& f0, const mpq& one_minus_f0) { lp_assert(is_int(j) && !a.is_int()); - mpq fj = fractional_part(a); + mpq fj = fractional_part(a); TRACE("gomory_cut_detail", tout << a << " j=" << j << " k = " << m_k; tout << ", fj: " << fj << ", "; @@ -56,10 +56,9 @@ class gomory::imp { mpq new_a; if (at_lower(j)) { new_a = fj <= one_minus_f0 ? fj / one_minus_f0 : ((1 - fj) / f0); - m_k.addmul(new_a, lower_bound(j).x); - // m_k += (new_a * lower_bound(j).x); lp_assert(new_a.is_pos()); - m_ex.push_justification(column_lower_bound_constraint(j), new_a); + m_k.addmul(new_a, lower_bound(j).x); + m_ex.push_justification(column_lower_bound_constraint(j), new_a); } else { lp_assert(at_upper(j)); @@ -67,7 +66,6 @@ class gomory::imp { new_a = - (fj <= f0 ? fj / f0 : ((1 - fj) / one_minus_f0)); lp_assert(new_a.is_neg()); m_k.addmul(new_a, upper_bound(j).x); - // m_k += (new_a * upper_bound(j).x); m_ex.push_justification(column_upper_bound_constraint(j), new_a); } m_t.add_monomial(new_a, j); @@ -251,9 +249,12 @@ class gomory::imp { std::ostream& dump_term_le_k(std::ostream & out) const { return dump_term_sum(out << "(<= ") << " " << m_k << ")"; } + void dump_the_cut_assert(std::ostream & out) const { dump_term_le_k(out << "(assert (not ") << "))\n"; } + + void dump_cut_and_constraints_as_smt_lemma(std::ostream& out) const { dump_declarations(out); dump_the_row(out); @@ -284,7 +285,6 @@ public: mpq one_min_f0 = 1 - f0; for (const auto & p : m_row) { unsigned j = p.var(); - if (j == m_inf_col) { lp_assert(p.coeff() == one_of_type()); TRACE("gomory_cut_detail", tout << "seeing basic var";); @@ -306,11 +306,11 @@ public: adjust_term_and_k_for_some_ints_case_gomory(lcm_den); lp_assert(m_int_solver.current_solution_is_inf_on_cut()); TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);); - m_int_solver.m_lar_solver->subs_term_columns(m_t, m_k); - TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);); + m_int_solver.m_lar_solver->subs_term_columns(m_t); TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t, tout << "gomory cut:"); tout << " <= " << m_k << std::endl;); return lia_move::cut; } + imp(lar_term & t, mpq & k, explanation& ex, unsigned basic_inf_int_j, const row_strip& row, const int_solver& int_slv ) : m_t(t), m_k(k), diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp index cd3a88669..83fbe3961 100644 --- a/src/util/lp/int_solver.cpp +++ b/src/util/lp/int_solver.cpp @@ -125,19 +125,19 @@ constraint_index int_solver::column_lower_bound_constraint(unsigned j) const { bool int_solver::current_solution_is_inf_on_cut() const { const auto & x = m_lar_solver->m_mpq_lar_core_solver.m_r_x; - impq v = m_t->apply(x); - mpq sign = *m_upper ? one_of_type() : -one_of_type(); - CTRACE("current_solution_is_inf_on_cut", v * sign <= (*m_k) * sign, - tout << "m_upper = " << *m_upper << std::endl; - tout << "v = " << v << ", k = " << (*m_k) << std::endl; + impq v = m_t.apply(x); + mpq sign = m_upper ? one_of_type() : -one_of_type(); + CTRACE("current_solution_is_inf_on_cut", v * sign <= m_k * sign, + tout << "m_upper = " << m_upper << std::endl; + tout << "v = " << v << ", k = " << m_k << std::endl; ); - return v * sign > (*m_k) * sign; + return v * sign > m_k * sign; } lia_move int_solver::mk_gomory_cut( unsigned inf_col, const row_strip & row) { lp_assert(column_is_int_inf(inf_col)); - gomory gc(*m_t, *m_k, *m_ex, inf_col, row, *this); + gomory gc(m_t, m_k, m_ex, inf_col, row, *this); return gc.create_cut(); } @@ -147,7 +147,7 @@ lia_move int_solver::proceed_with_gomory_cut(unsigned j) { if (!is_gomory_cut_target(row)) return create_branch_on_column(j); - *m_upper = true; + m_upper = true; return mk_gomory_cut(j, row); } @@ -373,21 +373,21 @@ lia_move int_solver::make_hnf_cut() { #else vector x0; #endif - lia_move r = m_hnf_cutter.create_cut(*m_t, *m_k, *m_ex, *m_upper, x0); + lia_move r = m_hnf_cutter.create_cut(m_t, m_k, m_ex, m_upper, x0); if (r == lia_move::cut) { TRACE("hnf_cut", - m_lar_solver->print_term(*m_t, tout << "cut:"); - tout << " <= " << *m_k << std::endl; + m_lar_solver->print_term(m_t, tout << "cut:"); + tout << " <= " << m_k << std::endl; for (unsigned i : m_hnf_cutter.constraints_for_explanation()) { m_lar_solver->print_constraint(i, tout); } ); lp_assert(current_solution_is_inf_on_cut()); settings().st().m_hnf_cuts++; - m_ex->clear(); + m_ex.clear(); for (unsigned i : m_hnf_cutter.constraints_for_explanation()) { - m_ex->push_justification(i); + m_ex.push_justification(i); } } return r; @@ -403,10 +403,13 @@ lia_move int_solver::hnf_cut() { return lia_move::undef; } -lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex, bool & upper) { +lia_move int_solver::check() { if (!has_inf_int()) return lia_move::sat; - m_t = &t; m_k = &k; m_ex = &ex; m_upper = &upper; + m_t.clear(); + m_k.reset(); + m_ex.clear(); + m_upper = false; lia_move r = run_gcd_test(); if (r != lia_move::undef) return r; @@ -646,8 +649,8 @@ bool int_solver::gcd_test_for_row(static_matrix> & A, uns void int_solver::add_to_explanation_from_fixed_or_boxed_column(unsigned j) { constraint_index lc, uc; m_lar_solver->get_bound_constraint_witnesses_for_column(j, lc, uc); - m_ex->m_explanation.push_back(std::make_pair(mpq(1), lc)); - m_ex->m_explanation.push_back(std::make_pair(mpq(1), uc)); + m_ex.m_explanation.push_back(std::make_pair(mpq(1), lc)); + m_ex.m_explanation.push_back(std::make_pair(mpq(1), uc)); } void int_solver::fill_explanation_from_fixed_columns(const row_strip & row) { for (const auto & c : row) { @@ -1042,20 +1045,20 @@ const impq& int_solver::lower_bound(unsigned j) const { lia_move int_solver::create_branch_on_column(int j) { TRACE("check_main_int", tout << "branching" << std::endl;); - lp_assert(m_t->is_empty()); + lp_assert(m_t.is_empty()); lp_assert(j != -1); - m_t->add_monomial(mpq(1), m_lar_solver->adjust_column_index_to_term_index(j)); + m_t.add_monomial(mpq(1), m_lar_solver->adjust_column_index_to_term_index(j)); if (is_free(j)) { - *m_upper = true; - *m_k = mpq(0); + m_upper = true; + m_k = mpq(0); } else { - *m_upper = left_branch_is_more_narrow_than_right(j); - *m_k = *m_upper? floor(get_value(j)) : ceil(get_value(j)); + m_upper = left_branch_is_more_narrow_than_right(j); + m_k = m_upper? floor(get_value(j)) : ceil(get_value(j)); } TRACE("arith_int", tout << "branching v" << j << " = " << get_value(j) << "\n"; display_column(tout, j); - tout << "k = " << *m_k << std::endl; + tout << "k = " << m_k << std::endl; ); return lia_move::branch; diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h index 013f53ce0..17ce20481 100644 --- a/src/util/lp/int_solver.h +++ b/src/util/lp/int_solver.h @@ -39,19 +39,23 @@ public: // fields lar_solver *m_lar_solver; unsigned m_number_of_calls; - lar_term *m_t; // the term to return in the cut - mpq *m_k; // the right side of the cut - explanation *m_ex; // the conflict explanation - bool *m_upper; // we have a cut m_t*x <= k if m_upper is true nad m_t*x >= k otherwise + lar_term m_t; // the term to return in the cut + mpq m_k; // the right side of the cut + explanation m_ex; // the conflict explanation + bool m_upper; // we have a cut m_t*x <= k if m_upper is true nad m_t*x >= k otherwise hnf_cutter m_hnf_cutter; // methods int_solver(lar_solver* lp); // main function to check that the solution provided by lar_solver is valid for integral values, // or provide a way of how it can be adjusted. - lia_move check(lar_term& t, mpq& k, explanation& ex, bool & upper); + lia_move check(); + lar_term const& get_term() const { return m_t; } + mpq const& get_offset() const { return m_k; } + explanation const& get_explanation() const { return m_ex; } + bool is_upper() const { return m_upper; } + bool move_non_basic_column_to_bounds(unsigned j); - lia_move check_wrapper(lar_term& t, mpq& k, explanation& ex); bool is_base(unsigned j) const; bool is_real(unsigned j) const; const impq & lower_bound(unsigned j) const; diff --git a/src/util/lp/lar_constraints.h b/src/util/lp/lar_constraints.h index ac15028bb..6305089b4 100644 --- a/src/util/lp/lar_constraints.h +++ b/src/util/lp/lar_constraints.h @@ -75,7 +75,7 @@ struct lar_term_constraint: public lar_base_constraint { } unsigned size() const override { return m_term->size();} lar_term_constraint(const lar_term *t, lconstraint_kind kind, const mpq& right_side) : lar_base_constraint(kind, right_side), m_term(t) { } - mpq get_free_coeff_of_left_side() const override { return m_term->m_v;} + // mpq get_free_coeff_of_left_side() const override { return m_term->m_v;} }; diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 56a61177c..30494aa1c 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -137,7 +137,7 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be, kind = static_cast(-kind); } rs_of_evidence /= ratio; - rs_of_evidence += t->m_v * ratio; + // rs_of_evidence += t->m_v * ratio; } return kind == be.kind() && rs_of_evidence == be.m_bound; @@ -602,7 +602,7 @@ void lar_solver::register_monoid_in_map(std::unordered_map & coe void lar_solver::substitute_terms_in_linear_expression(const vector>& left_side_with_terms, - vector> &left_side, mpq & free_coeff) const { + vector> &left_side) const { std::unordered_map coeffs; for (auto & t : left_side_with_terms) { unsigned j = t.second; @@ -613,7 +613,6 @@ void lar_solver::substitute_terms_in_linear_expression(const vector= constr.m_right_side; - case GT: return left_side_val > constr.m_right_side; + case GT: return left_side_val > constr.m_right_side; case EQ: return left_side_val == constr.m_right_side; default: lp_unreachable(); @@ -976,8 +975,10 @@ bool lar_solver::the_relations_are_of_same_type(const vectorm_kind); if (kind == GT || kind == LT) strict = true; - if (kind == GE || kind == GT) n_of_G++; - else if (kind == LE || kind == LT) n_of_L++; + if (kind == GE || kind == GT) + n_of_G++; + else if (kind == LE || kind == LT) + n_of_L++; } the_kind_of_sum = n_of_G ? GE : (n_of_L ? LE : EQ); if (strict) @@ -1117,7 +1118,7 @@ bool lar_solver::has_upper_bound(var_index var, constraint_index& ci, mpq& value bool lar_solver::has_value(var_index var, mpq& value) const { if (is_term(var)) { lar_term const& t = get_term(var); - value = t.m_v; + value = 0; for (auto const& cv : t) { impq const& r = get_column_value(cv.var()); if (!numeric_traits::is_zero(r.y)) return false; @@ -1229,8 +1230,7 @@ std::ostream& lar_solver::print_constraints(std::ostream& out) const { std::ostream& lar_solver::print_terms(std::ostream& out) const { for (auto it : m_terms) { - print_term(*it, out); - out << "\n"; + print_term(*it, out) << "\n"; } return out; } @@ -1244,9 +1244,6 @@ std::ostream& lar_solver::print_left_side_of_constraint(const lar_base_constrain } std::ostream& lar_solver::print_term(lar_term const& term, std::ostream & out) const { - if (!numeric_traits::is_zero(term.m_v)) { - out << term.m_v << " + "; - } bool first = true; for (const auto p : term) { mpq val = p.coeff(); @@ -1270,9 +1267,6 @@ std::ostream& lar_solver::print_term(lar_term const& term, std::ostream & out) c } std::ostream& lar_solver::print_term_as_indices(lar_term const& term, std::ostream & out) const { - if (!numeric_traits::is_zero(term.m_v)) { - out << term.m_v << " + "; - } print_linear_combination_of_column_indices_only(term, out); return out; } @@ -1497,7 +1491,7 @@ bool lar_solver::term_is_int(const lar_term * t) const { for (auto const & p : t->m_coeffs) if (! (column_is_int(p.first) && p.second.is_int())) return false; - return t->m_v.is_int(); + return true; } bool lar_solver::var_is_int(var_index v) const { @@ -1598,17 +1592,13 @@ void lar_solver::add_new_var_to_core_fields_for_mpq(bool register_in_basis) { } -var_index lar_solver::add_term_undecided(const vector> & coeffs, - const mpq &m_v) { - push_and_register_term(new lar_term(coeffs, m_v)); +var_index lar_solver::add_term_undecided(const vector> & coeffs) { + push_and_register_term(new lar_term(coeffs)); return m_terms_start_index + m_terms.size() - 1; } #if Z3DEBUG_CHECK_UNIQUE_TERMS -bool lar_solver::term_coeffs_are_ok(const vector> & coeffs, const mpq& v) { - if (coeffs.empty()) { - return is_zero(v); - } +bool lar_solver::term_coeffs_are_ok(const vector> & coeffs) { for (const auto & p : coeffs) { if (column_is_real(p.second)) @@ -1643,12 +1633,11 @@ void lar_solver::push_and_register_term(lar_term* t) { } // terms -var_index lar_solver::add_term(const vector> & coeffs, - const mpq &m_v) { +var_index lar_solver::add_term(const vector> & coeffs) { if (strategy_is_undecided()) - return add_term_undecided(coeffs, m_v); + return add_term_undecided(coeffs); - push_and_register_term(new lar_term(coeffs, m_v)); + push_and_register_term(new lar_term(coeffs)); unsigned adjusted_term_index = m_terms.size() - 1; var_index ret = m_terms_start_index + adjusted_term_index; if (use_tableau() && !coeffs.empty()) { @@ -1656,13 +1645,12 @@ var_index lar_solver::add_term(const vector> & coeffs, if (m_settings.bound_propagation()) m_rows_with_changed_bounds.insert(A_r().row_count() - 1); } - CTRACE("add_term_lar_solver", !m_v.is_zero(), print_term(*m_terms.back(), tout);); lp_assert(m_var_register.size() == A_r().column_count()); return ret; } void lar_solver::add_row_from_term_no_constraint(const lar_term * term, unsigned term_ext_index) { - TRACE("dump_terms", print_term(*term, tout); tout << std::endl;); + TRACE("dump_terms", print_term(*term, tout) << std::endl;); register_new_ext_var_index(term_ext_index, term_is_int(term)); // j will be a new variable unsigned j = A_r().column_count(); @@ -1744,9 +1732,8 @@ void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_k // lp_assert(!term_is_int(m_terms[adjusted_term_index]) || right_side.is_int()); unsigned term_j; if (m_var_register.external_is_used(j, term_j)) { - mpq rs = right_side - m_terms[adjusted_term_index]->m_v; m_constraints.push_back(new lar_term_constraint(m_terms[adjusted_term_index], kind, right_side)); - update_column_type_and_bound(term_j, kind, rs, ci); + update_column_type_and_bound(term_j, kind, right_side, ci); } else { add_constraint_from_term_and_create_new_column_row(j, m_terms[adjusted_term_index], kind, right_side); @@ -1755,11 +1742,10 @@ void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_k constraint_index lar_solver::add_constraint(const vector>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm) { vector> left_side; - mpq rs = -right_side_parm; - substitute_terms_in_linear_expression(left_side_with_terms, left_side, rs); - unsigned term_index = add_term(left_side, zero_of_type()); + substitute_terms_in_linear_expression(left_side_with_terms, left_side); + unsigned term_index = add_term(left_side); constraint_index ci = m_constraints.size(); - add_var_bound_on_constraint_for_term(term_index, kind_par, -rs, ci); + add_var_bound_on_constraint_for_term(term_index, kind_par, right_side_parm, ci); return ci; } @@ -1768,7 +1754,7 @@ void lar_solver::add_constraint_from_term_and_create_new_column_row(unsigned ter add_row_from_term_no_constraint(term, term_j); unsigned j = A_r().column_count() - 1; - update_column_type_and_bound(j, kind, right_side - term->m_v, m_constraints.size()); + update_column_type_and_bound(j, kind, right_side, m_constraints.size()); m_constraints.push_back(new lar_term_constraint(term, kind, right_side)); lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); } @@ -2266,15 +2252,6 @@ void lar_solver::set_cut_strategy(unsigned cut_frequency) { } } -void lar_solver::adjust_cut_for_terms(const lar_term& t, mpq & rs) { - for (const auto& p : t) { - if (!is_term(p.var())) continue; - const lar_term & p_term = get_term(p.var()); - if (p_term.m_v.is_zero()) continue; - rs -= p.coeff() * p_term.m_v; - } -} - } // namespace lp diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 9e9edacc8..f3aa4f23b 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -164,13 +164,11 @@ public: // terms - var_index add_term(const vector> & coeffs, - const mpq &m_v); + var_index add_term(const vector> & coeffs); - var_index add_term_undecided(const vector> & coeffs, - const mpq &m_v); + var_index add_term_undecided(const vector> & coeffs); - bool term_coeffs_are_ok(const vector> & coeffs, const mpq& v); + bool term_coeffs_are_ok(const vector> & coeffs); void push_and_register_term(lar_term* t); void add_row_for_term(const lar_term * term, unsigned term_ext_index); @@ -331,7 +329,7 @@ public: void substitute_terms_in_linear_expression( const vector>& left_side_with_terms, - vector> &left_side, mpq & free_coeff) const; + vector> &left_side) const; void detect_rows_of_bound_change_column_for_nbasic_column(unsigned j); @@ -534,7 +532,7 @@ public: return m_columns_to_ul_pairs()[j].lower_bound_witness(); } - void subs_term_columns(lar_term& t, mpq & rs) { + void subs_term_columns(lar_term& t) { vector> columns_to_subs; for (const auto & m : t.m_coeffs) { unsigned tj = adjust_column_index_to_term_index(m.first); @@ -548,7 +546,6 @@ public: mpq v = it->second; t.m_coeffs.erase(it); t.m_coeffs[p.second] = v; - rs -= v * lt.m_v; } } @@ -585,6 +582,5 @@ public: lar_term get_term_to_maximize(unsigned ext_j) const; void set_cut_strategy(unsigned cut_frequency); bool sum_first_coords(const lar_term& t, mpq & val) const; - void adjust_cut_for_terms(const lar_term& t, mpq & rs); }; } diff --git a/src/util/lp/lar_term.h b/src/util/lp/lar_term.h index 519847848..e9259b8c0 100644 --- a/src/util/lp/lar_term.h +++ b/src/util/lp/lar_term.h @@ -21,9 +21,9 @@ #include "util/lp/indexed_vector.h" namespace lp { struct lar_term { - // the term evaluates to sum of m_coeffs + m_v + // the term evaluates to sum of m_coeffs std::unordered_map m_coeffs; - mpq m_v; + // mpq m_v; lar_term() {} void add_monomial(const mpq& c, unsigned j) { auto it = m_coeffs.find(j); @@ -37,7 +37,7 @@ struct lar_term { } bool is_empty() const { - return m_coeffs.size() == 0 && is_zero(m_v); + return m_coeffs.size() == 0; // && is_zero(m_v); } unsigned size() const { return static_cast(m_coeffs.size()); } @@ -46,8 +46,7 @@ struct lar_term { return m_coeffs; } - lar_term(const vector>& coeffs, - const mpq & v) : m_v(v) { + lar_term(const vector>& coeffs) { for (const auto & p : coeffs) { add_monomial(p.first, p.second); } @@ -87,7 +86,7 @@ struct lar_term { template T apply(const vector& x) const { - T ret = T(m_v); + T ret(0); for (const auto & t : m_coeffs) { ret += t.second * x[t.first]; } @@ -96,7 +95,6 @@ struct lar_term { void clear() { m_coeffs.clear(); - m_v = zero_of_type(); } struct ival { From 91dbcbc36f1fe3ba51d6804e774ee70dd7b880cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 20 Sep 2018 18:57:47 -0700 Subject: [PATCH 04/22] fix test build Signed-off-by: Nikolaj Bjorner --- src/test/lp/gomory_test.h | 1 - src/test/lp/lp.cpp | 20 +++++++++++++------- 2 files changed, 13 insertions(+), 8 deletions(-) diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h index 501ad9e1a..972466dc3 100644 --- a/src/test/lp/gomory_test.h +++ b/src/test/lp/gomory_test.h @@ -185,7 +185,6 @@ struct gomory_test { } void print_term(lar_term & t, std::ostream & out) { - lp_assert(is_zero(t.m_v)); vector> row; for (auto p : t.m_coeffs) row.push_back(std::make_pair(p.second, p.first)); diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 6e418fe68..ff9de0e58 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -2667,13 +2667,20 @@ void test_term() { lar_solver solver; unsigned _x = 0; unsigned _y = 1; + unsigned _one = 2; var_index x = solver.add_var(_x, false); var_index y = solver.add_var(_y, false); + var_index one = solver.add_var(_one, false); + + vector> term_one; + term_one.push_back(std::make_pair((int)1, one)); + solver.add_constraint(term_one, lconstraint_kind::EQ, mpq(0)); vector> term_ls; term_ls.push_back(std::pair((int)1, x)); term_ls.push_back(std::pair((int)1, y)); - var_index z = solver.add_term(term_ls, mpq(3)); + term_ls.push_back(std::make_pair((int)3, one)); + var_index z = solver.add_term(term_ls); vector> ls; ls.push_back(std::pair((int)1, x)); @@ -2743,10 +2750,10 @@ void test_bound_propagation_one_small_sample1() { vector> coeffs; coeffs.push_back(std::pair(1, a)); coeffs.push_back(std::pair(-1, c)); - ls.add_term(coeffs, zero_of_type()); + ls.add_term(coeffs); coeffs.pop_back(); coeffs.push_back(std::pair(-1, b)); - ls.add_term(coeffs, zero_of_type()); + ls.add_term(coeffs); coeffs.clear(); coeffs.push_back(std::pair(1, a)); coeffs.push_back(std::pair(-1, b)); @@ -3485,12 +3492,12 @@ void test_maximize_term() { vector> term_ls; term_ls.push_back(std::pair((int)1, x)); term_ls.push_back(std::pair((int)-1, y)); - unsigned term_x_min_y = solver.add_term(term_ls, mpq(0)); + unsigned term_x_min_y = solver.add_term(term_ls); term_ls.clear(); term_ls.push_back(std::pair((int)2, x)); term_ls.push_back(std::pair((int)2, y)); - unsigned term_2x_pl_2y = solver.add_term(term_ls, mpq(0)); + unsigned term_2x_pl_2y = solver.add_term(term_ls); solver.add_var_bound(term_x_min_y, LE, zero_of_type()); solver.add_var_bound(term_2x_pl_2y, LE, mpq((int)5)); solver.find_feasible_solution(); @@ -3502,8 +3509,7 @@ void test_maximize_term() { std::cout<< "v[" << p.first << "] = " << p.second << std::endl; } std::cout << "calling int_solver\n"; - lar_term t; mpq k; explanation ex; bool upper; - lia_move lm = i_solver.check(t, k, ex, upper); + lia_move lm = i_solver.check(); VERIFY(lm == lia_move::sat); impq term_max; lp_status st = solver.maximize_term(term_2x_pl_2y, term_max); From 382bce4bb79c4823af0605bd94c7cc824c641b4d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 20 Sep 2018 19:19:40 -0700 Subject: [PATCH 05/22] fix #1836 Signed-off-by: Nikolaj Bjorner --- src/api/ml/z3.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 25b437bc4..d7d8aeddc 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1816,7 +1816,7 @@ struct let get_model x = let q = Z3native.solver_get_model (gc x) x in - if Z3native.is_null_model q then None else Some q + try if Z3native.is_null_model q then None else Some q with | _ -> None let get_proof x = let q = Z3native.solver_get_proof (gc x) x in From d6a1d17d695648e6e6b713323122a55a26283184 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Thu, 20 Sep 2018 16:28:45 -0700 Subject: [PATCH 06/22] extend(src/api/c++/z3++.h): support units() for solver class --- src/api/c++/z3++.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index e1f263e17..a65d6e4d8 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2038,6 +2038,7 @@ namespace z3 { stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); } expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } + expr_vector units() const { Z3_ast_vector r = Z3_solver_get_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); } friend std::ostream & operator<<(std::ostream & out, solver const & s); From 39ed27101ed9f465504f4e12e2bd2f676ea66fda Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 20 Sep 2018 19:56:55 -0700 Subject: [PATCH 07/22] include version.h in install include directory for cmake build #1833 Signed-off-by: Nikolaj Bjorner --- src/CMakeLists.txt | 2 ++ src/util/CMakeLists.txt | 1 + 2 files changed, 3 insertions(+) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 826f87e8c..c2d7d84a3 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -166,6 +166,8 @@ foreach (header ${libz3_public_headers}) set_property(TARGET libz3 APPEND PROPERTY PUBLIC_HEADER "${CMAKE_SOURCE_DIR}/src/api/${header}") endforeach() +set_property(TARGET libz3 APPEND PROPERTY + PUBLIC_HEADER "${CMAKE_CURRENT_BINARY_DIR}/util/version.h") install(TARGETS libz3 EXPORT Z3_EXPORTED_TARGETS diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 85b6f955c..a84cc1f00 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -7,6 +7,7 @@ endif() set(Z3_FULL_VERSION "\"${Z3_FULL_VERSION_STR}\"") configure_file(version.h.cmake.in ${CMAKE_CURRENT_BINARY_DIR}/version.h) + z3_add_component(util SOURCES approx_nat.cpp From c59a957737bdb04319df105cdd61130b228f23c6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 20 Sep 2018 20:37:14 -0700 Subject: [PATCH 08/22] add non-units method Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 15 +++++++++++++++ src/api/c++/z3++.h | 1 + src/api/z3_api.h | 8 ++++++++ src/solver/solver.cpp | 29 +++++++++++++++++++++++++++++ src/solver/solver.h | 2 ++ 5 files changed, 55 insertions(+) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index fc42acbb9..5a4537a4a 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -372,6 +372,21 @@ extern "C" { Z3_CATCH_RETURN(0); } + Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s) { + Z3_TRY; + LOG_Z3_solver_get_non_units(c, s); + RESET_ERROR_CODE(); + init_solver(c, s); + Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); + mk_c(c)->save_object(v); + expr_ref_vector fmls = to_solver_ref(s)->get_non_units(mk_c(c)->m()); + for (expr* f : fmls) { + v->m_ast_vector.push_back(f); + } + RETURN_Z3(of_ast_vector(v)); + Z3_CATCH_RETURN(0); + } + static Z3_lbool _solver_check(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[]) { for (unsigned i = 0; i < num_assumptions; i++) { if (!is_expr(to_ast(assumptions[i]))) { diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index e1f263e17..378819682 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2038,6 +2038,7 @@ namespace z3 { stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); } expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } + expr_vector non_units() const { Z3_ast_vector r = Z3_solver_get_non_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); } friend std::ostream & operator<<(std::ostream & out, solver const & s); diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 2657e558d..03bce5d5e 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6121,6 +6121,14 @@ extern "C" { */ Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s); + + /** + \brief Return the set of non units in the solver state. + + def_API('Z3_solver_get_non_units', AST_VECTOR, (_in(CONTEXT), _in(SOLVER))) + */ + Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s); + /** \brief Check whether the assertions in a given solver are consistent or not. diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 4044c4a85..149fe0d65 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -256,3 +256,32 @@ expr_ref_vector solver::get_units(ast_manager& m) { return result; } + +expr_ref_vector solver::get_non_units(ast_manager& m) { + expr_ref_vector result(m), fmls(m); + get_assertions(fmls); + family_id bfid = m.get_basic_family_id(); + expr_mark marked; + for (unsigned i = 0; i < fmls.size(); ++i) { + expr* f = fmls.get(i); + if (marked.is_marked(f)) continue; + marked.mark(f); + if (!is_app(f)) { + result.push_back(f); + continue; + } + app* _f = to_app(f); + if (_f->get_family_id() == bfid) { + if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) { + fmls.append(_f->get_num_args(), _f->get_args()); + } + else if (m.is_eq(f) || m.is_distinct(f)) { + result.push_back(f); + } + } + else { + result.push_back(f); + } + } + return result; +} diff --git a/src/solver/solver.h b/src/solver/solver.h index c371be284..5329161cd 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -236,6 +236,8 @@ public: */ expr_ref_vector get_units(ast_manager& m); + expr_ref_vector get_non_units(ast_manager& m); + class scoped_push { solver& s; bool m_nopop; From 0b7918c52eaadee049e28056b134e4621035d85f Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 21 Sep 2018 09:37:36 +0100 Subject: [PATCH 09/22] remove spurious pragma --- src/smt/smt_arith_value.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/smt/smt_arith_value.cpp b/src/smt/smt_arith_value.cpp index ce4c0d9a9..41679851a 100644 --- a/src/smt/smt_arith_value.cpp +++ b/src/smt/smt_arith_value.cpp @@ -1,4 +1,3 @@ - /*++ Copyright (c) 2018 Microsoft Corporation @@ -17,7 +16,6 @@ Author: Revision History: --*/ -#pragma once; #include "smt/smt_arith_value.h" #include "smt/theory_lra.h" From 0c4754d94bdfaf07077120f5cbff780d8fb0971d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Sep 2018 20:13:58 -0700 Subject: [PATCH 10/22] rename version.h to z3_version.h to differentiate name in install include directory. Add support for z3_version.h in python build system. #1833 Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 2 +- scripts/mk_util.py | 4 ++-- src/CMakeLists.txt | 2 +- src/shell/main.cpp | 2 +- src/solver/solver.cpp | 3 ++- src/util/CMakeLists.txt | 6 +++--- src/util/{version.h.cmake.in => z3_version.h.cmake.in} | 0 src/util/{version.h.in => z3_version.h.in} | 0 8 files changed, 10 insertions(+), 9 deletions(-) rename src/util/{version.h.cmake.in => z3_version.h.cmake.in} (100%) rename src/util/{version.h.in => z3_version.h.in} (100%) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index ca62f5c5f..1ec5f05b5 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -10,7 +10,7 @@ from mk_util import * # Z3 Project definition def init_project_def(): set_version(4, 8, 0, 0) - add_lib('util', []) + add_lib('util', [], includes2install = ['z3_version.h']) add_lib('polynomial', ['util'], 'math/polynomial') add_lib('sat', ['util']) add_lib('nlsat', ['polynomial', 'sat']) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 770e118ee..ebe017739 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2805,8 +2805,8 @@ def get_full_version_string(major, minor, build, revision): # Update files with the version number def mk_version_dot_h(major, minor, build, revision): c = get_component(UTIL_COMPONENT) - version_template = os.path.join(c.src_dir, 'version.h.in') - version_header_output = os.path.join(c.src_dir, 'version.h') + version_template = os.path.join(c.src_dir, 'z3_version.h.in') + version_header_output = os.path.join(c.src_dir, 'z3_version.h') # Note the substitution names are what is used by the CMake # builds system. If you change these you should change them # in the CMake build too diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c2d7d84a3..c497c19ee 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -167,7 +167,7 @@ foreach (header ${libz3_public_headers}) PUBLIC_HEADER "${CMAKE_SOURCE_DIR}/src/api/${header}") endforeach() set_property(TARGET libz3 APPEND PROPERTY - PUBLIC_HEADER "${CMAKE_CURRENT_BINARY_DIR}/util/version.h") + PUBLIC_HEADER "${CMAKE_CURRENT_BINARY_DIR}/util/z3_version.h") install(TARGETS libz3 EXPORT Z3_EXPORTED_TARGETS diff --git a/src/shell/main.cpp b/src/shell/main.cpp index bb1c19b47..1c8b6908d 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -26,7 +26,7 @@ Revision History: #include "shell/smtlib_frontend.h" #include "shell/z3_log_frontend.h" #include "util/warning.h" -#include "util/version.h" +#include "util/z3_version.h" #include "shell/dimacs_frontend.h" #include "shell/datalog_frontend.h" #include "shell/opt_frontend.h" diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index e4fe09adf..a7c1372b3 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -273,7 +273,8 @@ expr_ref_vector solver::get_non_units(ast_manager& m) { } app* _f = to_app(f); if (_f->get_family_id() == bfid) { - // basic objects are true/false/and/or/not/=/distinct and proof objects (that are not Boolean) + // basic objects are true/false/and/or/not/=/distinct + // and proof objects (that are not Boolean). if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) { fmls.append(_f->get_num_args(), _f->get_args()); } diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index a84cc1f00..b6abb785f 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -1,11 +1,11 @@ -if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/version.h") - message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/version.h\"" +if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/z3_version.h") + message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/z3_version.h\"" ${z3_polluted_tree_msg} ) endif() set(Z3_FULL_VERSION "\"${Z3_FULL_VERSION_STR}\"") -configure_file(version.h.cmake.in ${CMAKE_CURRENT_BINARY_DIR}/version.h) +configure_file(z3_version.h.cmake.in ${CMAKE_CURRENT_BINARY_DIR}/z3_version.h) z3_add_component(util diff --git a/src/util/version.h.cmake.in b/src/util/z3_version.h.cmake.in similarity index 100% rename from src/util/version.h.cmake.in rename to src/util/z3_version.h.cmake.in diff --git a/src/util/version.h.in b/src/util/z3_version.h.in similarity index 100% rename from src/util/version.h.in rename to src/util/z3_version.h.in From e391416855aa5298c1ce880109e1b4fbfc2b7a49 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Sep 2018 20:30:50 -0700 Subject: [PATCH 11/22] fix include path for z3_version.h Signed-off-by: Nikolaj Bjorner --- src/cmd_context/basic_cmds.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index e65eb1b32..ea5994ece 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -17,7 +17,7 @@ Notes: --*/ #include "util/gparams.h" #include "util/env_params.h" -#include "util/version.h" +#include "util/z3_version.h" #include "ast/ast_smt_pp.h" #include "ast/ast_smt2_pp.h" #include "ast/ast_pp_dot.h" From 8e0eebf507307b8a3ddc59f305a6486d78a5f4c5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Sep 2018 20:37:13 -0700 Subject: [PATCH 12/22] fix include path for z3_version.h Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index cc2a13aed..4b3b85399 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -19,7 +19,7 @@ Revision History: --*/ #include #include "api/api_context.h" -#include "util/version.h" +#include "util/z3_version.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" #include "api/api_log_macros.h" From 984e74428aedbc36ea5930ba78c9890594524444 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Sep 2018 20:41:26 -0700 Subject: [PATCH 13/22] fix include path for z3_version.h Signed-off-by: Nikolaj Bjorner --- src/api/api_log.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp index 1bdbb8735..0f531b98e 100644 --- a/src/api/api_log.cpp +++ b/src/api/api_log.cpp @@ -19,7 +19,7 @@ Revision History: #include "api/z3.h" #include "api/api_log_macros.h" #include "util/util.h" -#include "util/version.h" +#include "util/z3_version.h" std::ostream * g_z3_log = nullptr; bool g_z3_log_enabled = false; From f349d3d0137c0ad09cf6881a4291743110b87630 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Sep 2018 21:15:28 -0700 Subject: [PATCH 14/22] fix extraction of non-units Signed-off-by: Nikolaj Bjorner --- src/solver/solver.cpp | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index a7c1372b3..66fedb36f 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -257,6 +257,15 @@ expr_ref_vector solver::get_units(ast_manager& m) { return result; } +static bool is_atom(ast_manager& m, expr* f) { + if (!is_app(f)) return true; + app* _f = to_app(f); + family_id bfid = m.get_basic_family_id(); + if (_f->get_family_id() != bfid) return true; + if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) return false; + return m.is_eq(f) || m.is_distinct(f); +} + expr_ref_vector solver::get_non_units(ast_manager& m) { expr_ref_vector result(m), fmls(m); get_assertions(fmls); @@ -275,13 +284,17 @@ expr_ref_vector solver::get_non_units(ast_manager& m) { if (_f->get_family_id() == bfid) { // basic objects are true/false/and/or/not/=/distinct // and proof objects (that are not Boolean). - if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) { + if (i < sz0 && m.is_not(f) && is_atom(m, _f->get_arg(0))) { + marked.mark(_f->get_arg(0)); + } + else if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) { fmls.append(_f->get_num_args(), _f->get_args()); } - else if (m.is_eq(f) || m.is_distinct(f)) { - if (i >= sz0) result.push_back(f); + else if (i >= sz0 && is_atom(m, f)) { + result.push_back(f); } } + else { if (i >= sz0) result.push_back(f); } From 3113901c8fecf70ce0284bce0797ab2f7013ee67 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Sep 2018 23:15:57 -0700 Subject: [PATCH 15/22] rename is_atom Signed-off-by: Nikolaj Bjorner --- src/solver/solver.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 66fedb36f..1f0dac0ce 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -257,7 +257,7 @@ expr_ref_vector solver::get_units(ast_manager& m) { return result; } -static bool is_atom(ast_manager& m, expr* f) { +static bool is_m_atom(ast_manager& m, expr* f) { if (!is_app(f)) return true; app* _f = to_app(f); family_id bfid = m.get_basic_family_id(); @@ -284,13 +284,13 @@ expr_ref_vector solver::get_non_units(ast_manager& m) { if (_f->get_family_id() == bfid) { // basic objects are true/false/and/or/not/=/distinct // and proof objects (that are not Boolean). - if (i < sz0 && m.is_not(f) && is_atom(m, _f->get_arg(0))) { + if (i < sz0 && m.is_not(f) && is_m_atom(m, _f->get_arg(0))) { marked.mark(_f->get_arg(0)); } else if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) { fmls.append(_f->get_num_args(), _f->get_args()); } - else if (i >= sz0 && is_atom(m, f)) { + else if (i >= sz0 && is_m_atom(m, f)) { result.push_back(f); } } From 43f89dc2ccfbb24f2f13f394595abfd3e29b50bd Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 22 Sep 2018 12:01:24 -0700 Subject: [PATCH 16/22] changes in column_info of lar_solver Signed-off-by: Lev Nachmanson --- src/util/lp/column_info.h | 10 ---------- src/util/lp/lar_solver.cpp | 9 ++------- src/util/lp/lar_solver.h | 2 +- src/util/lp/lp_primal_core_solver_def.h | 1 + src/util/lp/lp_solver_def.h | 2 +- 5 files changed, 5 insertions(+), 19 deletions(-) diff --git a/src/util/lp/column_info.h b/src/util/lp/column_info.h index 407f40dfc..2a38900c1 100644 --- a/src/util/lp/column_info.h +++ b/src/util/lp/column_info.h @@ -69,16 +69,6 @@ public: m_column_index(static_cast(-1)) {} - column_info(unsigned column_index) : - m_lower_bound_is_set(false), - m_lower_bound_is_strict(false), - m_upper_bound_is_set (false), - m_upper_bound_is_strict (false), - m_is_fixed(false), - m_cost(numeric_traits::zero()), - m_column_index(column_index) { - } - column_info(const column_info & ci) { m_name = ci.m_name; m_lower_bound_is_set = ci.m_lower_bound_is_set; diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 30494aa1c..c83268602 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -909,13 +909,8 @@ bool lar_solver::try_to_set_fixed(column_info & ci) { return false; } -column_type lar_solver::get_column_type(const column_info & ci) { - auto ret = ci.get_column_type_no_flipping(); - if (ret == column_type::boxed) { // changing boxed to fixed because of the no span - if (ci.get_lower_bound() == ci.get_upper_bound()) - ret = column_type::fixed; - } - return ret; +column_type lar_solver::get_column_type(unsigned j) const{ + return m_mpq_lar_core_solver.m_column_types[j]; } std::string lar_solver::get_column_name(unsigned j) const { diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index f3aa4f23b..cfe581ba3 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -395,7 +395,7 @@ public: bool try_to_set_fixed(column_info & ci); - column_type get_column_type(const column_info & ci); + column_type get_column_type(unsigned j) const; std::string get_column_name(unsigned j) const; diff --git a/src/util/lp/lp_primal_core_solver_def.h b/src/util/lp/lp_primal_core_solver_def.h index 1e9edbd31..872922f60 100644 --- a/src/util/lp/lp_primal_core_solver_def.h +++ b/src/util/lp/lp_primal_core_solver_def.h @@ -1238,6 +1238,7 @@ template void lp_primal_core_solver::print_column break; case column_type::free_column: out << "( _" << this->m_x[j] << "_)" << std::endl; + break; default: lp_unreachable(); } diff --git a/src/util/lp/lp_solver_def.h b/src/util/lp/lp_solver_def.h index 10c7a6feb..9b385dee6 100644 --- a/src/util/lp/lp_solver_def.h +++ b/src/util/lp/lp_solver_def.h @@ -24,7 +24,7 @@ Revision History: namespace lp { template column_info * lp_solver::get_or_create_column_info(unsigned column) { auto it = m_map_from_var_index_to_column_info.find(column); - return (it == m_map_from_var_index_to_column_info.end())? (m_map_from_var_index_to_column_info[column] = new column_info(static_cast(-1))) : it->second; + return (it == m_map_from_var_index_to_column_info.end())? (m_map_from_var_index_to_column_info[column] = new column_info()) : it->second; } template From 7b3b1b6e9f70231d29981def70522913bc96ec20 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 Sep 2018 14:04:15 -0700 Subject: [PATCH 17/22] pop to base before incremental internalization to ensure that units are not lost Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 3 ++- src/solver/solver.cpp | 21 +++++++++++---------- 2 files changed, 13 insertions(+), 11 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index ff55598c2..097d3f0fa 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -259,7 +259,7 @@ public: return m_num_scopes; } - void assert_expr_core2(expr * t, expr * a) override { + void assert_expr_core2(expr * t, expr * a) override { if (a) { m_asmsf.push_back(a); assert_expr_core(m.mk_implies(a, t)); @@ -473,6 +473,7 @@ public: } void convert_internalized() { + m_solver.pop_to_base_level(); if (!is_internalized() && m_fmls_head > 0) { internalize_formulas(); } diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 1f0dac0ce..0e2128990 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -178,10 +178,19 @@ lbool solver::preferred_sat(expr_ref_vector const& asms, vector return check_sat(0, nullptr); } -bool solver::is_literal(ast_manager& m, expr* e) { - return is_uninterp_const(e) || (m.is_not(e, e) && is_uninterp_const(e)); + +static bool is_m_atom(ast_manager& m, expr* f) { + if (!is_app(f)) return true; + app* _f = to_app(f); + family_id bfid = m.get_basic_family_id(); + if (_f->get_family_id() != bfid) return true; + if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) return false; + return m.is_eq(f) || m.is_distinct(f); } +bool solver::is_literal(ast_manager& m, expr* e) { + return is_m_atom(m, e) || (m.is_not(e, e) && is_m_atom(m, e)); +} void solver::assert_expr(expr* f) { expr_ref fml(f, get_manager()); @@ -257,14 +266,6 @@ expr_ref_vector solver::get_units(ast_manager& m) { return result; } -static bool is_m_atom(ast_manager& m, expr* f) { - if (!is_app(f)) return true; - app* _f = to_app(f); - family_id bfid = m.get_basic_family_id(); - if (_f->get_family_id() != bfid) return true; - if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) return false; - return m.is_eq(f) || m.is_distinct(f); -} expr_ref_vector solver::get_non_units(ast_manager& m) { expr_ref_vector result(m), fmls(m); From 9a09689dfab27059332092bf329db0c4abc258b2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 Sep 2018 19:19:05 -0700 Subject: [PATCH 18/22] add documentation on the cuber Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 11 ++++++++++- src/sat/sat_lookahead.cpp | 2 ++ src/sat/sat_params.pyg | 28 +++++++++++++++++++++++++--- 3 files changed, 37 insertions(+), 4 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index b9e15d329..a6b05904c 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6605,7 +6605,12 @@ class Solver(Z3PPObject): _handle_parse_error(e, self.ctx) def cube(self, vars = None): - """Get set of cubes""" + """Get set of cubes + The method takes an optional set of variables that restrict which + variables may be used as a starting point for cubing. + If vars is not None, then the first case split is based on a variable in + this set. + """ self.cube_vs = AstVector(None, self.ctx) if vars is not None: for v in vars: @@ -6621,6 +6626,10 @@ class Solver(Z3PPObject): return def cube_vars(self): + """Access the set of variables that were touched by the most recently generated cube. + This set of variables can be used as a starting point for additional cubes. + The idea is that variables that appear in clauses that are reduced by the most recent + cube are likely more useful to cube on.""" return self.cube_vs def proof(self): diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 3833e2a52..4ca2c5f84 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -16,6 +16,8 @@ Author: Notes: + + --*/ #include diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 89776c479..113a8133e 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -50,17 +50,39 @@ def_module_params('sat', ('unit_walk', BOOL, False, 'use unit-walk search instead of CDCL'), ('unit_walk_threads', UINT, 0, 'number of unit-walk search threads to find satisfiable solution'), ('lookahead.cube.cutoff', SYMBOL, 'depth', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'), + # - depth: the maximal cutoff is fixed to the value of lookahead.cube.depth. + # So if the value is 10, at most 1024 cubes will be generated of length 10. + # - freevars: cutoff based on a variable fraction of lookahead.cube.freevars. + # Cut if the number of current unassigned variables drops below a fraction of number of initial variables. + # - psat: Let psat_heur := (Sum_{clause C} (psat.clause_base ^ {-|C|+1})) / |freevars|^psat.var_exp + # Cut if the value of psat_heur exceeds psat.trigger + # - adaptive_freevars: Cut if the number of current unassigned variables drops below a fraction of free variables + # at the time of the last conflict. The fraction is increased every time the a cutoff is created. + # - adative_psat: Cut based on psat_heur in an adaptive way. ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat'), ('lookahead.cube.depth', UINT, 1, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.'), - ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free fariable fraction. Used when lookahead.cube.cutoff is freevars'), + ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free variable fraction. Used when lookahead.cube.cutoff is freevars'), ('lookahead.cube.psat.var_exp', DOUBLE, 1, 'free variable exponent for PSAT cutoff'), ('lookahead.cube.psat.clause_base', DOUBLE, 2, 'clause base for PSAT cutoff'), ('lookahead.cube.psat.trigger', DOUBLE, 5, 'trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat'), - ('lookahead_search', BOOL, False, 'use lookahead solver'), ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), ('lookahead.use_learned', BOOL, False, 'use learned clauses when selecting lookahead literal'), ('lookahead_simplify.bca', BOOL, True, 'add learned binary clauses as part of lookahead simplification'), ('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'), - ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'))) + ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu')) + # reward function used to determine which literal to cube on. + # - ternary: reward function useful for random 3-SAT instances. Used by Heule and Knuth in March. + # - heule_schur: reward function based on "Schur Number 5", Heule, AAAI 2018 + # The score of a literal lit is: + # Sum_{C in Clauses | lit in C} 2 ^ (- |C|+1) + # * Sum_{lit' in C | lit' != lit} lit_occs(~lit') + # / | C | + # where lit_occs(lit) is the number of clauses containing lit. + # - heuleu: The score of a literal lit is: Sum_{C in Clauses | lit in C} 2 ^ (-|C| + 1) + # - unit: heule_schur + also counts number of unit clauses. + # - march_cu: default reward function used in a version of March + # Each reward function also comes with its own variant of "mix_diff", which + # is the function for combining reward metrics for the positive and negative variant of a literal. + ) From 066b5334ad5882dff635abd354928f14b9a3c4d2 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 22 Sep 2018 20:57:59 -0700 Subject: [PATCH 19/22] refactor some parameters into fields in Gomory cuts Signed-off-by: Lev Nachmanson --- src/util/lp/gomory.cpp | 119 +++++++++++++++++++++-------------------- 1 file changed, 62 insertions(+), 57 deletions(-) diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp index 96b3ab395..ad1c02625 100644 --- a/src/util/lp/gomory.cpp +++ b/src/util/lp/gomory.cpp @@ -27,11 +27,15 @@ class gomory::imp { lar_term & m_t; // the term to return in the cut mpq & m_k; // the right side of the cut explanation& m_ex; // the conflict explanation - unsigned m_inf_col; // a basis column which has to be an integer but has a not integral value + unsigned m_inf_col; // a basis column which has to be an integer but has a non integral value const row_strip& m_row; - const int_solver& m_int_solver; - - + const int_solver& m_int_solver; + mpq m_lcm_den; + mpq m_f; + mpq m_one_minus_f; + mpq m_fj; + mpq m_one_minus_fj; + const impq & get_value(unsigned j) const { return m_int_solver.get_value(j); } bool is_real(unsigned j) const { return m_int_solver.is_real(j); } bool at_lower(unsigned j) const { return m_int_solver.at_lower(j); } @@ -42,66 +46,60 @@ class gomory::imp { constraint_index column_upper_bound_constraint(unsigned j) const { return m_int_solver.column_upper_bound_constraint(j); } bool column_is_fixed(unsigned j) const { return m_int_solver.m_lar_solver->column_is_fixed(j); } - void int_case_in_gomory_cut(const mpq & a, unsigned j, - mpq & lcm_den, const mpq& f0, const mpq& one_minus_f0) { - lp_assert(is_int(j) && !a.is_int()); - mpq fj = fractional_part(a); + void int_case_in_gomory_cut(unsigned j) { + lp_assert(is_int(j) && m_fj.is_pos()); TRACE("gomory_cut_detail", - tout << a << " j=" << j << " k = " << m_k; - tout << ", fj: " << fj << ", "; - tout << "a - fj = " << a - fj << ", "; + tout << " k = " << m_k; + tout << ", fj: " << m_fj << ", "; tout << (at_lower(j)?"at_lower":"at_upper")<< std::endl; ); - lp_assert(fj.is_pos() && (a - fj).is_int()); mpq new_a; if (at_lower(j)) { - new_a = fj <= one_minus_f0 ? fj / one_minus_f0 : ((1 - fj) / f0); + new_a = m_fj <= m_one_minus_f ? m_fj / m_one_minus_f : ((1 - m_fj) / m_f); lp_assert(new_a.is_pos()); m_k.addmul(new_a, lower_bound(j).x); - m_ex.push_justification(column_lower_bound_constraint(j), new_a); + m_ex.push_justification(column_lower_bound_constraint(j)); } else { lp_assert(at_upper(j)); // the upper terms are inverted: therefore we have the minus - new_a = - (fj <= f0 ? fj / f0 : ((1 - fj) / one_minus_f0)); + new_a = - (m_fj <= m_f ? m_fj / m_f : ((1 - m_fj) / m_one_minus_f)); lp_assert(new_a.is_neg()); m_k.addmul(new_a, upper_bound(j).x); - m_ex.push_justification(column_upper_bound_constraint(j), new_a); + m_ex.push_justification(column_upper_bound_constraint(j)); } m_t.add_monomial(new_a, j); - lcm_den = lcm(lcm_den, denominator(new_a)); - TRACE("gomory_cut_detail", tout << "v" << j << " new_a = " << new_a << ", k = " << m_k << ", lcm_den = " << lcm_den << "\n";); + m_lcm_den = lcm(m_lcm_den, denominator(new_a)); + TRACE("gomory_cut_detail", tout << "v" << j << " new_a = " << new_a << ", k = " << m_k << ", m_lcm_den = " << m_lcm_den << "\n";); } - void real_case_in_gomory_cut(const mpq & a, unsigned x_j, const mpq& f0, const mpq& one_minus_f0) { + void real_case_in_gomory_cut(const mpq & a, unsigned j) { TRACE("gomory_cut_detail_real", tout << "real\n";); mpq new_a; - if (at_lower(x_j)) { + if (at_lower(j)) { if (a.is_pos()) { - new_a = a / one_minus_f0; + new_a = a / m_one_minus_f; } else { - new_a = a / f0; - new_a.neg(); + new_a = - a / m_f; } - m_k.addmul(new_a, lower_bound(x_j).x); // is it a faster operation than - // k += lower_bound(x_j).x * new_a; - m_ex.push_justification(column_lower_bound_constraint(x_j), new_a); + m_k.addmul(new_a, lower_bound(j).x); // is it a faster operation than + // k += lower_bound(j).x * new_a; + m_ex.push_justification(column_lower_bound_constraint(j)); } else { - lp_assert(at_upper(x_j)); + lp_assert(at_upper(j)); if (a.is_pos()) { - new_a = a / f0; - new_a.neg(); // the upper terms are inverted. + new_a = - a / m_f; } else { - new_a = a / one_minus_f0; + new_a = a / m_one_minus_f; } - m_k.addmul(new_a, upper_bound(x_j).x); // k += upper_bound(x_j).x * new_a; - m_ex.push_justification(column_upper_bound_constraint(x_j), new_a); + m_k.addmul(new_a, upper_bound(j).x); // k += upper_bound(j).x * new_a; + m_ex.push_justification(column_upper_bound_constraint(j)); } - TRACE("gomory_cut_detail_real", tout << a << "*v" << x_j << " k: " << m_k << "\n";); - m_t.add_monomial(new_a, x_j); + TRACE("gomory_cut_detail_real", tout << a << "*v" << j << " k: " << m_k << "\n";); + m_t.add_monomial(new_a, j); } lia_move report_conflict_from_gomory_cut() { @@ -111,7 +109,7 @@ class gomory::imp { return lia_move::conflict; } - void adjust_term_and_k_for_some_ints_case_gomory(mpq &lcm_den) { + void adjust_term_and_k_for_some_ints_case_gomory() { lp_assert(!m_t.is_empty()); // k = 1 + sum of m_t at bounds auto pol = m_t.coeffs_as_vector(); @@ -134,16 +132,16 @@ class gomory::imp { m_t.add_monomial(mpq(1), v); } } else { - lcm_den = lcm(lcm_den, denominator(m_k)); - lp_assert(lcm_den.is_pos()); - TRACE("gomory_cut_detail", tout << "pol.size() > 1 den: " << lcm_den << std::endl;); - if (!lcm_den.is_one()) { + m_lcm_den = lcm(m_lcm_den, denominator(m_k)); + lp_assert(m_lcm_den.is_pos()); + TRACE("gomory_cut_detail", tout << "pol.size() > 1 den: " << m_lcm_den << std::endl;); + if (!m_lcm_den.is_one()) { // normalize coefficients of integer parameters to be integers. for (auto & pi: pol) { - pi.first *= lcm_den; + pi.first *= m_lcm_den; SASSERT(!is_int(pi.second) || pi.first.is_int()); } - m_k *= lcm_den; + m_k *= m_lcm_den; } // negate everything to return -pol <= -m_k for (const auto & pi: pol) { @@ -275,14 +273,14 @@ public: // gomory will be t <= k and the current solution has a property t > k m_k = 1; m_t.clear(); - mpq lcm_den(1); + mpq m_lcm_den(1); bool some_int_columns = false; - mpq f0 = fractional_part(get_value(m_inf_col)); - TRACE("gomory_cut_detail", tout << "f0: " << f0 << ", "; - tout << "1 - f0: " << 1 - f0 << ", get_value(m_inf_col).x - f0 = " << get_value(m_inf_col).x - f0;); - lp_assert(f0.is_pos() && (get_value(m_inf_col).x - f0).is_int()); + mpq m_f = fractional_part(get_value(m_inf_col)); + TRACE("gomory_cut_detail", tout << "m_f: " << m_f << ", "; + tout << "1 - m_f: " << 1 - m_f << ", get_value(m_inf_col).x - m_f = " << get_value(m_inf_col).x - m_f;); + lp_assert(m_f.is_pos() && (get_value(m_inf_col).x - m_f).is_int()); - mpq one_min_f0 = 1 - f0; + mpq one_min_m_f = 1 - m_f; for (const auto & p : m_row) { unsigned j = p.var(); if (j == m_inf_col) { @@ -290,20 +288,26 @@ public: TRACE("gomory_cut_detail", tout << "seeing basic var";); continue; } - // make the format compatible with the format used in: Integrating Simplex with DPLL(T) - mpq a = - p.coeff(); - if (is_real(j)) - real_case_in_gomory_cut(a, j, f0, one_min_f0); - else if (!a.is_int()) { // fj will be zero and no monomial will be added + + // use -p.coeff() to make the format compatible with the format used in: Integrating Simplex with DPLL(T) + if (is_real(j)) { + real_case_in_gomory_cut(- p.coeff(), j); + } else { + if (p.coeff().is_int()) { + // m_fj will be zero and no monomial will be added + continue; + } some_int_columns = true; - int_case_in_gomory_cut(a, j, lcm_den, f0, one_min_f0); + m_fj = fractional_part(-p.coeff()); + m_one_minus_fj = 1 - m_fj; + int_case_in_gomory_cut(j); } } if (m_t.is_empty()) return report_conflict_from_gomory_cut(); if (some_int_columns) - adjust_term_and_k_for_some_ints_case_gomory(lcm_den); + adjust_term_and_k_for_some_ints_case_gomory(); lp_assert(m_int_solver.current_solution_is_inf_on_cut()); TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);); m_int_solver.m_lar_solver->subs_term_columns(m_t); @@ -317,9 +321,10 @@ public: m_ex(ex), m_inf_col(basic_inf_int_j), m_row(row), - m_int_solver(int_slv) - { - } + m_int_solver(int_slv), + m_lcm_den(1), + m_f(fractional_part(get_value(basic_inf_int_j).x)), + m_one_minus_f(1 - m_f) {} }; From 80d0c5cf8217e344e1a18de7dadda53298927074 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Sep 2018 16:52:25 -0700 Subject: [PATCH 20/22] fix #1836 again Signed-off-by: Nikolaj Bjorner --- src/api/ml/z3.ml | 12 ++++++++---- src/sat/sat_solver/inc_sat_solver.cpp | 4 ++++ 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index d7d8aeddc..231587729 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1815,8 +1815,10 @@ struct | _ -> UNKNOWN let get_model x = - let q = Z3native.solver_get_model (gc x) x in - try if Z3native.is_null_model q then None else Some q with | _ -> None + try + let q = Z3native.solver_get_model (gc x) x in + if Z3native.is_null_model q then None else Some q + with | _ -> None let get_proof x = let q = Z3native.solver_get_proof (gc x) x in @@ -1952,8 +1954,10 @@ struct | _ -> Solver.UNKNOWN let get_model (x:optimize) = - let q = Z3native.optimize_get_model (gc x) x in - if Z3native.is_null_model q then None else Some q + try + let q = Z3native.optimize_get_model (gc x) x in + if Z3native.is_null_model q then None else Some q + with | _ -> None let get_lower (x:handle) = Z3native.optimize_get_lower (gc x.opt) x.opt x.h let get_upper (x:handle) = Z3native.optimize_get_upper (gc x.opt) x.opt x.h diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 097d3f0fa..f0fe44160 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -113,6 +113,7 @@ public: if (m_num_scopes > 0) { throw default_exception("Cannot translate sat solver at non-base level"); } + std::cout << "translate\n"; std::cout.flush(); ast_translation tr(m, dst_m); m_solver.pop_to_base_level(); inc_sat_solver* result = alloc(inc_sat_solver, dst_m, p, is_incremental()); @@ -167,6 +168,7 @@ public: lbool check_sat(unsigned sz, expr * const * assumptions) override { m_solver.pop_to_base_level(); m_core.reset(); + std::cout << "#inconsistent: " << m_solver.inconsistent() << "\n"; if (m_solver.inconsistent()) return l_false; expr_ref_vector _assumptions(m); obj_map asm2fml; @@ -777,6 +779,8 @@ private: } m_core.push_back(e); } + std::cout << "core " << core << "\n"; + std::cout.flush(); } void check_assumptions(dep2asm_t& dep2asm) { From 7335b3bf565a0c6a50bd98c21fab67bee0ff810b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Sep 2018 16:53:15 -0700 Subject: [PATCH 21/22] remove debug Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index f0fe44160..097d3f0fa 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -113,7 +113,6 @@ public: if (m_num_scopes > 0) { throw default_exception("Cannot translate sat solver at non-base level"); } - std::cout << "translate\n"; std::cout.flush(); ast_translation tr(m, dst_m); m_solver.pop_to_base_level(); inc_sat_solver* result = alloc(inc_sat_solver, dst_m, p, is_incremental()); @@ -168,7 +167,6 @@ public: lbool check_sat(unsigned sz, expr * const * assumptions) override { m_solver.pop_to_base_level(); m_core.reset(); - std::cout << "#inconsistent: " << m_solver.inconsistent() << "\n"; if (m_solver.inconsistent()) return l_false; expr_ref_vector _assumptions(m); obj_map asm2fml; @@ -779,8 +777,6 @@ private: } m_core.push_back(e); } - std::cout << "core " << core << "\n"; - std::cout.flush(); } void check_assumptions(dep2asm_t& dep2asm) { From af41255a9d01e50e328900dbbaeb48959e5d779c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 25 Sep 2018 10:00:13 -0700 Subject: [PATCH 22/22] fix regression in model generation for UFLRA Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 41 +++++++++++++++++++++++++---------------- 1 file changed, 25 insertions(+), 16 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index ca59a2c27..5b1de851e 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -218,6 +218,8 @@ class theory_lra::imp { mutable std::unordered_map m_variable_values; // current model lp::var_index m_one_var; lp::var_index m_zero_var; + lp::var_index m_rone_var; + lp::var_index m_rzero_var; enum constraint_source { inequality_source, @@ -333,11 +335,11 @@ class theory_lra::imp { } } - void add_const(int c, lp::var_index& var) { + lp::var_index add_const(int c, lp::var_index& var, bool is_int) { if (var != UINT_MAX) { - return; + return var; } - app_ref cnst(a.mk_int(c), m); + app_ref cnst(a.mk_numeral(rational(c), is_int), m); TRACE("arith", tout << "add " << cnst << "\n";); enode* e = mk_enode(cnst); theory_var v = mk_var(cnst); @@ -347,16 +349,15 @@ class theory_lra::imp { m_var_trail.push_back(v); add_def_constraint(m_solver->add_var_bound(var, lp::GE, rational(c))); add_def_constraint(m_solver->add_var_bound(var, lp::LE, rational(c))); + return var; } - lp::var_index get_one() { - add_const(1, m_one_var); - return m_one_var; + lp::var_index get_one(bool is_int) { + return add_const(1, is_int ? m_one_var : m_rone_var, is_int); } - lp::var_index get_zero() { - add_const(0, m_zero_var); - return m_zero_var; + lp::var_index get_zero(bool is_int) { + return add_const(0, is_int ? m_zero_var : m_rzero_var, is_int); } @@ -577,6 +578,7 @@ class theory_lra::imp { } enode * mk_enode(app * n) { + TRACE("arith", tout << expr_ref(n, m) << "\n";); if (ctx().e_internalized(n)) { return get_enode(n); } @@ -777,6 +779,7 @@ class theory_lra::imp { } theory_var internalize_def(app* term, scoped_internalize_state& st) { + TRACE("arith", tout << expr_ref(term, m) << "\n";); if (ctx().e_internalized(term)) { IF_VERBOSE(0, verbose_stream() << "repeated term\n";); return mk_var(term, false); @@ -807,10 +810,10 @@ class theory_lra::imp { return st.vars()[0]; } else if (is_one(st)) { - return get_one(); + return get_one(a.is_int(term)); } else if (is_zero(st)) { - return get_zero(); + return get_zero(a.is_int(term)); } else { init_left_side(st); @@ -820,7 +823,7 @@ class theory_lra::imp { if (vi == UINT_MAX) { rational const& offset = st.offset(); if (!offset.is_zero()) { - m_left_side.push_back(std::make_pair(offset, get_one())); + m_left_side.push_back(std::make_pair(offset, get_one(a.is_int(term)))); } SASSERT(!m_left_side.empty()); vi = m_solver->add_term(m_left_side); @@ -854,6 +857,8 @@ public: m_internalize_head(0), m_one_var(UINT_MAX), m_zero_var(UINT_MAX), + m_rone_var(UINT_MAX), + m_rzero_var(UINT_MAX), m_not_handled(nullptr), m_asserted_qhead(0), m_assume_eq_head(0), @@ -925,16 +930,18 @@ public: } return true; } + + bool is_arith(enode* n) { + return n && n->get_th_var(get_id()) != null_theory_var; + } void internalize_eq_eh(app * atom, bool_var) { + TRACE("arith_verbose", tout << mk_pp(atom, m) << "\n";); expr* lhs = nullptr, *rhs = nullptr; VERIFY(m.is_eq(atom, lhs, rhs)); enode * n1 = get_enode(lhs); enode * n2 = get_enode(rhs); - if (n1->get_th_var(get_id()) != null_theory_var && - n2->get_th_var(get_id()) != null_theory_var && - n1 != n2) { - TRACE("arith_verbose", tout << mk_pp(atom, m) << "\n";); + if (is_arith(n1) && is_arith(n2) && n1 != n2) { m_arith_eq_adapter.mk_axioms(n1, n2); } } @@ -1301,6 +1308,7 @@ public: void init_variable_values() { reset_variable_values(); if (!m.canceled() && m_solver.get() && th.get_num_vars() > 0) { + TRACE("arith", tout << "update variable values\n";); m_solver->get_model(m_variable_values); } } @@ -3002,6 +3010,7 @@ public: if (!can_get_bound(v)) return false; lp::var_index vi = m_theory_var2var_index[v]; if (m_solver->has_value(vi, val)) { + TRACE("arith", tout << expr_ref(n->get_owner(), m) << " := " << val << "\n";); if (is_int(n) && !val.is_int()) return false; return true; }