From ed19af4c4e7fc2d4387650c7c0087ccbfa5a7d63 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 Sep 2018 09:02:37 -0700 Subject: [PATCH 1/7] 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 2/7] 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 3/7] 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 4/7] 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 5/7] 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 39ed27101ed9f465504f4e12e2bd2f676ea66fda Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 20 Sep 2018 19:56:55 -0700 Subject: [PATCH 6/7] 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 7/7] 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;