mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 19:53:34 +00:00
Code Activity

fix #3235 - return early during lookaehad, avoid checking invariant when context is inconsistent

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-11 10:55:56 -07:00
parent 59acd1093d
commit 36cddd0c46
3 changed files with 24 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/smt/smt_context.cpp
View file

@ -311,9 +311,6 @@ namespace smt {
}
void context::assign_core(literal l, b_justification j, bool decision) {
CTRACE("assign_core", l.var() == 13, tout << (decision?"decision: ":"propagating: ") << l << " ";
display_literal_smt2(tout, l) << " level: " << m_scope_lvl << "\n";
display(tout << "relevant: " << is_relevant_core(l) << "\n", j););
m_assigned_literals.push_back(l);
m_assignment[l.index()] = l_true;
m_assignment[(~l).index()] = l_false;
@ -327,26 +324,25 @@ namespace smt {
}
d.m_phase_available = true;
d.m_phase = !l.sign();
CTRACE("assign_core", l.var() == 13, tout << (decision?"decision: ":"propagating: ") << l << " ";
/*display_literal(tout, l);*/
tout << "relevant: " << is_relevant_core(l) << " level: " << m_scope_lvl << " is atom " << d.is_atom() << "\n";
/*display(tout, j);*/
);
TRACE("phase_selection", tout << "saving phase, is_pos: " << d.m_phase << " l: " << l << "\n";);
TRACE("relevancy",
CTRACE("relevancy", l.var() == 13,
tout << "is_atom: " << d.is_atom() << " is relevant: "
<< is_relevant_core(l) << " relevancy-lvl: " << relevancy_lvl() << "\n";);
if (d.is_atom() && (relevancy_lvl() == 0 || (relevancy_lvl() == 1 && !d.is_quantifier()) || is_relevant_core(l)))
if (d.is_atom() && (relevancy_lvl() == 0 || (relevancy_lvl() == 1 && !d.is_quantifier()) || is_relevant_core(l))) {
CTRACE("assign_core", l.var() == 13, tout << "propagation queue\n";);
m_atom_propagation_queue.push_back(l);
}
if (m.has_trace_stream())
trace_assign(l, j, decision);
m_case_split_queue->assign_lit_eh(l);
// a unit is asserted at search level. Mark it as relevant.
// this addresses bug... where a literal becomes fixed to true (false)
// as a conflict gets assigned misses relevancy (and quantifier instantiation).
//
if (false && !decision && relevancy() && at_search_level() && !is_relevant_core(l)) {
mark_as_relevant(l);
}
}
bool context::bcp() {
@ -1356,13 +1352,14 @@ namespace smt {
*/
bool context::propagate_atoms() {
SASSERT(!inconsistent());
CTRACE("propagate_atoms", !m_atom_propagation_queue.empty(), tout << m_atom_propagation_queue << "\n";);
for (unsigned i = 0; i < m_atom_propagation_queue.size() && !get_cancel_flag(); i++) {
SASSERT(!inconsistent());
literal l = m_atom_propagation_queue[i];
bool_var v = l.var();
bool_var_data & d = get_bdata(v);
lbool val = get_assignment(v);
TRACE("propagate_atoms", tout << "propagating atom, #" << bool_var2expr(v)->get_id() << ", is_enode(): " << d.is_enode()
CTRACE("propagate_atoms", v == 13, tout << "propagating atom, #" << bool_var2expr(v)->get_id() << ", is_enode(): " << d.is_enode()
<< " tag: " << (d.is_eq()?"eq":"") << (d.is_theory_atom()?"th":"") << (d.is_quantifier()?"q":"") << " " << l << "\n";);
SASSERT(val != l_undef);
if (d.is_enode())
@ -2070,7 +2067,7 @@ namespace smt {
while (i != old_lim) {
--i;
literal l = m_assigned_literals[i];
CTRACE("assign_core", l.var() == 1573 || l.var() == 1253, tout << "unassign " << l << "\n";);
CTRACE("assign_core", l.var() == 13, tout << "unassign " << l << "\n";);
m_assignment[l.index()] = l_undef;
m_assignment[(~l).index()] = l_undef;
bool_var v = l.var();
@ -2443,6 +2440,8 @@ namespace smt {
m_asserted_formulas.pop_scope(num_scopes);
CTRACE("propagate_atoms", !m_atom_propagation_queue.empty(), tout << m_atom_propagation_queue << "\n";);
m_eq_propagation_queue.reset();
m_th_eq_propagation_queue.reset();
m_th_diseq_propagation_queue.reset();

8
src/smt/smt_lookahead.cpp
View file

@ -82,7 +82,10 @@ namespace smt {
unsigned nf = 0, nc = 0, ns = 0, bound = 2000, n = 0;
for (bool_var v : vars) {
if (!ctx.bool_var2expr(v)) continue;
literal lit(v, false);
literal lit(v, false);
ctx.propagate();
if (ctx.inconsistent())
return expr_ref(m.mk_false(), m);
ctx.push_scope();
ctx.assign(lit, b_justification::mk_axiom(), true);
ctx.propagate();
@ -96,6 +99,9 @@ namespace smt {
continue;
}
ctx.propagate();
if (ctx.inconsistent())
return expr_ref(m.mk_false(), m);
ctx.push_scope();
ctx.assign(~lit, b_justification::mk_axiom(), true);
ctx.propagate();

4
src/smt/theory_bv.cpp
View file

@ -1457,7 +1457,7 @@ namespace smt {
m_diseq_watch_lim.shrink(m_diseq_watch_lim.size()-num_scopes);
#endif
theory::pop_scope_eh(num_scopes);
TRACE("bv", m_find.display(tout << get_context().get_scope_level() << " - "
TRACE("bv_verbose", m_find.display(tout << get_context().get_scope_level() << " - "
<< num_scopes << " = " << (get_context().get_scope_level() - num_scopes) << "\n"););
}
@ -1888,6 +1888,8 @@ namespace smt {
}
bool theory_bv::check_invariant() {
if (get_context().inconsistent())
return true;
unsigned num = get_num_vars();
for (unsigned v = 0; v < num; v++) {
check_assignment(v);