mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

introduce factor

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-11-28 09:50:11 -08:00 • committed by Lev Nachmanson
parent c5c89704a6
commit f211be1e49
2 changed files with 45 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -15,7 +15,7 @@ void const_iterator_mon::init_vars_by_the_mask(unsigned_vector & k_vars, unsigne
}
}
bool const_iterator_mon::get_factors(unsigned& k, unsigned& j, rational& sign) const {
bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const {
unsigned_vector k_vars;
unsigned_vector j_vars;
init_vars_by_the_mask(k_vars, j_vars);
@ -23,27 +23,29 @@ bool const_iterator_mon::get_factors(unsigned& k, unsigned& j, rational& sign) c
std::sort(k_vars.begin(), k_vars.end());
std::sort(j_vars.begin(), j_vars.end());
rational k_sign, j_sign;
monomial m;
if (k_vars.size() == 1) {
k = k_vars[0];
k_sign = 1;
k.index() = k_vars[0];
k.type() = factor_type::VAR;
} else {
if (!m_ff->find_monomial_of_vars(k_vars, m, k_sign)) {
unsigned i;
if (!m_ff->find_monomial_of_vars(k_vars,i)) {
return false;
}
k = m.var();
k.index() = i;
k.type() = factor_type::RM;
}
if (j_vars.size() == 1) {
j = j_vars[0];
j_sign = 1;
j.index() = j_vars[0];
j.type() = factor_type::VAR;
} else {
if (!m_ff->find_monomial_of_vars(j_vars, m, j_sign)) {
unsigned i;
if (!m_ff->find_monomial_of_vars(j_vars,i)) {
return false;
}
j = m.var();
j.index() = i;
j.type() = factor_type::RM;
}
sign = j_sign * k_sign;
return true;
}
@ -51,7 +53,7 @@ const_iterator_mon::reference const_iterator_mon::operator*() const {
if (m_full_factorization_returned == false) {
return create_full_factorization();
}
unsigned j, k; rational sign;
factor j, k; rational sign;
if (!get_factors(j, k, sign))
return factorization();
return create_binary_factorization(j, k);
@ -90,7 +92,7 @@ bool const_iterator_mon::operator==(const const_iterator_mon::self_type &other)
}
bool const_iterator_mon::operator!=(const const_iterator_mon::self_type &other) const { return !(*this == other); }
factorization const_iterator_mon::create_binary_factorization(lpvar j, lpvar k) const {
factorization const_iterator_mon::create_binary_factorization(factor j, factor k) const {
// todo : the current explanation is an overkill
// std::function<void (expl_set&)> explain = [&](expl_set& exp){
// const imp & impl = m_ff->m_impf;
@ -105,14 +107,17 @@ factorization const_iterator_mon::create_binary_factorization(lpvar j, lpvar k)
// impl.add_explanation_of_reducing_to_rooted_monomial(m_ff->m_mon, exp);
// };
factorization f;
f.vars().push_back(j);
f.vars().push_back(k);
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;
// f.vars() = m_ff->m_vars;
for (lpvar j : m_ff->m_vars) {
f.push_back(factor(j, factor_type::VAR));
}
return f;
}
}

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

@ -26,16 +26,30 @@ namespace nla {
struct factorization_factory;
typedef unsigned lpvar;
enum class factor_type { VAR, RM}; // RM stands for rooted monomial
class factor {
unsigned m_index;
factor_type m_type;
public:
factor() {}
factor(unsigned i, factor_type t) : m_index(i), m_type(t) {}
unsigned index() const {return m_index;}
unsigned& index() {return m_index;}
factor_type type() const {return m_type;}
factor_type& type() {return m_type;}
};
class factorization {
svector<lpvar> m_vars;
vector<factor> m_vars;
public:
bool is_empty() const { return m_vars.empty(); }
svector<lpvar> & vars() { return m_vars; }
const svector<lpvar> & vars() const { return m_vars; }
unsigned operator[](unsigned k) const { return m_vars[k]; }
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 lpvar* begin() const { return m_vars.begin(); }
const lpvar* end() const { return m_vars.end(); }
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);}
};
struct const_iterator_mon {
@ -53,7 +67,7 @@ struct const_iterator_mon {
void init_vars_by_the_mask(unsigned_vector & k_vars, unsigned_vector & j_vars) const;
bool get_factors(unsigned& k, unsigned& j, rational& sign) const;
bool get_factors(factor& k, factor& j, rational& sign) const;
reference operator*() const;
void advance_mask();
@ -66,7 +80,7 @@ struct const_iterator_mon {
bool operator==(const self_type &other) const;
bool operator!=(const self_type &other) const;
factorization create_binary_factorization(lpvar j, lpvar k) const;
factorization create_binary_factorization(factor j, factor k) const;
factorization create_full_factorization() const;
};
@ -74,7 +88,7 @@ struct const_iterator_mon {
struct factorization_factory {
const svector<lpvar>& m_vars;
// returns true if found
virtual bool find_monomial_of_vars(const svector<lpvar>& vars, monomial& m, rational & sign) const = 0;
virtual bool find_monomial_of_vars(const svector<lpvar>& vars, unsigned& i) const = 0;
factorization_factory(const svector<lpvar>& vars) :
m_vars(vars) {