mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

dbg

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-06 21:43:44 -08:00
parent 02b074e28b
commit b2c265496e
3 changed files with 13 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/lp/emonics.cpp
View file

@ -226,7 +226,6 @@ bool emonics::elists_are_consistent(std::unordered_map<unsigned_vector, std::uno
c.insert(e.var()); c.insert(e.var());
auto it = lists.find(m.rvars()); auto it = lists.find(m.rvars());
(void)it; (void)it;
CTRACE("nla_solver_mons", it->second != c, CTRACE("nla_solver_mons", it->second != c,
tout << "m = " << m << "\n"; tout << "m = " << m << "\n";
tout << "c = " ; print_vector(c, tout); tout << "\n"; tout << "c = " ; print_vector(c, tout); tout << "\n";

6
src/math/lp/int_solver.cpp
View file

@ -40,8 +40,9 @@ bool int_solver::has_inf_int() const {
int int_solver::find_inf_int_base_column() { int int_solver::find_inf_int_base_column() {
unsigned inf_int_count = 0; unsigned inf_int_count = 0;
int j = find_inf_int_boxed_base_column_with_smallest_range(inf_int_count); int j = find_inf_int_boxed_base_column_with_smallest_range(inf_int_count);
if (j != -1) if (j != -1) {
return j; return j;
}
if (inf_int_count == 0) if (inf_int_count == 0)
return -1; return -1;
unsigned k = random() % inf_int_count; unsigned k = random() % inf_int_count;
@ -58,8 +59,9 @@ int int_solver::get_kth_inf_int(unsigned k) const {
int int_solver::find_inf_int_nbasis_column() const { int int_solver::find_inf_int_nbasis_column() const {
for (unsigned j : m_lar_solver->r_nbasis()) for (unsigned j : m_lar_solver->r_nbasis())
if (!column_is_int_inf(j)) if (!column_is_int_inf(j)) {
return j; return j;
}
return -1; return -1;
} }

12
src/smt/theory_lra.cpp
View file

@ -1692,7 +1692,6 @@ public:
ctx().push_trail(value_trail<context, unsigned>(m_assume_eq_head)); ctx().push_trail(value_trail<context, unsigned>(m_assume_eq_head));
while (m_assume_eq_head < m_assume_eq_candidates.size()) { while (m_assume_eq_head < m_assume_eq_candidates.size()) {
++m_stats.m_assume_eqs;
std::pair<theory_var, theory_var> const & p = m_assume_eq_candidates[m_assume_eq_head]; std::pair<theory_var, theory_var> const & p = m_assume_eq_candidates[m_assume_eq_head];
theory_var v1 = p.first; theory_var v1 = p.first;
theory_var v2 = p.second; theory_var v2 = p.second;
@ -1703,6 +1702,7 @@ public:
is_eq(v1, v2) && n1->get_root() != n2->get_root(), is_eq(v1, v2) && n1->get_root() != n2->get_root(),
tout << "assuming eq: v" << v1 << " = v" << v2 << "\n";); tout << "assuming eq: v" << v1 << " = v" << v2 << "\n";);
if (is_eq(v1, v2) && n1->get_root() != n2->get_root() && th.assume_eq(n1, n2)) { if (is_eq(v1, v2) && n1->get_root() != n2->get_root() && th.assume_eq(n1, n2)) {
std::cout << v1 << " == " << v2 << "\n"; // mk_pp(n1->get_owner(), m) << " == " << mk_pp(n2->get_owner(), m) << "\n";
return true; return true;
} }
} }
@ -1736,6 +1736,12 @@ public:
case l_true: case l_true:
if (delayed_assume_eqs()) { if (delayed_assume_eqs()) {
++m_stats.m_assume_eqs;
return FC_CONTINUE;
}
if (assume_eqs()) {
++m_stats.m_assume_eqs;
return FC_CONTINUE; return FC_CONTINUE;
} }
@ -1761,14 +1767,10 @@ public:
st = FC_GIVEUP; st = FC_GIVEUP;
break; break;
} }
if (assume_eqs()) {
return FC_CONTINUE;
}
if (m_not_handled != nullptr) { if (m_not_handled != nullptr) {
TRACE("arith", tout << "unhandled operator " << mk_pp(m_not_handled, m) << "\n";); TRACE("arith", tout << "unhandled operator " << mk_pp(m_not_handled, m) << "\n";);
st = FC_GIVEUP; st = FC_GIVEUP;
} }
return st; return st;
case l_false: case l_false:
get_infeasibility_explanation_and_set_conflict(); get_infeasibility_explanation_and_set_conflict();