mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

fill columns to fill in random update as in theory_arith_aux.h

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-04-07 15:21:32 -07:00
parent 0e78f092b5
commit ae8c6acc1a
2 changed files with 45 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/lp/random_updater_def.h
View file

@ -38,6 +38,7 @@ random_updater::random_updater(
bool random_updater::shift_var(unsigned v) {
SASSERT(!m_lar_solver.column_is_fixed(v));
return m_lar_solver.get_int_solver()->shift_var(v, m_range);
}
@ -81,7 +82,7 @@ void random_updater::add_column_to_sets(unsigned j) {
unsigned row = m_lar_solver.get_core_solver().m_r_heading[j];
for (auto & row_c : m_lar_solver.get_core_solver().m_r_A.m_rows[row]) {
unsigned cj = row_c.var();
if (m_lar_solver.get_core_solver().m_r_heading[cj] < 0) {
if (m_lar_solver.get_core_solver().m_r_heading[cj] < 0 && !m_lar_solver.column_is_fixed(cj)) {
m_var_set.insert(cj);
add_value(m_lar_solver.get_core_solver().m_r_x[cj]);
}

47
src/smt/theory_lra.cpp
View file

@ -265,8 +265,10 @@ class theory_lra::imp {
svector<std::pair<theory_var, theory_var> > m_assume_eq_candidates;
unsigned m_assume_eq_head;
unsigned m_num_conflicts;
std::unordered_map<lp::impq, theory_var> m_var_value_table;
lp::u_set m_tmp_var_set;
unsigned m_num_conflicts;
// non-linear arithmetic
scoped_ptr<nra::solver> m_nra;
@ -1586,12 +1588,49 @@ public:
bool assume_eqs() {
svector<lpvar> vars;
m_var_value_table.clear();
m_tmp_var_set.clear();
m_tmp_var_set.resize(th.get_num_vars());
theory_var sz = static_cast<theory_var>(th.get_num_vars());
for (theory_var v = 0; v < sz; ++v) {
if (th.is_relevant_and_shared(get_enode(v))) {
auto vi = register_theory_var_in_lar_solver(v);
if (!can_get_ivalue(v)) {
continue;
}
enode * n1 = get_enode(v);
if (!th.is_relevant_and_shared(n1)) {
continue;
}
lpvar vi = lp().external_to_local(v);
if (vi == lp::null_lpvar)
continue;
if (lp::tv::is_term(vi)) {
vi = lp().map_term_index_to_column_index(vi);
}
const auto& vi_val = lp().get_column_value(vi);
auto it = m_var_value_table.find(vi_val);
if (it == m_var_value_table.end()) {
m_var_value_table[vi_val] = v;
continue;
}
theory_var other = it->second;
SASSERT(other != v);
enode * n2 = get_enode(other);
if (n1->get_root() == n2->get_root())
continue;
if (!lp().column_is_fixed(vi)) {
vars.push_back(vi);
}
else if (!m_tmp_var_set.contains(other)) {
m_tmp_var_set.insert(other);
lpvar other_j = lp().external_to_local(other);
if (lp::tv::is_term(other_j)) {
other_j = lp().map_term_index_to_column_index(other_j);
}
if (!lp().column_is_fixed(other_j)) {
vars.push_back(other_j);
}
}
}
if (vars.empty()) {
return false;