mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

debugging #1233

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-21 08:16:41 -08:00
parent 33e8113c9e
commit c5f231acdf
4 changed files with 43 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
src/smt/smt_conflict_resolution.cpp
View file

@ -313,8 +313,8 @@ namespace smt {
SASSERT(var < static_cast<int>(m_ctx.get_num_bool_vars()));
TRACE("conflict", tout << "processing antecedent (level " << lvl << "):";
m_ctx.display_literal(tout, antecedent);
m_ctx.display_detailed_literal(tout << " ", antecedent); tout << "\n";);
m_ctx.display_detailed_literal(tout << " ", antecedent) << "\n";);
if (!m_ctx.is_marked(var) && lvl > m_ctx.get_base_level()) {
m_ctx.set_mark(var);
m_ctx.inc_bvar_activity(var);
@ -328,8 +328,7 @@ namespace smt {
if (get_manager().has_trace_stream()) {
get_manager().trace_stream() << "[resolve-lit] " << m_conflict_lvl - lvl << " ";
m_ctx.display_literal(get_manager().trace_stream(), ~antecedent);
get_manager().trace_stream() << "\n";
m_ctx.display_literal(get_manager().trace_stream(), ~antecedent) << "\n";
}
if (lvl == m_conflict_lvl) {
@ -391,7 +390,7 @@ namespace smt {
<< " search_lvl: " << m_ctx.get_search_level() << "\n";
tout << "js.kind: " << js.get_kind() << "\n";
tout << "consequent: " << consequent << ": ";
m_ctx.display_literal_verbose(tout, consequent); tout << "\n";
m_ctx.display_literal_verbose(tout, consequent) << "\n";
m_ctx.display(tout, js); tout << "\n";
);
@ -430,32 +429,16 @@ namespace smt {
void conflict_resolution::finalize_resolve(b_justification conflict, literal not_l) {
unmark_justifications(0);
TRACE("conflict",
tout << "before minimization:\n";
m_ctx.display_literals(tout, m_lemma);
tout << "\n";);
TRACE("conflict", m_ctx.display_literals(tout << "before minimization:\n", m_lemma) << "\n";);
TRACE("conflict_verbose",
tout << "before minimization:\n";
m_ctx.display_literals_verbose(tout, m_lemma);
tout << "\n";);
TRACE("conflict_verbose",m_ctx.display_literals_verbose(tout << "before minimization:\n", m_lemma) << "\n";);
if (m_params.m_minimize_lemmas)
minimize_lemma();
TRACE("conflict",
tout << "after minimization:\n";
m_ctx.display_literals(tout, m_lemma);
tout << "\n";);
TRACE("conflict_verbose",
tout << "after minimization:\n";
m_ctx.display_literals_verbose(tout, m_lemma);
tout << "\n";);
TRACE("conflict_bug",
m_ctx.display_literals_verbose(tout, m_lemma);
tout << "\n";);
TRACE("conflict", m_ctx.display_literals(tout << "after minimization:\n", m_lemma) << "\n";);
TRACE("conflict_verbose", m_ctx.display_literals_verbose(tout << "after minimization:\n", m_lemma) << "\n";);
TRACE("conflict_bug", m_ctx.display_literals_verbose(tout, m_lemma) << "\n";);
literal_vector::iterator it = m_lemma.begin();
literal_vector::iterator end = m_lemma.end();
@ -527,7 +510,8 @@ namespace smt {
get_manager().trace_stream() << "\n";
}
TRACE("conflict", tout << "processing consequent: " << idx << " "; m_ctx.display_literal_verbose(tout, consequent); tout << "\n";
TRACE("conflict", tout << "processing consequent id: " << idx << " lit: " << consequent << " "; m_ctx.display_literal(tout, consequent);
m_ctx.display_literal_verbose(tout, consequent) << "\n";
tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << " level: " << m_ctx.get_assign_level(consequent) << "\n";
);
SASSERT(js != null_b_justification);

9
src/smt/smt_context.cpp
View file

@ -287,6 +287,13 @@ namespace smt {
void context::assign_core(literal l, b_justification j, bool decision) {
#if 0
// for debugging #1233
if (l.var() == 11133 && l.sign()) {
std::cout << l << "\n";
UNREACHABLE();
}
#endif
TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " ";
display_literal_verbose(tout, l); tout << " level: " << m_scope_lvl << "\n";
display(tout, j););
@ -902,7 +909,7 @@ namespace smt {
}
/**
\brief Propabate the boolean assignment when two equivalence classes are merged.
\brief Propagate the boolean assignment when two equivalence classes are merged.
*/
void context::propagate_bool_enode_assignment(enode * r1, enode * r2, enode * n1, enode * n2) {
SASSERT(n1->is_bool());

2
src/smt/smt_context.h
View file

@ -1237,7 +1237,7 @@ namespace smt {
std::ostream& display_literal(std::ostream & out, literal l) const;
void display_detailed_literal(std::ostream & out, literal l) const { l.display(out, m_manager, m_bool_var2expr.c_ptr()); }
std::ostream& display_detailed_literal(std::ostream & out, literal l) const { l.display(out, m_manager, m_bool_var2expr.c_ptr()); return out; }
void display_literal_info(std::ostream & out, literal l) const;

23
src/smt/theory_seq.cpp
View file

@ -1298,6 +1298,21 @@ void theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) {
display_deps(tout, dep);
);
#if 0
//std::cout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n";
//display_deps(std::cout, dep);
for (literal lit : lits) {
SASSERT(ctx.get_assignment(lit) == l_true);
}
for (enode_pair p : eqs) {
if (p.first->get_root() != p.second->get_root()) {
std::cout << mk_pp(p.first->get_owner(), m) << " " << mk_pp(p.second->get_owner(), m) << "\n";
}
SASSERT(p.first->get_root() == p.second->get_root());
}
#endif
justification* js = ctx.mk_justification(
ext_theory_eq_propagation_justification(
get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2));
@ -3027,6 +3042,8 @@ expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) {
enode* n1 = ctx.get_enode(num);
enode* n2 = ctx.get_enode(e1);
res = m_util.str.mk_string(symbol(val.to_string().c_str()));
#if 1
// TBD remove this: using roots is unsound for propagation.
if (n1->get_root() == n2->get_root()) {
result = res;
deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(n1, n2)));
@ -3037,6 +3054,12 @@ expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) {
add_axiom(mk_eq(num, e1, false), ~mk_eq(e, res, false));
result = e;
}
#else
TRACE("seq", tout << "add axiom\n";);
add_axiom(~mk_eq(num, e1, false), mk_eq(e, res, false));
add_axiom(mk_eq(num, e1, false), ~mk_eq(e, res, false));
result = e;
#endif
}
else {
result = e;