From 0644194fc96a853df44c37f9e4522796aa40add8 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 30 Aug 2018 18:58:26 +0800 Subject: [PATCH] work on lemma from product to factors, and some renaming Signed-off-by: Lev Nachmanson --- src/util/lp/hnf_cutter.h | 2 +- src/util/lp/int_solver.cpp | 2 +- src/util/lp/lar_solver.cpp | 2 +- src/util/lp/lar_term.h | 4 +-- src/util/lp/niil_solver.cpp | 70 ++++++++++++++++++++----------------- 5 files changed, 43 insertions(+), 37 deletions(-) diff --git a/src/util/lp/hnf_cutter.h b/src/util/lp/hnf_cutter.h index b70af3aff..74ee47d35 100644 --- a/src/util/lp/hnf_cutter.h +++ b/src/util/lp/hnf_cutter.h @@ -164,7 +164,7 @@ public: void fill_term(const vector & row, lar_term& t) { for (unsigned j = 0; j < row.size(); j++) { if (!is_zero(row[j])) - t.add_monomial(row[j], m_var_register.local_to_external(j)); + t.add_coeff_var(row[j], m_var_register.local_to_external(j)); } } #ifdef Z3DEBUG diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp index 977b7aa84..4814748bb 100644 --- a/src/util/lp/int_solver.cpp +++ b/src/util/lp/int_solver.cpp @@ -999,7 +999,7 @@ 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(j != -1); - m_t.add_monomial(mpq(1), m_lar_solver->adjust_column_index_to_term_index(j)); + m_t->add_coeff_var(mpq(1), m_lar_solver->adjust_column_index_to_term_index(j)); if (is_free(j)) { m_upper = true; m_k = mpq(0); diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 08046fdde..c5520507c 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -587,7 +587,7 @@ lar_term lar_solver::get_term_to_maximize(unsigned j_or_term) const { } if (j_or_term < m_mpq_lar_core_solver.m_r_x.size()) { lar_term r; - r.add_monomial(one_of_type(), j_or_term); + r.add_coeff_var(one_of_type(), j_or_term); return r; } return lar_term(); // return an empty term diff --git a/src/util/lp/lar_term.h b/src/util/lp/lar_term.h index 7ce1e3f88..d7bc8261e 100644 --- a/src/util/lp/lar_term.h +++ b/src/util/lp/lar_term.h @@ -54,7 +54,7 @@ public: lar_term(const vector>& coeffs) { for (const auto & p : coeffs) { - add_monomial(p.first, p.second); + add_coeff_var(p.first, p.second); } } bool operator==(const lar_term & a) const { return false; } // take care not to create identical terms @@ -76,7 +76,7 @@ public: if (it == nullptr) return; const mpq & b = it->get_data().m_value; for (unsigned it_j :li.m_index) { - add_monomial(- b * li.m_data[it_j], it_j); + add_coeff_var(- b * li.m_data[it_j], it_j); } m_coeffs.erase(j); } diff --git a/src/util/lp/niil_solver.cpp b/src/util/lp/niil_solver.cpp index d14d2e37e..a15c7c5e8 100644 --- a/src/util/lp/niil_solver.cpp +++ b/src/util/lp/niil_solver.cpp @@ -106,7 +106,7 @@ struct vars_equivalence { m_equivs.push_back(equiv(i, j, sign, c0, c1)); } - // we look for octagon constraints here : x - y = 0, x + y = 0, - x - y = 0 , etc. + // we look for octagon constraints here, with a left part +-x +- y void collect_equivs(const lp::lar_solver& s) { for (unsigned i = 0; i < s.terms().size(); i++) { unsigned ti = i + s.terms_start_index(); @@ -184,13 +184,6 @@ struct solver::imp { typedef lp::lar_base_constraint lpcon; - struct var_lists { - svector m_monomials; // of the var - const svector& mons() const { return m_monomials;} - svector& mons() { return m_monomials;} - void add_monomial(unsigned i) { mons().push_back(i); } - }; - struct mono_index_with_sign { unsigned m_i; // the monomial index int m_sign; // the monomial sign: -1 or 1 @@ -205,7 +198,7 @@ struct solver::imp { m_minimal_monomials; unsigned_vector m_monomials_lim; lp::lar_solver& m_lar_solver; - std::unordered_map m_var_lists; + std::unordered_map> m_var_lists; lp::explanation * m_expl; lemma * m_lemma; imp(lp::lar_solver& s, reslimit& lim, params_ref const& p) @@ -304,8 +297,8 @@ struct solver::imp { m_lar_solver.print_constraint(p.second, tout); tout << "\n"; ); lp::lar_term t; - t.add_monomial(rational(1), a.var()); - t.add_monomial(rational(- sign), b.var()); + t.add_coeff_var(rational(1), a.var()); + t.add_coeff_var(rational(- sign), b.var()); TRACE("niil_solver", print_explanation_and_lemma(tout);); ineq in(lp::lconstraint_kind::NE, t); m_lemma->push_back(in); @@ -317,7 +310,7 @@ struct solver::imp { bool generate_basic_lemma_for_mon_sign_var(unsigned i_mon, unsigned j_var, const svector& mon_vars, int sign) { auto it = m_var_lists.find(j_var); - for (auto other_i_mon : it->second.mons()) { + for (auto other_i_mon : it->second) { if (other_i_mon == i_mon) continue; if (generate_basic_lemma_for_mon_sign_var_other_mon( i_mon, @@ -478,7 +471,7 @@ struct solver::imp { return false; } lp::lar_term t; - t.add_monomial(rational(1), m_monomials[i_mon].var()); + t.add_coeff_var(rational(1), m_monomials[i_mon].var()); t.m_v = -rs; ineq in(kind, t); m_lemma->push_back(in); @@ -505,7 +498,7 @@ struct solver::imp { ineq ineq_j_is_equal_to_zero(lpvar j) const { lp::lar_term t; - t.add_monomial(rational(1), j); + t.add_coeff_var(rational(1), j); ineq i(lp::lconstraint_kind::EQ, t); return i; } @@ -725,8 +718,8 @@ struct solver::imp { add_explanation_of_one(ones_of_monomial[k]); } lp::lar_term t; - t.add_monomial(rational(1), m.var()); - t.add_monomial(rational(- sign), j); + t.add_coeff_var(rational(1), m.var()); + t.add_coeff_var(rational(- sign), j); ineq in(lp::lconstraint_kind::EQ, t); m_lemma->push_back(in); TRACE("niil_solver", print_explanation_and_lemma(tout);); @@ -801,18 +794,18 @@ struct solver::imp { // j_sign * x[j] < 0 || mon_sign * x[m.var()] < 0 || mon_sign * x[m.var()] >= j_sign * x[j] // the first literal lp::lar_term t; - t.add_monomial(rational(j_sign), j); + t.add_coeff_var(rational(j_sign), j); m_lemma->push_back(ineq(lp::lconstraint_kind::LT, t)); t.clear(); // the second literal - t.add_monomial(rational(mon_sign), m.var()); + t.add_coeff_var(rational(mon_sign), m.var()); m_lemma->push_back(ineq(lp::lconstraint_kind::LT, t)); t.clear(); // the third literal - t.add_monomial(rational(mon_sign), m.var()); - t.add_monomial(- rational(j_sign), j); + t.add_coeff_var(rational(mon_sign), m.var()); + t.add_coeff_var(- rational(j_sign), j); m_lemma->push_back(ineq(lp::lconstraint_kind::GE, t)); } @@ -871,20 +864,19 @@ struct solver::imp { // For this case we would have x[j] < 0 || x[m.var()] < 0 || x[j] >= x[m.var()] // But for the general case we have // j_sign * x[j] < 0 || mon_sign * x[m.var()] < 0 || j_sign * x[j] >= mon_sign * x[m.var] - // the first literal - + lp::lar_term t; // the first literal - t.add_monomial(rational(j_sign), j); + t.add_coeff_var(rational(j_sign), j); m_lemma->push_back(ineq(lp::lconstraint_kind::LT, t)); //the second literal t.clear(); - t.add_monomial(rational(mon_sign), m.var()); + t.add_coeff_var(rational(mon_sign), m.var()); m_lemma->push_back(ineq(lp::lconstraint_kind::LT, t)); // the third literal t.clear(); - t.add_monomial(rational(j_sign), j); - t.add_monomial(- rational(mon_sign), m.var()); + t.add_coeff_var(rational(j_sign), j); + t.add_coeff_var(- rational(mon_sign), m.var()); m_lemma->push_back(ineq(lp::lconstraint_kind::GE, t)); } @@ -978,11 +970,25 @@ struct solver::imp { if (basic_lemma_for_mon_proportionality_from_factors_to_product(i_mon)) return true; - return large_basic_lemma_for_mon_proportionality_from_product_to_factors(i_mon); + return basic_lemma_for_mon_proportionality_from_product_to_factors(i_mon); + } + + struct factors_of_monomial { + vector> m_factors; + factors_of_monomial(unsigned i_mon) {} + + vector>::const_iterator begin() { return m_factors.begin(); } + vector>::const_iterator end() { return m_factors.end(); } + + }; + bool lemma_for_proportional_factors(unsigned i_mon, lpvar a, lpvar b) { + return false; } // we derive a lemma from |xy| > |y| => |x| >= 1 || |y| = 0 - bool large_basic_lemma_for_mon_proportionality_from_product_to_factors(unsigned i_mon) { - // SASSERT(false); + bool basic_lemma_for_mon_proportionality_from_product_to_factors(unsigned i_mon) { + for (std::pair factors : factors_of_monomial(i_mon)) + if (lemma_for_proportional_factors(i_mon, factors.first, factors.second)) + return true; return false; } @@ -1007,12 +1013,12 @@ struct solver::imp { for (lpvar j : m.m_vs) { auto it = m_var_lists.find(j); if (it == m_var_lists.end()) { - var_lists v; - v.add_monomial(i); + svector v; + v.push_back(i); m_var_lists[j] = v; } else { - it->second.add_monomial(i); + it->second.push_back(i); } } }