diff --git a/src/smt/smt_b_justification.h b/src/smt/smt_b_justification.h index 700c41807..55669a7ef 100644 --- a/src/smt/smt_b_justification.h +++ b/src/smt/smt_b_justification.h @@ -93,6 +93,16 @@ namespace smt { const b_justification null_b_justification(static_cast(0)); + inline std::ostream& operator<<(std::ostream& out, b_justification::kind k) { + switch (k) { + case b_justification::CLAUSE: return out << "clause"; + case b_justification::BIN_CLAUSE: return out << "bin_clause"; + case b_justification::AXIOM: return out << "axiom"; + case b_justification::JUSTIFICATION: return out << "theory"; + } + return out; + } + typedef std::pair justified_literal; }; diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 02c38a2bd..a6432c960 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -468,20 +468,6 @@ namespace smt { } bool conflict_resolution::resolve(b_justification conflict, literal not_l) { - -#if 0 - // for debugging #1233 - if (not_l == to_literal(22267)) { - std::cout << not_l << "\n"; - enable_trace("conflict"); - enable_trace("conflict_verbose"); - TRACE("conflict", - unsigned idx = 0; - for (literal lit : m_assigned_literals) { - m_ctx.display_literal(tout << (idx++) << ":", lit); tout << "\n"; - }); - } -#endif b_justification js; literal consequent; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 8819e37b6..62a569e2b 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -285,15 +285,7 @@ namespace smt { d.set_justification(j); } - 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);); diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index f2fb1084b..f5ba52128 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -601,7 +601,7 @@ namespace smt { out << "justification " << j.get_justification()->get_from_theory() << ": "; literal_vector lits; const_cast(*m_conflict_resolution).justification2literals(j.get_justification(), lits); - display_literals(out, lits.size(), lits.c_ptr()); + display_literals(out, lits); break; } default: diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index caba4e92e..6f7cf1b5e 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1228,18 +1228,25 @@ bool theory_seq::is_solved() { return true; } -void theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const { +/** + \brief while extracting dependency literals ensure that they have all been asserted on the context. +*/ +bool theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const { + context & ctx = get_context(); + DEBUG_CODE(for (literal lit : lits) SASSERT(ctx.get_assignment(lit) == l_true); ); + bool asserted = true; svector assumptions; const_cast(m_dm).linearize(dep, assumptions); - for (unsigned i = 0; i < assumptions.size(); ++i) { - assumption const& a = assumptions[i]; + for (assumption const& a : assumptions) { if (a.lit != null_literal) { lits.push_back(a.lit); + asserted &= ctx.get_assignment(a.lit) == l_true; } if (a.n1 != 0) { eqs.push_back(enode_pair(a.n1, a.n2)); } } + return asserted; } @@ -1257,7 +1264,8 @@ void theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits ctx.mark_as_relevant(lit); enode_pair_vector eqs; - linearize(dep, eqs, lits); + if (!linearize(dep, eqs, lits)) + return; TRACE("seq", tout << "assert:"; ctx.display_detailed_literal(tout, lit); @@ -1276,7 +1284,8 @@ void theory_seq::set_conflict(dependency* dep, literal_vector const& _lits) { context& ctx = get_context(); enode_pair_vector eqs; literal_vector lits(_lits); - linearize(dep, eqs, lits); + if (!linearize(dep, eqs, lits)) + return; TRACE("seq", display_deps(tout << "assert conflict:", lits, eqs);); m_new_propagation = true; ctx.set_conflict( @@ -1292,27 +1301,13 @@ void theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) { context& ctx = get_context(); literal_vector lits; enode_pair_vector eqs; - linearize(dep, eqs, lits); + if (!linearize(dep, eqs, lits)) + return; TRACE("seq", tout << "assert: " << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << " <-\n"; 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)); @@ -1858,12 +1853,12 @@ bool theory_seq::solve_ne(unsigned idx) { ne const& n = m_nqs[idx]; unsigned num_undef_lits = 0; - for (unsigned i = 0; i < n.lits().size(); ++i) { - switch (ctx.get_assignment(n.lits(i))) { + for (literal lit : n.lits()) { + switch (ctx.get_assignment(lit)) { case l_false: TRACE("seq", display_disequation(tout << "has false literal\n", n); - ctx.display_literal_verbose(tout, n.lits(i)); - tout << "\n" << n.lits(i) << " " << ctx.is_relevant(n.lits(i)) << "\n"; + ctx.display_literal_verbose(tout, lit); + tout << "\n" << lit << " " << ctx.is_relevant(lit) << "\n"; ); return true; case l_true: @@ -1967,8 +1962,7 @@ bool theory_seq::solve_ne(unsigned idx) { if (num_undef_lits == 1 && new_ls.empty()) { literal_vector lits; literal undef_lit = null_literal; - for (unsigned i = 0; i < new_lits.size(); ++i) { - literal lit = new_lits[i]; + for (literal lit : new_lits) { switch (ctx.get_assignment(lit)) { case l_true: lits.push_back(lit); @@ -2574,8 +2568,8 @@ void theory_seq::display_disequations(std::ostream& out) const { } void theory_seq::display_disequation(std::ostream& out, ne const& e) const { - for (unsigned j = 0; j < e.lits().size(); ++j) { - out << e.lits(j) << " "; + for (literal lit : e.lits()) { + out << lit << " "; } if (e.lits().size() > 0) { out << "\n"; @@ -3820,11 +3814,11 @@ literal theory_seq::mk_eq_empty(expr* _e, bool phase) { } expr_ref_vector concats(m); m_util.str.get_concat(e, concats); - for (unsigned i = 0; i < concats.size(); ++i) { - if (m_util.str.is_unit(concats[i].get())) { + for (expr* c : concats) { + if (m_util.str.is_unit(c)) { return false_literal; } - if (m_util.str.is_string(concats[i].get(), s) && s.length() > 0) { + if (m_util.str.is_string(c, s) && s.length() > 0) { return false_literal; } } @@ -3895,8 +3889,9 @@ void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp literal_vector lits(_lits); enode_pair_vector eqs; - linearize(deps, eqs, lits); - + if (!linearize(deps, eqs, lits)) + return; + if (add_to_eqs) { deps = mk_join(deps, _lits); new_eq_eh(deps, n1, n2); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 2ad257fd7..e08c0588e 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -431,7 +431,7 @@ namespace smt { bool explain_empty(expr_ref_vector& es, dependency*& dep); // asserting consequences - void linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const; + bool linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const; void propagate_lit(dependency* dep, literal lit) { propagate_lit(dep, 0, 0, lit); } void propagate_lit(dependency* dep, unsigned n, literal const* lits, literal lit); void propagate_eq(dependency* dep, enode* n1, enode* n2);