mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 06:39:02 +00:00
Code Activity

simplify m_monomials_by_abs_vals

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-11-21 12:17:29 -08:00 committed by Lev Nachmanson
parent e4cbe980e9
commit 2d144cd774
2 changed files with 38 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -344,16 +344,36 @@ struct solver::imp {
mk_ineq(m_monomials[i].var(), -sign, m_monomials[k].var(), lp::lconstraint_kind::EQ);
TRACE("nla_solver", print_lemma(tout););
}
static int rat_sign(const rational& r) {
return r.is_pos()? 1 : ( r.is_neg()? -1 : 0);
}
int vars_sign(const svector<lpvar>& v) {
int sign = 1;
for (lpvar j : v) {
sign *= rat_sign(vvr(j));
if (sign == 0)
return 0;
}
return sign;
}
bool basic_sign_lemma_on_a_bucket_of_abs_vals(const vector<rational>& abs_vals, const vector<index_with_sign>& list){
rational sign = list[0].m_sign;
rational val = vvr(m_monomials[list[0].m_i].var());
bool basic_sign_lemma_on_a_bucket_of_abs_vals(const vector<rational>& abs_vals, const unsigned_vector& list){
rational val = vvr(m_monomials[list[0]].var());
int sign = vars_sign(m_monomials[list[0]].vars());
if (sign == 0) {
return false;
}
for (unsigned i = 1; i < list.size(); i++) {
rational other_sign = list[i].m_sign;
rational other_val = vvr(m_monomials[list[i].m_i].var());
if (val * sign != other_val * other_sign) {
generate_sign_lemma(abs_vals, list[0].m_i, list[i].m_i, sign * other_sign);
rational rsign = rational(vars_sign(m_monomials[list[i]].vars()) * sign);
SASSERT(!rsign.is_zero());
rational other_val = vvr(m_monomials[list[i]].var());
if (val * rsign != other_val) {
generate_sign_lemma(abs_vals, list[0], list[i], rsign);
return true;
}
}
@ -920,6 +940,7 @@ struct solver::imp {
unsigned i_bd_equiv,
unsigned i_bd,
unsigned d, unsigned i_ac, const factorization& ac, unsigned k) {
return false;
}
@ -931,6 +952,8 @@ struct solver::imp {
bool order_lemma_on_factor_equiv_and_other_mon_eq(unsigned i_bd_equiv,
unsigned i_bd,
unsigned d, unsigned i_ac, const factorization& ac, unsigned k) {
return false;
/*
TRACE("nla_solver", tout << "i_bd_equiv = "; print_monomial_with_vars(i_bd_equiv, tout); );
rational abs_d = abs(vvr(d));
for (unsigned k = 0; k < m_monomials[i_bd_equiv].size(); k++) {
@ -947,7 +970,7 @@ struct solver::imp {
return true;
}
}
return false;
return false;*/
}

17
src/util/lp/vars_equivalence.h
View file

@ -82,9 +82,8 @@ struct vars_equivalence {
vector<equiv> m_equivs; // all equivalences extracted from constraints
std::unordered_map<rational,unsigned_vector> m_vars_by_abs_values;
std::unordered_map<vector<rational>,
vector<index_with_sign>,
hash_vector>
m_monomials_by_abs_vals;
unsigned_vector,
hash_vector> m_monomials_by_abs_vals;
std::function<rational(lpvar)> m_vvr;
@ -93,7 +92,7 @@ struct vars_equivalence {
vars_equivalence(std::function<rational(lpvar)> vvr) : m_vvr(vvr) {}
const std::unordered_map<vector<rational>,
vector<index_with_sign>,
unsigned_vector,
hash_vector>& monomials_by_abs_values() const {
return m_monomials_by_abs_vals;
}
@ -223,7 +222,7 @@ struct vars_equivalence {
void deregister_monomial_from_abs_vals(const monomial & m, unsigned i){
int sign;
auto key = get_sorted_abs_vals_from_mon(m, sign);
SASSERT(m_monomials_by_abs_vals.find(key)->second.back() == index_with_sign(i, rational(sign)));
SASSERT(m_monomials_by_abs_vals.find(key)->second.back() == i);
m_monomials_by_abs_vals.find(key)->second.pop_back();
}
@ -244,17 +243,15 @@ struct vars_equivalence {
void register_monomial_in_abs_vals(unsigned i, const monomial & m ) {
int sign;
vector<rational> abs_vals = get_sorted_abs_vals_from_mon(m, sign);
index_with_sign ms(i, rational(sign));
auto it = m_monomials_by_abs_vals.find(abs_vals);
if (it == m_monomials_by_abs_vals.end()) {
vector<index_with_sign> v;
v.push_back(ms);
unsigned_vector v;
v.push_back(i);
// v is a vector containing a single index_with_sign
m_monomials_by_abs_vals.emplace(abs_vals, v);
}
else {
it->second.push_back(ms);
it->second.push_back(i);
}
}