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

minor refactor

Browse source
This commit is contained in:
Jakob Rath 2023-08-01 16:08:42 +02:00
parent 417dbf3354
commit f6fb9bf316
2 changed files with 16 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/math/polysat/slicing.cpp
View file

@ -171,7 +171,7 @@ namespace polysat {
m_scopes.push_back(m_trail.size());
m_egraph.push();
m_dep_size_trail.push_back(m_dep_var.size());
SASSERT(!m_solver.config().m_slicing_congruence || m_needs_congruence.empty());
SASSERT(!use_var_congruences() || m_needs_congruence.empty());
}
void slicing::pop_scope(unsigned num_scopes) {
@ -313,7 +313,7 @@ namespace polysat {
m_egraph.merge(s, concat, dep_t().encode());
}
void slicing::add_congruence(pvar v) {
void slicing::add_var_congruence(pvar v) {
enode_vector& base = m_tmp2;
SASSERT(base.empty());
enode* sv = var2slice(v);
@ -323,21 +323,25 @@ namespace polysat {
base.clear();
}
void slicing::add_congruence_if_needed(pvar v) {
void slicing::add_var_congruence_if_needed(pvar v) {
if (!m_needs_congruence.contains(v))
return;
m_needs_congruence.remove(v);
add_congruence(v);
add_var_congruence(v);
}
void slicing::update_var_congruences() {
if (!m_solver.config().m_slicing_congruence)
if (!use_var_congruences())
return;
for (pvar v : m_needs_congruence)
add_congruence(v);
add_var_congruence(v);
m_needs_congruence.reset();
}
bool slicing::use_var_congruences() const {
return m_solver.config().m_slicing_congruence;
}
// split a single slice without updating any equivalences
void slicing::split_core(enode* s, unsigned cut) {
SASSERT(is_slice(s)); // this action only makes sense for slices
@ -732,7 +736,7 @@ namespace polysat {
}
bool slicing::can_propagate() const {
if (m_solver.config().m_slicing_congruence && !m_needs_congruence.empty())
if (use_var_congruences() && !m_needs_congruence.empty())
return true;
return m_egraph.can_propagate();
}
@ -1052,8 +1056,8 @@ namespace polysat {
else {
enode* n = find_or_alloc_disequality(sy, sx, lit);
if (!m_disequality_conflict && is_equal(sx, sy)) {
add_congruence_if_needed(x);
add_congruence_if_needed(y);
add_var_congruence_if_needed(x);
add_var_congruence_if_needed(y);
m_disequality_conflict = n;
return false;
}

5
src/math/polysat/slicing.h
View file

@ -116,8 +116,9 @@ namespace polysat {
// Add an equation v = concat(s1, ..., sn)
// for each variable v with base slices s1, ..., sn
void update_var_congruences();
void add_congruence(pvar v);
void add_congruence_if_needed(pvar v);
void add_var_congruence(pvar v);
void add_var_congruence_if_needed(pvar v);
bool use_var_congruences() const;
func_decl* mk_concat_decl(ptr_vector<expr> const& args);
enode* mk_concat_node(enode_vector const& slices);