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

fix ordering of delayed assume eqs

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-26 16:22:24 -07:00
parent 499843ae7f
commit 7a04e52c41
4 changed files with 10 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_arith.h
View file

@ -46,6 +46,7 @@ namespace smt {
unsigned m_assert_lower, m_assert_upper, m_assert_diseq, m_core2th_eqs, m_core2th_diseqs;
unsigned m_th2core_eqs, m_th2core_diseqs, m_bound_props, m_offset_eqs, m_fixed_eqs, m_offline_eqs;
unsigned m_max_min;
unsigned m_assume_eqs;
unsigned m_gb_simplify, m_gb_superpose, m_gb_compute_basis, m_gb_num_processed;
unsigned m_nl_branching, m_nl_linear, m_nl_bounds, m_nl_cross_nested;
unsigned m_branch_infeasible_int, m_branch_infeasible_var;

2
src/smt/theory_arith_aux.h
View file

@ -2237,7 +2237,6 @@ namespace smt {
if (result)
get_context().push_trail(restore_size_trail<context, std::pair<theory_var, theory_var>, false>(m_assume_eq_candidates, old_sz));
return delayed_assume_eqs();
// return this->assume_eqs(m_var_value_table);
}
template<typename Ext>
@ -2258,6 +2257,7 @@ namespace smt {
if (get_value(v1) == get_value(v2) &&
get_enode(v1)->get_root() != get_enode(v2)->get_root() &&
assume_eq(get_enode(v1), get_enode(v2))) {
++m_stats.m_assume_eqs;
return true;
}
}

1
src/smt/theory_arith_pp.h
View file

@ -35,6 +35,7 @@ namespace smt {
st.update("arith assert diseq", m_stats.m_assert_diseq);
st.update("arith bound prop", m_stats.m_bound_props);
st.update("arith fixed eqs", m_stats.m_fixed_eqs);
st.update("arith assume eqs", m_stats.m_assume_eqs);
st.update("arith offset eqs", m_stats.m_offset_eqs);
st.update("arith gcd tests", m_stats.m_gcd_tests);
st.update("arith ineq splits", m_stats.m_branches);

15
src/smt/theory_lra.cpp
View file

@ -1583,13 +1583,13 @@ public:
}
tout << "\n"; );
if (!m_use_nra_model && !m_nla) {
lp().random_update(vars.size(), vars.c_ptr());
// lp().random_update(vars.size(), vars.c_ptr());
}
m_model_eqs.reset();
TRACE("arith", display(tout););
unsigned old_sz = m_assume_eq_candidates.size();
bool result = false;
unsigned num_candidates = 0;
int start = ctx().get_random_value();
for (theory_var i = 0; i < sz; ++i) {
theory_var v = (i + start) % sz;
@ -1611,11 +1611,10 @@ public:
tout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n";
tout << "v" << v << " = " << "v" << other << "\n";);
m_assume_eq_candidates.push_back(std::make_pair(v, other));
result = true;
}
}
if (result) {
if (num_candidates > 0) {
ctx().push_trail(restore_size_trail<context, std::pair<theory_var, theory_var>, false>(m_assume_eq_candidates, old_sz));
}
@ -1692,14 +1691,14 @@ public:
st = FC_GIVEUP;
break;
}
if (assume_eqs()) {
++m_stats.m_assume_eqs;
return FC_CONTINUE;
}
if (delayed_assume_eqs()) {
++m_stats.m_assume_eqs;
return FC_CONTINUE;
}
if (assume_eqs()) {
++m_stats.m_assume_eqs;
return FC_CONTINUE;
}
if (m_not_handled != nullptr) {
TRACE("arith", tout << "unhandled operator " << mk_pp(m_not_handled, m) << "\n";);
st = FC_GIVEUP;