diff --git a/src/util/lp/factorization.cpp b/src/util/lp/factorization.cpp index 1553b7363..dddc2fa1b 100644 --- a/src/util/lp/factorization.cpp +++ b/src/util/lp/factorization.cpp @@ -51,11 +51,11 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const factorization const_iterator_mon::operator*() const { if (m_full_factorization_returned == false) { - return create_full_factorization(); + return create_full_factorization(m_ff->m_monomial); } factor j, k; rational sign; if (!get_factors(j, k, sign)) - return factorization(); + return factorization(nullptr); return create_binary_factorization(j, k); } @@ -82,7 +82,7 @@ const_iterator_mon::self_type const_iterator_mon::operator++(int) { advance_mask const_iterator_mon::const_iterator_mon(const svector& mask, const factorization_factory *f) : m_mask(mask), m_ff(f) , - m_full_factorization_returned(mask.size() == 1) // if mask.size() is equal to 1 the full factorization is not needed + m_full_factorization_returned(false) {} bool const_iterator_mon::operator==(const const_iterator_mon::self_type &other) const { @@ -106,19 +106,21 @@ factorization const_iterator_mon::create_binary_factorization(factor j, factor k // impl.add_explanation_of_reducing_to_rooted_monomial(m_ff->m_mon, exp); // }; - factorization f; + factorization f(nullptr); f.push_back(j); f.push_back(k); return f; } -factorization const_iterator_mon::create_full_factorization() const { - factorization f; - // f.vars() = m_ff->m_vars; +factorization const_iterator_mon::create_full_factorization(const monomial* m) const { + if (m != nullptr) + return factorization(m); + factorization f(nullptr); for (lpvar j : m_ff->m_vars) { f.push_back(factor(j, factor_type::VAR)); } return f; } + } diff --git a/src/util/lp/factorization.h b/src/util/lp/factorization.h index 05e78442a..0a1188621 100644 --- a/src/util/lp/factorization.h +++ b/src/util/lp/factorization.h @@ -54,21 +54,32 @@ inline bool operator!=(const factor& a, const factor& b) { class factorization { vector m_vars; + const monomial* m_mon; public: + factorization(const monomial* m): m_mon(m) { + if (m != nullptr) { + for(lpvar j : *m) + m_vars.push_back(factor(j, factor_type::VAR)); + } + } + bool is_mon() const { return m_mon != nullptr;} bool is_empty() const { return m_vars.empty(); } - const vector & vars() const { return m_vars; } factor operator[](unsigned k) const { return m_vars[k]; } size_t size() const { return m_vars.size(); } const factor* begin() const { return m_vars.begin(); } const factor* end() const { return m_vars.end(); } - void push_back(factor v) {m_vars.push_back(v);} + void push_back(factor v) { + SASSERT(!is_mon()); + m_vars.push_back(v); + } + const monomial* mon() const { return m_mon; } }; struct const_iterator_mon { // fields - svector m_mask; + svector m_mask; const factorization_factory * m_ff; - bool m_full_factorization_returned; + bool m_full_factorization_returned; //typedefs typedef const_iterator_mon self_type; @@ -93,23 +104,34 @@ struct const_iterator_mon { factorization create_binary_factorization(factor j, factor k) const; - factorization create_full_factorization() const; + factorization create_full_factorization(const monomial*) const; }; struct factorization_factory { const svector& m_vars; + const monomial* m_monomial; // returns true if found virtual bool find_rm_monomial_of_vars(const svector& vars, unsigned& i) const = 0; + virtual const monomial* find_monomial_of_vars(const svector& vars) const = 0; + - factorization_factory(const svector& vars) : - m_vars(vars) { + factorization_factory(const svector& vars, const monomial* m) : + m_vars(vars), m_monomial(m) { } - const_iterator_mon begin() const { + svector get_mask() const { // we keep the last element always in the first factor to avoid - // repeating a pair twice - svector mask(m_vars.size() - 1, false); - return const_iterator_mon(mask, this); + // repeating a pair twice, that is why m_mask is shorter by one then m_vars + + return + m_vars.size() != 2? + svector(m_vars.size() - 1, false) + : + svector(1, true); // init mask as in the end() since the full iteration will do the job + } + + const_iterator_mon begin() const { + return const_iterator_mon(get_mask(), this); } const_iterator_mon end() const { diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 8f44816b1..4f146218b 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -1060,16 +1060,29 @@ struct solver::imp { return true; } + const monomial* find_monomial_of_vars(const svector& vars) const { + unsigned i; + if (!find_rm_monomial_of_vars(vars, i)) + return nullptr; + return &m_monomials[m_rm_table.rms()[i].orig_index()]; + } + struct factorization_factory_imp: factorization_factory { const imp& m_imp; + const monomial *m_mon; + const rooted_mon& m_rm; - factorization_factory_imp(const svector& m_vars, const imp& s) : - factorization_factory(m_vars), - m_imp(s) { } + factorization_factory_imp(const rooted_mon& rm, const imp& s) : + factorization_factory(rm.m_vars, &s.m_monomials[rm.orig_index()]), + m_imp(s), m_mon(& s.m_monomials[rm.orig_index()]), m_rm(rm) { } bool find_rm_monomial_of_vars(const svector& vars, unsigned & i) const { return m_imp.find_rm_monomial_of_vars(vars, i); } + const monomial* find_monomial_of_vars(const svector& vars) const { + return m_imp.find_monomial_of_vars(vars); + } + }; // here we use the fact // xy = 0 -> x = 0 or y = 0 @@ -1163,7 +1176,15 @@ struct solver::imp { current_expl().add(m_lar_solver.get_column_lower_bound_witness(j)); } // x = 0 or y = 0 -> xy = 0 - bool basic_lemma_for_mon_non_zero_model_based(const rooted_mon& rm, const factorization& f) { + void basic_lemma_for_mon_non_zero_model_based(const rooted_mon& rm, const factorization& f) { + TRACE("nla_solver_bl", trace_print_monomial_and_factorization(rm, f, tout);); + if (f.is_mon()) + basic_lemma_for_mon_non_zero_model_based_mf(f); + else + basic_lemma_for_mon_non_zero_model_based_mf(f); + } + // x = 0 or y = 0 -> xy = 0 + void basic_lemma_for_mon_non_zero_model_based_rm(const rooted_mon& rm, const factorization& f) { TRACE("nla_solver_bl", trace_print_monomial_and_factorization(rm, f, tout);); SASSERT (!vvr(rm).is_zero()); int zero_j = -1; @@ -1174,16 +1195,30 @@ struct solver::imp { } } - if (zero_j == -1) { - return false; - } + if (zero_j == -1) { return; } add_empty_lemma(); mk_ineq(zero_j, llc::NE); mk_ineq(var(rm), llc::EQ); - explain(rm, current_expl()); + explain(f, current_expl()); + TRACE("nla_solver", print_lemma(tout);); + } + + void basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f) { + TRACE("nla_solver_bl", print_factorization(f, tout);); + int zero_j = -1; + for (auto j : f) { + if (vvr(j).is_zero()) { + zero_j = var(j); + break; + } + } + + if (zero_j == -1) { return; } + add_empty_lemma(); + mk_ineq(zero_j, llc::NE); + mk_ineq(f.mon()->var(), llc::EQ); TRACE("nla_solver", print_lemma(tout);); - return true; } bool var_has_positive_lower_bound(lpvar j) const { @@ -1579,14 +1614,14 @@ struct solver::imp { void basic_lemma_for_mon_model_based(const rooted_mon& rm) { TRACE("nla_solver_bl", tout << "rm = "; print_rooted_monomial(rm, tout);); if (vvr(rm).is_zero()) { - for (auto factorization : factorization_factory_imp(rm.m_vars, *this)) { + for (auto factorization : factorization_factory_imp(rm, *this)) { if (factorization.is_empty()) continue; basic_lemma_for_mon_zero_model_based(rm, factorization); basic_lemma_for_mon_neutral_model_based(rm, factorization); } } else { - for (auto factorization : factorization_factory_imp(rm.m_vars, *this)) { + for (auto factorization : factorization_factory_imp(rm, *this)) { if (factorization.is_empty()) continue; basic_lemma_for_mon_non_zero_model_based(rm, factorization); @@ -1598,7 +1633,7 @@ struct solver::imp { bool basic_lemma_for_mon_derived(const rooted_mon& rm) { if (var_is_fixed_to_zero(var(rm))) { - for (auto factorization : factorization_factory_imp(rm.m_vars, *this)) { + for (auto factorization : factorization_factory_imp(rm, *this)) { if (factorization.is_empty()) continue; if (basic_lemma_for_mon_zero(rm, factorization) || @@ -1608,7 +1643,7 @@ struct solver::imp { } } } else { - for (auto factorization : factorization_factory_imp(rm.m_vars, *this)) { + for (auto factorization : factorization_factory_imp(rm, *this)) { if (factorization.is_empty()) continue; if (basic_lemma_for_mon_non_zero_derived(rm, factorization) || @@ -2260,7 +2295,7 @@ struct solver::imp { tout << "rm = "; print_product(rm, tout); tout << ", orig = "; print_monomial(m_monomials[rm.orig_index()], tout); ); - for (auto ac : factorization_factory_imp(rm.vars(), *this)) { + for (auto ac : factorization_factory_imp(rm, *this)) { if (ac.size() != 2) continue; order_lemma_on_factorization(rm, ac); @@ -2599,7 +2634,7 @@ struct solver::imp { } bool find_bfc_on_monomial(const rooted_mon& rm, bfc & bf) { - for (auto factorization : factorization_factory_imp(rm.m_vars, *this)) { + for (auto factorization : factorization_factory_imp(rm, *this)) { if (factorization.size() == 2) { lpvar a = var(factorization[0]); lpvar b = var(factorization[1]); @@ -2924,23 +2959,23 @@ struct solver::imp { return true; } - void test_factorization(unsigned mon_index, unsigned number_of_factorizations) { - vector lemma; + void test_factorization(unsigned /*mon_index*/, unsigned /*number_of_factorizations*/) { + // vector lemma; - unsigned_vector vars = m_monomials[mon_index].vars(); + // unsigned_vector vars = m_monomials[mon_index].vars(); - factorization_factory_imp fc(vars, // 0 is the index of "abcde" - *this); + // factorization_factory_imp fc(vars, // 0 is the index of "abcde" + // *this); - std::cout << "factorizations = of "; print_monomial(m_monomials[mon_index], std::cout) << "\n"; - unsigned found_factorizations = 0; - for (auto f : fc) { - if (f.is_empty()) continue; - found_factorizations ++; - print_factorization(f, std::cout); - std::cout << std::endl; - } - SASSERT(found_factorizations == number_of_factorizations); + // std::cout << "factorizations = of "; print_monomial(m_monomials[mon_index], std::cout) << "\n"; + // unsigned found_factorizations = 0; + // for (auto f : fc) { + // if (f.is_empty()) continue; + // found_factorizations ++; + // print_factorization(f, std::cout); + // std::cout << std::endl; + // } + // SASSERT(found_factorizations == number_of_factorizations); } lbool test_check(