mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

stop keying monomials by abs values

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-03-29 12:39:05 -07:00
parent 086e25b7fa
commit 3f9229a698
2 changed files with 0 additions and 91 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -859,41 +859,6 @@ struct solver::imp {
return true; return true;
} }
void init_abs_val_table() {
// register those vars that a factors in a monomial
for (auto & p : m_monomials_containing_var) {
m_vars_equivalence.register_var_with_abs_val(p.first, vvr(p.first));
}
// register monomial vars too
for (auto & p : m_var_to_its_monomial) {
m_vars_equivalence.register_var_with_abs_val(p.first, vvr(p.first));
}
}
// replaces each var with its abs root and sorts the return vector
template <typename T>
unsigned_vector get_abs_key(const T& m) const {
unsigned_vector r;
for (unsigned j : m) {
r.push_back(m_vars_equivalence.get_abs_root_for_var(abs(vvr(j))));
}
std::sort(r.begin(), r.end());
return r;
}
// For each monomial m = m_monomials[i], where i is in m_to_refine,
// try adding the pair (get_abs_key(m), i) to map
std::unordered_map<unsigned_vector, unsigned, hash_svector> create_relevant_abs_keys() {
std::unordered_map<unsigned_vector, unsigned, hash_svector> r;
for (unsigned i : m_to_refine) {
unsigned_vector key = get_abs_key(m_monomials[i]);
if (contains(r, key))
continue;
r[key] = i;
}
return r;
}
void basic_sign_lemma_model_based_one_mon(const monomial& m, int product_sign) { void basic_sign_lemma_model_based_one_mon(const monomial& m, int product_sign) {
if (product_sign == 0) { if (product_sign == 0) {
TRACE("nla_solver_bl", tout << "zero product sign\n";); TRACE("nla_solver_bl", tout << "zero product sign\n";);
@ -909,9 +874,6 @@ struct solver::imp {
} }
bool basic_sign_lemma_model_based() { bool basic_sign_lemma_model_based() {
init_abs_val_table();
std::unordered_map<unsigned_vector, unsigned, hash_svector> key_mons =
create_relevant_abs_keys();
unsigned i = random() % m_to_refine.size(); unsigned i = random() % m_to_refine.size();
unsigned ii = i; unsigned ii = i;
do { do {
@ -2239,17 +2201,6 @@ struct solver::imp {
} }
} }
vector<factor> factors_with_the_same_abs_val(const factor& c) const {
vector<factor> r;
std::unordered_set<lpvar> found_vars;
std::unordered_set<unsigned> found_rm;
TRACE("nla_solver", tout << "c = "; print_factor_with_vars(c, tout););
for (lpvar i : m_vars_equivalence.get_vars_with_the_same_abs_val(vvr(c))) {
maybe_add_a_factor(i, c, found_vars, found_rm, r);
}
return r;
}
bool order_lemma_on_ac_explore(const rooted_mon& rm, const factorization& ac, unsigned k) { bool order_lemma_on_ac_explore(const rooted_mon& rm, const factorization& ac, unsigned k) {
const factor c = ac[k]; const factor c = ac[k];
TRACE("nla_solver", tout << "c = "; print_factor_with_vars(c, tout); ); TRACE("nla_solver", tout << "c = "; print_factor_with_vars(c, tout); );

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

@ -64,7 +64,6 @@ struct vars_equivalence {
// If m_tree[v] == -1 then the variable is a root. // If m_tree[v] == -1 then the variable is a root.
// if m_tree[v] is not equal to -1 then m_equivs[m_tree[v]] = (k, v) or (v, k), where k is the parent of v // if m_tree[v] is not equal to -1 then m_equivs[m_tree[v]] = (k, v) or (v, k), where k is the parent of v
vector<equiv> m_equivs; // all equivalences extracted from constraints vector<equiv> m_equivs; // all equivalences extracted from constraints
std::unordered_map<rational, unsigned_vector> m_vars_by_abs_values;
std::function<rational(lpvar)> m_vvr; std::function<rational(lpvar)> m_vvr;
@ -74,14 +73,6 @@ struct vars_equivalence {
void clear() { void clear() {
m_equivs.clear(); m_equivs.clear();
m_tree.clear(); m_tree.clear();
m_vars_by_abs_values.clear();
}
const svector<lpvar>& get_vars_with_the_same_abs_val(const rational& v) const {
auto it = m_vars_by_abs_values.find(abs(v));
SASSERT (it != m_vars_by_abs_values.end());
TRACE("nla_solver", tout << "size of same_abs_vals = " << it->second.size(); );
return it->second;
} }
// j itself is also included // j itself is also included
@ -256,38 +247,5 @@ struct vars_equivalence {
explain(j, exp); explain(j, exp);
} }
lpvar get_abs_root_for_var(const rational & v) const {
SASSERT(!v.is_neg());
lpvar j = *(m_vars_by_abs_values.find(v)->second.begin());
SASSERT(abs(m_vvr(j)) == v);
return j;
}
void register_var_with_abs_val(unsigned j, const rational& val) {
TRACE("nla_vars_eq", tout << "j = " << j;);
rational v = abs(val);
auto it = m_vars_by_abs_values.find(v);
if (it == m_vars_by_abs_values.end()) {
unsigned_vector uv;
uv.push_back(j);
m_vars_by_abs_values[v] = uv;
} else {
it->second.push_back(j);
}
}
vector<rational> get_sorted_abs_vals_from_mon(const monomial& m, int & sign) {
sign = 1;
vector<rational> abs_vals;
for (lpvar j : m) {
const rational v = m_vvr(j);
abs_vals.push_back(abs(v));
if (v.is_neg()) {
sign = -sign;
}
}
std::sort(abs_vals.begin(), abs_vals.end());
return abs_vals;
}
}; // end of vars_equivalence }; // end of vars_equivalence
} }