mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

towards full factorizations on a monomial

Browse source
This commit is contained in:
Lev Nachmanson 2019-03-25 15:43:12 -07:00
parent 1810d7e77d
commit 90bda39aef
3 changed files with 106 additions and 47 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/util/lp/factorization.cpp
View file

@ -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<bool>& 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;
}
}

44
src/util/lp/factorization.h
View file

@ -54,21 +54,32 @@ inline bool operator!=(const factor& a, const factor& b) {
class factorization {
vector<factor> 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<factor> & 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<bool> m_mask;
svector<bool> 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<lpvar>& m_vars;
const monomial* m_monomial;
// returns true if found
virtual bool find_rm_monomial_of_vars(const svector<lpvar>& vars, unsigned& i) const = 0;
virtual const monomial* find_monomial_of_vars(const svector<lpvar>& vars) const = 0;
factorization_factory(const svector<lpvar>& vars) :
m_vars(vars) {
factorization_factory(const svector<lpvar>& vars, const monomial* m) :
m_vars(vars), m_monomial(m) {
}
const_iterator_mon begin() const {
svector<bool> get_mask() const {
// we keep the last element always in the first factor to avoid
// repeating a pair twice
svector<bool> 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<bool>(m_vars.size() - 1, false)
:
svector<bool>(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 {

93
src/util/lp/nla_solver.cpp
View file

@ -1060,16 +1060,29 @@ struct solver::imp {
return true;
}
const monomial* find_monomial_of_vars(const svector<lpvar>& 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<lpvar>& 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<lpvar>& vars, unsigned & i) const {
return m_imp.find_rm_monomial_of_vars(vars, i);
}
const monomial* find_monomial_of_vars(const svector<lpvar>& 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<ineq> lemma;
void test_factorization(unsigned /*mon_index*/, unsigned /*number_of_factorizations*/) {
// vector<ineq> 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(