mirror of
https://github.com/Z3Prover/z3
synced 2025-07-17 09:56:39 +00:00
some renaming in var_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
821886b94b
commit
0c214ec465
2 changed files with 23 additions and 23 deletions
|
@ -51,10 +51,10 @@ void var_eqs::merge(signed_var v1, signed_var v2, eq_justification const& j) {
|
||||||
m_trail.push_back(std::make_pair(v1, v2));
|
m_trail.push_back(std::make_pair(v1, v2));
|
||||||
m_uf.merge(v1.index(), v2.index());
|
m_uf.merge(v1.index(), v2.index());
|
||||||
m_uf.merge((~v1).index(), (~v2).index());
|
m_uf.merge((~v1).index(), (~v2).index());
|
||||||
m_eqs[v1.index()].push_back(justified_var(v2, j));
|
m_eqs[v1.index()].push_back(eq_edge(v2, j));
|
||||||
m_eqs[v2.index()].push_back(justified_var(v1, j));
|
m_eqs[v2.index()].push_back(eq_edge(v1, j));
|
||||||
m_eqs[(~v1).index()].push_back(justified_var(~v2, j));
|
m_eqs[(~v1).index()].push_back(eq_edge(~v2, j));
|
||||||
m_eqs[(~v2).index()].push_back(justified_var(~v1, j));
|
m_eqs[(~v2).index()].push_back(eq_edge(~v1, j));
|
||||||
}
|
}
|
||||||
|
|
||||||
signed_var var_eqs::find(signed_var v) const {
|
signed_var var_eqs::find(signed_var v) const {
|
||||||
|
@ -71,7 +71,7 @@ void var_eqs::explain_dfs(signed_var v1, signed_var v2, lp::explanation& e) cons
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
m_todo.push_back(var_frame(v1, 0));
|
m_todo.push_back(var_frame(v1, 0));
|
||||||
m_jtrail.reset();
|
m_justtrail.reset();
|
||||||
m_marked.reserve(m_eqs.size(), false);
|
m_marked.reserve(m_eqs.size(), false);
|
||||||
SASSERT(m_marked_trail.empty());
|
SASSERT(m_marked_trail.empty());
|
||||||
m_marked[v1.index()] = true;
|
m_marked[v1.index()] = true;
|
||||||
|
@ -87,30 +87,30 @@ void var_eqs::explain_dfs(signed_var v1, signed_var v2, lp::explanation& e) cons
|
||||||
bool seen_all = true;
|
bool seen_all = true;
|
||||||
unsigned sz = next.size();
|
unsigned sz = next.size();
|
||||||
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];
|
eq_edge const& jv = next[i];
|
||||||
signed_var v3 = jv.m_var;
|
signed_var v3 = jv.m_var;
|
||||||
if (!m_marked[v3.index()]) {
|
if (!m_marked[v3.index()]) {
|
||||||
seen_all = false;
|
seen_all = false;
|
||||||
f.m_index = i + 1;
|
f.m_index = i + 1;
|
||||||
m_todo.push_back(var_frame(v3, 0));
|
m_todo.push_back(var_frame(v3, 0));
|
||||||
m_jtrail.push_back(jv.m_j);
|
m_justtrail.push_back(jv.m_just);
|
||||||
m_marked_trail.push_back(v3.index());
|
m_marked_trail.push_back(v3.index());
|
||||||
m_marked[v3.index()] = true;
|
m_marked[v3.index()] = true;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
if (seen_all) {
|
if (seen_all) {
|
||||||
m_todo.pop_back();
|
m_todo.pop_back();
|
||||||
m_jtrail.pop_back();
|
m_justtrail.pop_back();
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
for (eq_justification const& j : m_jtrail) {
|
for (eq_justification const& j : m_justtrail) {
|
||||||
j.explain(e);
|
j.explain(e);
|
||||||
}
|
}
|
||||||
m_stats.m_num_explains += m_jtrail.size();
|
m_stats.m_num_explains += m_justtrail.size();
|
||||||
m_stats.m_num_explain_calls++;
|
m_stats.m_num_explain_calls++;
|
||||||
m_todo.reset();
|
m_todo.reset();
|
||||||
m_jtrail.reset();
|
m_justtrail.reset();
|
||||||
for (unsigned idx : m_marked_trail) {
|
for (unsigned idx : m_marked_trail) {
|
||||||
m_marked[idx] = false;
|
m_marked[idx] = false;
|
||||||
}
|
}
|
||||||
|
@ -125,7 +125,7 @@ void var_eqs::explain_bfs(signed_var v1, signed_var v2, lp::explanation& e) cons
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
m_todo.push_back(var_frame(v1, 0));
|
m_todo.push_back(var_frame(v1, 0));
|
||||||
m_jtrail.push_back(eq_justification({}));
|
m_justtrail.push_back(eq_justification({}));
|
||||||
m_marked.reserve(m_eqs.size(), false);
|
m_marked.reserve(m_eqs.size(), false);
|
||||||
SASSERT(m_marked_trail.empty());
|
SASSERT(m_marked_trail.empty());
|
||||||
m_marked[v1.index()] = true;
|
m_marked[v1.index()] = true;
|
||||||
|
@ -140,11 +140,11 @@ void var_eqs::explain_bfs(signed_var v1, signed_var v2, lp::explanation& e) cons
|
||||||
auto const& next = m_eqs[v.index()];
|
auto const& next = m_eqs[v.index()];
|
||||||
unsigned sz = next.size();
|
unsigned sz = next.size();
|
||||||
for (unsigned i = sz; i-- > 0; ) {
|
for (unsigned i = sz; i-- > 0; ) {
|
||||||
justified_var const& jv = next[i];
|
eq_edge const& jv = next[i];
|
||||||
signed_var v3 = jv.m_var;
|
signed_var v3 = jv.m_var;
|
||||||
if (!m_marked[v3.index()]) {
|
if (!m_marked[v3.index()]) {
|
||||||
m_todo.push_back(var_frame(v3, head));
|
m_todo.push_back(var_frame(v3, head));
|
||||||
m_jtrail.push_back(jv.m_j);
|
m_justtrail.push_back(jv.m_just);
|
||||||
m_marked_trail.push_back(v3.index());
|
m_marked_trail.push_back(v3.index());
|
||||||
m_marked[v3.index()] = true;
|
m_marked[v3.index()] = true;
|
||||||
}
|
}
|
||||||
|
@ -152,14 +152,14 @@ void var_eqs::explain_bfs(signed_var v1, signed_var v2, lp::explanation& e) cons
|
||||||
}
|
}
|
||||||
|
|
||||||
while (head != 0) {
|
while (head != 0) {
|
||||||
m_jtrail[head].explain(e);
|
m_justtrail[head].explain(e);
|
||||||
head = m_todo[head].m_index;
|
head = m_todo[head].m_index;
|
||||||
++m_stats.m_num_explains;
|
++m_stats.m_num_explains;
|
||||||
}
|
}
|
||||||
++m_stats.m_num_explain_calls;
|
++m_stats.m_num_explain_calls;
|
||||||
|
|
||||||
m_todo.reset();
|
m_todo.reset();
|
||||||
m_jtrail.reset();
|
m_justtrail.reset();
|
||||||
for (unsigned idx : m_marked_trail) {
|
for (unsigned idx : m_marked_trail) {
|
||||||
m_marked[idx] = false;
|
m_marked[idx] = false;
|
||||||
}
|
}
|
||||||
|
|
|
@ -56,12 +56,12 @@ public:
|
||||||
};
|
};
|
||||||
|
|
||||||
class var_eqs {
|
class var_eqs {
|
||||||
struct justified_var {
|
struct eq_edge {
|
||||||
signed_var m_var;
|
signed_var m_var;
|
||||||
eq_justification m_j;
|
eq_justification m_just;
|
||||||
justified_var(signed_var v, eq_justification const& j): m_var(v), m_j(j) {}
|
eq_edge(signed_var v, eq_justification const& j): m_var(v), m_just(j) {}
|
||||||
};
|
};
|
||||||
typedef svector<justified_var> justified_vars;
|
typedef svector<eq_edge> eq_edges;
|
||||||
|
|
||||||
struct var_frame {
|
struct var_frame {
|
||||||
signed_var m_var;
|
signed_var m_var;
|
||||||
|
@ -80,14 +80,14 @@ class var_eqs {
|
||||||
union_find<var_eqs> m_uf;
|
union_find<var_eqs> m_uf;
|
||||||
svector<signed_var_pair> m_trail;
|
svector<signed_var_pair> m_trail;
|
||||||
unsigned_vector m_trail_lim;
|
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.
|
vector<eq_edges> m_eqs; // signed_var-index -> eq_edges corresponding to edges in a graph used to extract justifications.
|
||||||
|
|
||||||
typedef trail_stack<var_eqs> trail_stack_t;
|
typedef trail_stack<var_eqs> trail_stack_t;
|
||||||
trail_stack_t m_stack;
|
trail_stack_t m_stack;
|
||||||
mutable svector<var_frame> m_todo;
|
mutable svector<var_frame> m_todo;
|
||||||
mutable svector<bool> m_marked;
|
mutable svector<bool> m_marked;
|
||||||
mutable unsigned_vector m_marked_trail;
|
mutable unsigned_vector m_marked_trail;
|
||||||
mutable svector<eq_justification> m_jtrail;
|
mutable svector<eq_justification> m_justtrail;
|
||||||
|
|
||||||
mutable stats m_stats;
|
mutable stats m_stats;
|
||||||
public:
|
public:
|
||||||
|
@ -154,7 +154,7 @@ public:
|
||||||
return explain(find(s), s, e);
|
return explain(find(s), s, e);
|
||||||
}
|
}
|
||||||
|
|
||||||
// iterates over the class of signed_var(m_idx)
|
// iterates over the class of lpvar(m_idx)
|
||||||
class iterator {
|
class iterator {
|
||||||
var_eqs& m_ve; // context.
|
var_eqs& m_ve; // context.
|
||||||
unsigned m_idx; // index into a signed variable, same as union-find index
|
unsigned m_idx; // index into a signed variable, same as union-find index
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue