mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 14:23:40 +00:00
Code Activity

debugging var_eqs

Browse source
This commit is contained in:
Lev Nachmanson 2019-04-03 15:24:55 -07:00
parent 09152013b3
commit 7a3a696b6f
3 changed files with 179 additions and 176 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -34,9 +34,11 @@ bool try_insert(const A& elem, B& collection) {
collection.insert(elem); collection.insert(elem);
return true; return true;
} }
typedef lp::constraint_index lpci; typedef lp::constraint_index lpci;
typedef lp::lconstraint_kind llc; typedef lp::lconstraint_kind llc;
struct point { struct point {
rational x; rational x;
rational y; rational y;
@ -86,7 +88,7 @@ struct solver::imp {
}; };
//fields //fields
var_eqs m_vars_equivalence; var_eqs m_evars;
vector<monomial> m_monomials; vector<monomial> m_monomials;
rooted_mon_table m_rm_table; rooted_mon_table m_rm_table;
@ -114,7 +116,7 @@ struct solver::imp {
imp(lp::lar_solver& s, reslimit& lim, params_ref const& p) imp(lp::lar_solver& s, reslimit& lim, params_ref const& p)
: :
m_vars_equivalence(), m_evars(),
m_lar_solver(s) m_lar_solver(s)
// m_limit(lim), // m_limit(lim),
// m_params(p) // m_params(p)
@ -201,7 +203,7 @@ struct solver::imp {
} }
rational canonize_sign_of_var(lpvar j) const { rational canonize_sign_of_var(lpvar j) const {
return m_vars_equivalence.find_sign(j); return m_evars.find(j).rsign();
} }
// the value of the rooted monomias is equal to the value of the variable multiplied // the value of the rooted monomias is equal to the value of the variable multiplied
@ -222,6 +224,7 @@ struct solver::imp {
void push() { void push() {
TRACE("nla_solver",); TRACE("nla_solver",);
m_monomials_counts.push_back(m_monomials.size()); m_monomials_counts.push_back(m_monomials.size());
m_evars.push();
} }
void deregister_monomial_from_rooted_monomials (const monomial & m, unsigned i){ void deregister_monomial_from_rooted_monomials (const monomial & m, unsigned i){
@ -248,6 +251,7 @@ struct solver::imp {
} }
m_monomials.shrink(new_size); m_monomials.shrink(new_size);
m_monomials_counts.shrink(m_monomials_counts.size() - n); m_monomials_counts.shrink(m_monomials_counts.size() - n);
m_evars.pop(n);
} }
rational mon_value_by_vars(unsigned i) const { rational mon_value_by_vars(unsigned i) const {
@ -287,7 +291,7 @@ struct solver::imp {
} }
void explain(lpvar j, lp::explanation& exp) const { void explain(lpvar j, lp::explanation& exp) const {
m_vars_equivalence.explain(j, exp); m_evars.explain(j, exp);
} }
template <typename T> template <typename T>
@ -616,17 +620,17 @@ struct solver::imp {
// //
svector<lpvar> reduce_monomial_to_rooted(const svector<lpvar> & vars, rational & sign) const { svector<lpvar> reduce_monomial_to_rooted(const svector<lpvar> & vars, rational & sign) const {
svector<lpvar> ret; svector<lpvar> ret;
sign = 1; bool s = false;
for (lpvar v : vars) { for (lpvar v : vars) {
unsigned root = m_vars_equivalence.find(v, sign); auto root = m_evars.find(v);
SASSERT(m_vars_equivalence.is_root(root)); s ^= root.sign();
TRACE("nla_solver_eq", TRACE("nla_solver_eq",
print_var(v,tout); print_var(v,tout);
tout << " mapped to "; tout << " mapped to ";
print_var(root.var(), tout););
print_var(root, tout);); ret.push_back(root.var());
ret.push_back(root);
} }
sign = rational(s? -1: 1);
std::sort(ret.begin(), ret.end()); std::sort(ret.begin(), ret.end());
return ret; return ret;
} }
@ -844,10 +848,10 @@ struct solver::imp {
/* /*
unsigned_vector eq_vars(lpvar j) const { unsigned_vector eq_vars(lpvar j) const {
TRACE("nla_solver_eq", tout << "j = "; print_var(j, tout); tout << "eqs = "; TRACE("nla_solver_eq", tout << "j = "; print_var(j, tout); tout << "eqs = ";
for(auto jj : m_vars_equivalence.eq_vars(j)) { for(auto jj : m_evars.eq_vars(j)) {
print_var(jj, tout); print_var(jj, tout);
}); });
return m_vars_equivalence.eq_vars(j); return m_evars.eq_vars(j);
} }
*/ */
// Monomials m and n vars have the same values, up to "sign" // Monomials m and n vars have the same values, up to "sign"
@ -1091,7 +1095,7 @@ struct solver::imp {
if (!(var_has_positive_lower_bound(j) || var_has_negative_upper_bound(j))) { if (!(var_has_positive_lower_bound(j) || var_has_negative_upper_bound(j))) {
return 0; return 0;
} }
sign *= m_vars_equivalence.find_sign(j); sign *= m_evars.find(j).rsign();
} }
return rat_sign(sign); return rat_sign(sign);
} }
@ -1339,13 +1343,13 @@ struct solver::imp {
bool vars_are_equiv(lpvar a, lpvar b) const { bool vars_are_equiv(lpvar a, lpvar b) const {
SASSERT(abs(vvr(a)) == abs(vvr(b))); SASSERT(abs(vvr(a)) == abs(vvr(b)));
return m_vars_equivalence.vars_are_equiv(a, b); return m_evars.vars_are_equiv(a, b);
} }
void explain_equiv_vars(lpvar a, lpvar b) { void explain_equiv_vars(lpvar a, lpvar b) {
SASSERT(abs(vvr(a)) == abs(vvr(b))); SASSERT(abs(vvr(a)) == abs(vvr(b)));
if (m_vars_equivalence.vars_are_equiv(a, b)) { if (m_evars.vars_are_equiv(a, b)) {
explain(a, current_expl()); explain(a, current_expl());
explain(b, current_expl()); explain(b, current_expl());
} else { } else {
@ -1864,9 +1868,9 @@ struct solver::imp {
auto c2 = m_lar_solver.get_column_upper_bound_witness(v[k]); auto c2 = m_lar_solver.get_column_upper_bound_witness(v[k]);
auto c3 = m_lar_solver.get_column_lower_bound_witness(v[k]); auto c3 = m_lar_solver.get_column_lower_bound_witness(v[k]);
if (vvr(head) == vvr(v[k])) if (vvr(head) == vvr(v[k]))
m_vars_equivalence.merge_plus(head, v[k], eq_justification({c0, c1, c2, c3})); m_evars.merge_plus(head, v[k], eq_justification({c0, c1, c2, c3}));
else else
m_vars_equivalence.merge_minus(head, v[k], eq_justification({c0, c1, c2, c3})); m_evars.merge_minus(head, v[k], eq_justification({c0, c1, c2, c3}));
} }
} }
} }
@ -1895,16 +1899,16 @@ struct solver::imp {
SASSERT(j != static_cast<unsigned>(-1)); SASSERT(j != static_cast<unsigned>(-1));
bool sign = (seen_minus && seen_plus)? false : true; bool sign = (seen_minus && seen_plus)? false : true;
if (sign) if (sign)
m_vars_equivalence.merge_minus(i, j, eq_justification({c0, c1})); m_evars.merge_minus(i, j, eq_justification({c0, c1}));
else else
m_vars_equivalence.merge_plus(i, j, eq_justification({c0, c1})); m_evars.merge_plus(i, j, eq_justification({c0, c1}));
} }
// x is equivalent to y if x = +- y // x is equivalent to y if x = +- y
void init_vars_equivalence() { void init_vars_equivalence() {
/* SASSERT(m_vars_equivalence.empty());*/ /* SASSERT(m_evars.empty());*/
collect_equivs(); collect_equivs();
/* TRACE("nla_solver_details", tout << "number of equivs = " << m_vars_equivalence.size(););*/ /* TRACE("nla_solver_details", tout << "number of equivs = " << m_evars.size(););*/
SASSERT((settings().random_next() % 100) || tables_are_ok()); SASSERT((settings().random_next() % 100) || tables_are_ok());
} }
@ -1932,7 +1936,7 @@ struct solver::imp {
bool rm_table_is_ok() const { bool rm_table_is_ok() const {
for (const auto & rm : m_rm_table.rms()) { for (const auto & rm : m_rm_table.rms()) {
for (lpvar j : rm.vars()) { for (lpvar j : rm.vars()) {
if (!m_vars_equivalence.is_root(j)){ if (!m_evars.is_root(j)){
TRACE("nla_solver", print_var(j, tout);); TRACE("nla_solver", print_var(j, tout););
return false; return false;
} }
@ -1945,7 +1949,7 @@ struct solver::imp {
return vars_table_is_ok() && rm_table_is_ok(); return vars_table_is_ok() && rm_table_is_ok();
} }
bool var_is_a_root(lpvar j) const { return m_vars_equivalence.is_root(j); } bool var_is_a_root(lpvar j) const { return m_evars.is_root(j); }
template <typename T> template <typename T>
bool vars_are_roots(const T& v) const { bool vars_are_roots(const T& v) const {
@ -2244,7 +2248,7 @@ struct solver::imp {
SASSERT(abs(vvr(i)) == abs(vvr(c))); SASSERT(abs(vvr(i)) == abs(vvr(c)));
auto it = m_var_to_its_monomial.find(i); auto it = m_var_to_its_monomial.find(i);
if (it == m_var_to_its_monomial.end()) { if (it == m_var_to_its_monomial.end()) {
i = m_vars_equivalence.find(i); i = m_evars.find(i).var();
if (try_insert(i, found_vars)) { if (try_insert(i, found_vars)) {
r.push_back(factor(i, factor_type::VAR)); r.push_back(factor(i, factor_type::VAR));
} }
@ -2382,7 +2386,7 @@ struct solver::imp {
void order_lemma_on_factor_binomial_explore(const monomial& m, unsigned k) { void order_lemma_on_factor_binomial_explore(const monomial& m, unsigned k) {
SASSERT(m.size() == 2); SASSERT(m.size() == 2);
lpvar c = m[k]; lpvar c = m[k];
lpvar d = m_vars_equivalence.find(c); lpvar d = m_evars.find(c).var();
auto it = m_rm_table.var_map().find(d); auto it = m_rm_table.var_map().find(d);
SASSERT(it != m_rm_table.var_map().end()); SASSERT(it != m_rm_table.var_map().end());
for (unsigned bd_i : it->second) { for (unsigned bd_i : it->second) {
@ -2393,7 +2397,7 @@ struct solver::imp {
} }
void order_lemma_on_factor_binomial_rm(const monomial& ac, unsigned k, const rooted_mon& rm_bd) { void order_lemma_on_factor_binomial_rm(const monomial& ac, unsigned k, const rooted_mon& rm_bd) {
factor d(m_vars_equivalence.find(ac[k]), factor_type::VAR); factor d(m_evars.find(ac[k]).var(), factor_type::VAR);
factor b; factor b;
if (!divide(rm_bd, d, b)) if (!divide(rm_bd, d, b))
return; return;
@ -2407,7 +2411,7 @@ struct solver::imp {
int p = (k + 1) % 2; int p = (k + 1) % 2;
lpvar a = ac[p]; lpvar a = ac[p];
lpvar c = ac[k]; lpvar c = ac[k];
SASSERT(m_vars_equivalence.find(c) == d); SASSERT(m_evars.find(c).var() == d);
rational acv = vvr(ac); rational acv = vvr(ac);
rational av = vvr(a); rational av = vvr(a);
rational c_sign = rrat_sign(vvr(c)); rational c_sign = rrat_sign(vvr(c));

10
src/util/lp/var_eqs.cpp
View file

@ -20,7 +20,6 @@
#include "util/lp/var_eqs.h" #include "util/lp/var_eqs.h"
namespace nla { namespace nla {
@ -40,13 +39,13 @@ namespace nla {
m_eqs[(~sv.first).index()].pop_back(); m_eqs[(~sv.first).index()].pop_back();
m_eqs[(~sv.second).index()].pop_back(); m_eqs[(~sv.second).index()].pop_back();
} }
m_trail_lim.shrink(n); m_trail_lim.shrink(m_trail_lim.size() - n);
m_trail.shrink(old_sz); m_trail.shrink(old_sz);
m_ufctx.get_trail_stack().pop_scope(n); m_ufctx.get_trail_stack().pop_scope(n);
} }
void var_eqs::merge(signed_var v1, signed_var v2, eq_justification const& j) { void var_eqs::merge(signed_var v1, signed_var v2, eq_justification const& j) {
unsigned max_i = std::max(v1.index(), v2.index()) + 1; unsigned max_i = std::max(v1.index(), v2.index()) + 2;
m_eqs.reserve(max_i); m_eqs.reserve(max_i);
while (m_uf.get_num_vars() <= max_i) m_uf.mk_var(); while (m_uf.get_num_vars() <= max_i) m_uf.mk_var();
m_uf.merge(v1.index(), v2.index()); m_uf.merge(v1.index(), v2.index());
@ -62,7 +61,7 @@ namespace nla {
return v; return v;
} }
unsigned idx = m_uf.find(v.index()); unsigned idx = m_uf.find(v.index());
return signed_var(idx); return signed_var(idx, from_index()); // 0 is needed to call the right constructor
} }
void var_eqs::explain(signed_var v1, signed_var v2, lp::explanation& e) const { void var_eqs::explain(signed_var v1, signed_var v2, lp::explanation& e) const {
@ -85,7 +84,7 @@ namespace nla {
auto const& next = m_eqs[v.index()]; auto const& next = m_eqs[v.index()];
unsigned sz = next.size(); unsigned sz = next.size();
bool seen_all = true; bool seen_all = true;
for (unsigned i = f.m_index; !seen_all && i < sz; ++i) { for (unsigned i = f.m_index; seen_all && i < sz; ++i) {
justified_var const& jv = next[i]; justified_var const& jv = next[i];
if (!m_marked[jv.m_var.index()]) { if (!m_marked[jv.m_var.index()]) {
seen_all = false; seen_all = false;
@ -104,6 +103,7 @@ namespace nla {
for (eq_justification const& j : m_dfs_trail) { for (eq_justification const& j : m_dfs_trail) {
j.explain(e); j.explain(e);
} }
m_todo.reset();
m_dfs_trail.reset(); m_dfs_trail.reset();
for (unsigned idx : m_marked_trail) { for (unsigned idx : m_marked_trail) {
m_marked[idx] = false; m_marked[idx] = false;

279
src/util/lp/var_eqs.h
View file

@ -26,157 +26,156 @@
namespace nla { namespace nla {
typedef lp::var_index lpvar; typedef lp::var_index lpvar;
typedef lp::constraint_index lpcindex; typedef lp::constraint_index lpci;
struct from_index{};
class signed_var { class signed_var {
unsigned m_sv; unsigned m_sv;
public: public:
// constructor, sign = true means minus // constructor, sign = true means minus
signed_var(lpvar v, bool sign): m_sv((v << 1) + (sign ? 1 : 0)) {} signed_var(lpvar v, bool sign): m_sv((v << 1) + (sign ? 1 : 0)) {}
// constructor // constructor
explicit signed_var(unsigned sv): m_sv(sv) {} signed_var(unsigned sv, from_index): m_sv(sv) {}
bool sign() const { return 0 != (m_sv & 0x1); } bool sign() const { return 0 != (m_sv & 0x1); }
lpvar var() const { return m_sv >> 1; } lpvar var() const { return m_sv >> 1; }
unsigned index() const { return m_sv; } unsigned index() const { return m_sv; }
void neg() { m_sv = m_sv ^ 1; } void neg() { m_sv = m_sv ^ 1; }
friend signed_var operator~(signed_var const& sv) { friend signed_var operator~(signed_var const& sv) {
return signed_var(sv.var(), !sv.sign()); return signed_var(sv.var(), !sv.sign());
} }
bool operator==(signed_var const& other) const { bool operator==(signed_var const& other) const {
return m_sv == other.m_sv; return m_sv == other.m_sv;
} }
bool operator!=(signed_var const& other) const { bool operator!=(signed_var const& other) const {
return m_sv != other.m_sv; return m_sv != other.m_sv;
} }
}; rational rsign() const { return sign() ? rational::minus_one() : rational::one(); }
};
class eq_justification {
class eq_justification { lpci m_cs[4];
svector<lpcindex> m_cs; public:
public: eq_justification(std::initializer_list<lpci> cs) {
eq_justification(std::initializer_list<lpcindex> cs) { int i = 0;
for (lpcindex c: cs) for (lpci c: cs) {
m_cs.push_back(c); m_cs[i++] = c;
} }
void explain(lp::explanation& e) const { for (; i < 4; i++) {
for (lpcindex c : m_cs) m_cs[i] = -1;
}
}
void explain(lp::explanation& e) const {
for (lpci c : m_cs)
if (c + 1 != 0) // c != -1
e.add(c); e.add(c);
} }
};
class var_eqs {
struct justified_var {
signed_var m_var;
eq_justification m_j;
justified_var(signed_var v, eq_justification const& j): m_var(v), m_j(j) {}
}; };
typedef svector<justified_var> justified_vars;
class var_eqs { struct dfs_frame {
struct justified_var { signed_var m_var;
signed_var m_var; unsigned m_index;
eq_justification m_j; dfs_frame(signed_var v, unsigned i): m_var(v), m_index(i) {}
justified_var(signed_var v, eq_justification const& j): m_var(v), m_j(j) {} };
}; typedef std::pair<signed_var, signed_var> signed_var_pair;
typedef svector<justified_var> justified_vars;
struct dfs_frame { union_find_default_ctx m_ufctx;
signed_var m_var; union_find<> m_uf;
unsigned m_index; svector<signed_var_pair> m_trail;
dfs_frame(signed_var v, unsigned i): m_var(v), m_index(i) {} unsigned_vector m_trail_lim;
}; vector<justified_vars> m_eqs; // signed_var-index -> justified_var corresponding to edges in a graph used to extract justifications.
typedef std::pair<signed_var, signed_var> signed_var_pair;
union_find_default_ctx m_ufctx; mutable svector<dfs_frame> m_todo;
union_find<> m_uf; mutable svector<bool> m_marked;
svector<signed_var_pair> m_trail; mutable unsigned_vector m_marked_trail;
unsigned_vector m_trail_lim; mutable svector<eq_justification> m_dfs_trail;
vector<justified_vars> m_eqs; // signed_var-index -> justified_var corresponding to edges in a graph used to extract justifications.
mutable svector<dfs_frame> m_todo; public:
mutable svector<bool> m_marked; var_eqs();
mutable unsigned_vector m_marked_trail;
mutable svector<eq_justification> m_dfs_trail;
/**
\brief push a scope
*/
void push();
/**
\brief pop n scopes
*/
void pop(unsigned n);
/**
\brief merge equivalence classes for v1, v2 with justification j
*/
void merge(signed_var v1, signed_var v2, eq_justification const& j);
void merge_plus(lpvar v1, lpvar v2, eq_justification const& j) { merge(signed_var(v1, false), signed_var(v2, false), j); }
void merge_minus(lpvar v1, lpvar v2, eq_justification const& j) { merge(signed_var(v1, false), signed_var(v2, true), j); }
/**
\brief find equivalence class representative for v
*/
signed_var find(signed_var v) const;
inline signed_var find(lpvar j) const {
return find(signed_var(j, false));
}
inline bool is_root(lpvar j) const {
signed_var sv = find(signed_var(j, false));
return sv.var() == j;
}
bool vars_are_equiv(lpvar j, lpvar k) const {
signed_var sj = find(signed_var(j, false));
signed_var sk = find(signed_var(k, false));
return sj.var() == sk.var();
}
/**
\brief Returns eq_justifications for
\pre find(v1) == find(v2)
*/
void explain(signed_var v1, signed_var v2, lp::explanation& e) const;
inline
void explain(lpvar v1, lpvar v2, lp::explanation & e) const {
return explain(signed_var(v1, false), signed_var(v2, false), e);
}
inline void explain(lpvar j, lp::explanation& e) const {
signed_var s(j, false);
return explain(find(s), s, e);
}
class iterator {
var_eqs& m_ve; // context.
unsigned m_idx; // index into a signed variable, same as union-find index
bool m_touched; // toggle between initial and final state
public: public:
var_eqs(); iterator(var_eqs& ve, unsigned idx, bool t) : m_ve(ve), m_idx(idx), m_touched(t) {}
signed_var operator*() const {
/** return signed_var(m_idx, from_index()); // 0 is needed to call the right constructor
\brief push a scope
*/
void push();
/**
\brief pop n scopes
*/
void pop(unsigned n);
/**
\brief merge equivalence classes for v1, v2 with justification j
*/
void merge(signed_var v1, signed_var v2, eq_justification const& j);
void merge_plus(lpvar v1, lpvar v2, eq_justification const& j) { merge(signed_var(v1, false), signed_var(v2, false), j); }
void merge_minus(lpvar v1, lpvar v2, eq_justification const& j) { merge(signed_var(v1, false), signed_var(v2, true), j); }
/**
\brief find equivalence class representative for v
*/
signed_var find(signed_var v) const;
inline lpvar find(lpvar j, rational& sign) const {
signed_var sv = find(signed_var(j, false));
sign = sv.sign()? rational(-1) : rational(1);
return sv.var();
} }
iterator& operator++() { m_idx = m_ve.m_uf.next(m_idx); m_touched = true; return *this; }
inline rational find_sign(lpvar j) const { bool operator==(iterator const& other) const { return m_idx == other.m_idx && m_touched == other.m_touched; }
signed_var sv = find(signed_var(j, false)); bool operator!=(iterator const& other) const { return m_idx != other.m_idx || m_touched != other.m_touched; }
return sv.sign()? rational(-1) : rational(1);
}
inline lpvar find(lpvar j) const {
signed_var sv = find(signed_var(j, false));
return sv.var();
}
inline bool is_root(lpvar j) const {
signed_var sv = find(signed_var(j, false));
return sv.var() == j;
}
bool vars_are_equiv(lpvar j, lpvar k) const {
signed_var sj = find(signed_var(j, false));
signed_var sk = find(signed_var(k, false));
return sj.var() == sk.var();
}
/**
\brief Returns eq_justifications for
\pre find(v1) == find(v2)
*/
void explain(signed_var v1, signed_var v2, lp::explanation& e) const;
inline
void explain(lpvar v1, lpvar v2, lp::explanation & e) const {
return explain(signed_var(v1), signed_var(v2), e);
}
inline void explain(lpvar j, lp::explanation& e) const {
signed_var s(j, false);
return explain(find(s), s, e);
}
class iterator {
var_eqs& m_ve; // context.
unsigned m_idx; // index into a signed variable, same as union-find index
bool m_touched; // toggle between initial and final state
public:
iterator(var_eqs& ve, unsigned idx, bool t) : m_ve(ve), m_idx(idx), m_touched(t) {}
signed_var operator*() const { return signed_var(m_idx); }
iterator& operator++() { m_idx = m_ve.m_uf.next(m_idx); m_touched = true; return *this; }
bool operator==(iterator const& other) const { return m_idx == other.m_idx && m_touched == other.m_touched; }
bool operator!=(iterator const& other) const { return m_idx != other.m_idx || m_touched != other.m_touched; }
};
class eq_class {
var_eqs& m_ve;
signed_var m_v;
public:
eq_class(var_eqs& ve, signed_var v) : m_ve(ve), m_v(v) {}
iterator begin() { return iterator(m_ve, m_v.index(), false); }
iterator end() { return iterator(m_ve, m_v.index(), true); }
};
eq_class equiv_class(signed_var v) { return eq_class(*this, v); }
eq_class equiv_class(lpvar v) { return equiv_class(signed_var(v, false)); }
}; };
class eq_class {
var_eqs& m_ve;
signed_var m_v;
public:
eq_class(var_eqs& ve, signed_var v) : m_ve(ve), m_v(v) {}
iterator begin() { return iterator(m_ve, m_v.index(), false); }
iterator end() { return iterator(m_ve, m_v.index(), true); }
};
eq_class equiv_class(signed_var v) { return eq_class(*this, v); }
eq_class equiv_class(lpvar v) { return equiv_class(signed_var(v, false)); }
};
} }