mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

adding instrumentation to debug #1233

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-20 16:51:17 -08:00
parent 14714f2803
commit 33e8113c9e
6 changed files with 94 additions and 127 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/muz/pdr/pdr_context.cpp
View file

@ -149,30 +149,27 @@ namespace pdr {
}
datalog::rule const& pred_transformer::find_rule(model_core const& model) const {
obj_map<expr, datalog::rule const*>::iterator it = m_tag2rule.begin(), end = m_tag2rule.end();
TRACE("pdr_verbose",
datalog::rule_manager& rm = ctx.get_context().get_rule_manager();
for (; it != end; ++it) {
expr* pred = it->m_key;
for (auto const& kv : m_tag2rule) {
expr* pred = kv.m_key;
tout << mk_pp(pred, m) << ":\n";
if (it->m_value) rm.display_smt2(*it->m_value, tout) << "\n";
if (kv.m_value) rm.display_smt2(*kv.m_value, tout) << "\n";
}
);
it = m_tag2rule.begin();
if (m_tag2rule.size() == 1) {
return *it->m_value;
return *m_tag2rule.begin()->m_value;
}
expr_ref vl(m);
for (; it != end; ++it) {
expr* pred = it->m_key;
for (auto const& kv : m_tag2rule) {
expr* pred = kv.m_key;
if (model.eval(to_app(pred)->get_decl(), vl) && m.is_true(vl)) {
return *it->m_value;
return *kv.m_value;
}
}
UNREACHABLE();
return *((datalog::rule*)0);
throw default_exception("could not find rule");
}
void pred_transformer::find_predecessors(datalog::rule const& r, ptr_vector<func_decl>& preds) const {
@ -201,7 +198,7 @@ namespace pdr {
void pred_transformer::simplify_formulas(tactic& tac, expr_ref_vector& v) {
goal_ref g(alloc(goal, m, false, false, false));
for (unsigned j = 0; j < v.size(); ++j) g->assert_expr(v[j].get());
for (expr* e : v) g->assert_expr(e);
model_converter_ref mc;
proof_converter_ref pc;
expr_dependency_ref core(m);
@ -216,9 +213,8 @@ namespace pdr {
void pred_transformer::simplify_formulas() {
tactic_ref us = mk_unit_subsumption_tactic(m);
simplify_formulas(*us, m_invariants);
for (unsigned i = 0; i < m_levels.size(); ++i) {
simplify_formulas(*us, m_levels[i]);
}
for (auto & fmls : m_levels)
simplify_formulas(*us, fmls);
}
expr_ref pred_transformer::get_formulas(unsigned level, bool add_axioms) {

70
src/smt/smt_conflict_resolution.cpp
View file

@ -257,10 +257,8 @@ namespace smt {
literal_vector & antecedents = m_tmp_literal_vector;
antecedents.reset();
justification2literals(js, antecedents);
literal_vector::iterator it = antecedents.begin();
literal_vector::iterator end = antecedents.end();
for(; it != end; ++it)
r = std::max(r, m_ctx.get_assign_level(*it));
for (literal lit : antecedents)
r = std::max(r, m_ctx.get_assign_level(lit));
return r;
}
@ -335,6 +333,7 @@ namespace smt {
}
if (lvl == m_conflict_lvl) {
TRACE("conflict", m_ctx.display_literal(tout << "marking:", antecedent) << "\n";);
num_marks++;
}
else {
@ -486,6 +485,20 @@ 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;
@ -514,7 +527,7 @@ namespace smt {
get_manager().trace_stream() << "\n";
}
TRACE("conflict", tout << "processing consequent: "; m_ctx.display_literal_verbose(tout, consequent); tout << "\n";
TRACE("conflict", tout << "processing consequent: " << idx << " "; m_ctx.display_literal_verbose(tout, consequent); tout << "\n";
tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << " level: " << m_ctx.get_assign_level(consequent) << "\n";
);
SASSERT(js != null_b_justification);
@ -566,8 +579,10 @@ namespace smt {
if (m_ctx.is_marked(l.var()))
break;
CTRACE("conflict", m_ctx.get_assign_level(l) != m_conflict_lvl && m_ctx.get_assign_level(l) != m_ctx.get_base_level(),
tout << "assign_level(l): " << m_ctx.get_assign_level(l) << ", conflict_lvl: " << m_conflict_lvl << ", l: "; m_ctx.display_literal_verbose(tout, l);
tout << "\n";);
tout << "assign_level(l): " << m_ctx.get_assign_level(l) << ", conflict_lvl: ";
tout << m_conflict_lvl << ", l: "; m_ctx.display_literal_verbose(tout, l);
tout << "\n";
tout << "num marks: " << num_marks << "\n";);
SASSERT(m_ctx.get_assign_level(l) == m_conflict_lvl ||
// it may also be an (out-of-order) asserted literal
m_ctx.get_assign_level(l) == m_ctx.get_base_level());
@ -606,10 +621,8 @@ namespace smt {
*/
level_approx_set conflict_resolution::get_lemma_approx_level_set() {
level_approx_set result;
literal_vector::const_iterator it = m_lemma.begin();
literal_vector::const_iterator end = m_lemma.end();
for(; it != end; ++it)
result.insert(m_ctx.get_assign_level(*it));
for (literal l : m_lemma)
result.insert(m_ctx.get_assign_level(l));
return result;
}
@ -660,10 +673,8 @@ namespace smt {
// The method unmark_justifications must be invoked to reset these caches.
// Remark: The method reset_unmark_and_justifications invokes unmark_justifications.
justification2literals_core(js, antecedents);
literal_vector::iterator it = antecedents.begin();
literal_vector::iterator end = antecedents.end();
for(; it != end; ++it)
if (!process_antecedent_for_minimization(*it))
for (literal l : antecedents)
if (!process_antecedent_for_minimization(l))
return false;
return true;
}
@ -1063,10 +1074,8 @@ namespace smt {
m_eq2proof.reset();
m_lit2proof.reset();
m_js2proof.reset();
literal_vector::iterator it = m_lemma.begin();
literal_vector::iterator end = m_lemma.end();
for (; it != end; ++it)
m_ctx.set_mark((*it).var());
for (literal lit : m_lemma)
m_ctx.set_mark(lit.var());
}
bool conflict_resolution::visit_b_justification(literal l, b_justification js) {
@ -1246,12 +1255,9 @@ namespace smt {
SASSERT(conflict.get_kind() != b_justification::BIN_CLAUSE);
SASSERT(conflict.get_kind() != b_justification::AXIOM);
SASSERT(not_l == null_literal || conflict.get_kind() == b_justification::JUSTIFICATION);
TRACE("mk_conflict_proof", tout << "lemma literals: ";
literal_vector::iterator it = m_lemma.begin();
literal_vector::iterator end = m_lemma.end();
for (; it != end; ++it) {
m_ctx.display_literal(tout, *it);
tout << " ";
TRACE("mk_conflict_proof", tout << "lemma literals:";
for (literal lit : m_lemma) {
m_ctx.display_literal(tout << " ", lit);
}
tout << "\n";);
init_mk_proof();
@ -1328,12 +1334,10 @@ namespace smt {
pr = m_manager.mk_unit_resolution(2, prs);
}
expr_ref_buffer lits(m_manager);
literal_vector::iterator it = m_lemma.begin();
literal_vector::iterator end = m_lemma.end();
for (; it != end; ++it) {
m_ctx.unset_mark((*it).var());
for (literal lit : m_lemma) {
m_ctx.unset_mark(lit.var());
expr_ref l_expr(m_manager);
m_ctx.literal2expr(*it, l_expr);
m_ctx.literal2expr(lit, l_expr);
lits.push_back(l_expr);
}
expr * fact = 0;
@ -1369,10 +1373,8 @@ namespace smt {
literal_vector & antecedents = m_tmp_literal_vector;
antecedents.reset();
justification2literals_core(js, antecedents);
literal_vector::iterator it = antecedents.begin();
literal_vector::iterator end = antecedents.end();
for(; it != end; ++it)
process_antecedent_for_unsat_core(*it);
for (literal lit : antecedents)
process_antecedent_for_unsat_core(lit);
}
void conflict_resolution::mk_unsat_core(b_justification conflict, literal not_l) {

48
src/smt/smt_context.cpp
View file

@ -1615,11 +1615,9 @@ namespace smt {
\brief Return set of assigned literals as expressions.
*/
void context::get_assignments(expr_ref_vector& assignments) {
literal_vector::const_iterator it = m_assigned_literals.begin();
literal_vector::const_iterator end = m_assigned_literals.end();
for (; it != end; ++it) {
for (literal lit : m_assigned_literals) {
expr_ref e(m_manager);
literal2expr(*it, e);
literal2expr(lit, e);
assignments.push_back(e);
}
}
@ -1694,10 +1692,8 @@ namespace smt {
}
bool context::propagate_theories() {
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it) {
(*it)->propagate();
for (theory * t : m_theory_set) {
t->propagate();
if (inconsistent())
return false;
}
@ -1733,10 +1729,8 @@ namespace smt {
}
bool context::can_theories_propagate() const {
ptr_vector<theory>::const_iterator it = m_theory_set.begin();
ptr_vector<theory>::const_iterator end = m_theory_set.end();
for (; it != end; ++it) {
if ((*it)->can_propagate()) {
for (theory* t : m_theory_set) {
if (t->can_propagate()) {
return true;
}
}
@ -1821,7 +1815,7 @@ namespace smt {
}
void context::rescale_bool_var_activity() {
TRACE("case_split", tout << "rescale\n";);
TRACE("case_split", tout << "rescale\n";);
svector<double>::iterator it = m_activity.begin();
svector<double>::iterator end = m_activity.end();
for (; it != end; ++it)
@ -1968,10 +1962,8 @@ namespace smt {
m_case_split_queue->push_scope();
m_asserted_formulas.push_scope();
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it)
(*it)->push_scope_eh();
for (theory* t : m_theory_set)
t->push_scope_eh();
CASSERT("context", check_invariant());
}
@ -2146,10 +2138,7 @@ namespace smt {
}
for (unsigned i = new_scope_lvl; i <= lim; i++) {
clause_vector & v = m_clauses_to_reinit[i];
clause_vector::iterator it = v.begin();
clause_vector::iterator end = v.end();
for (; it != end; ++it) {
clause * cls = *it;
for (clause* cls : v) {
cache_generation(cls, new_scope_lvl);
}
}
@ -2246,10 +2235,7 @@ namespace smt {
}
for (unsigned i = m_scope_lvl+1; i <= lim; i++) {
clause_vector & v = m_clauses_to_reinit[i];
clause_vector::iterator it = v.begin();
clause_vector::iterator end = v.end();
for (; it != end; ++it) {
clause * cls = *it;
for (clause* cls : v) {
if (cls->deleted()) {
cls->release_atoms(m_manager);
cls->m_reinit = false;
@ -2922,10 +2908,8 @@ namespace smt {
TRACE("flush", tout << "m_scope_lvl: " << m_scope_lvl << "\n";);
m_relevancy_propagator = 0;
m_model_generator->reset();
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it)
(*it)->flush_eh();
for (theory* t : m_theory_set)
t->flush_eh();
undo_trail_stack(0);
m_qmanager = 0;
del_clauses(m_aux_clauses, 0);
@ -3183,10 +3167,8 @@ namespace smt {
}
void context::reset_assumptions() {
literal_vector::iterator it = m_assumptions.begin();
literal_vector::iterator end = m_assumptions.end();
for (; it != end; ++it)
get_bdata(it->var()).m_assumption = false;
for (literal lit : m_assumptions)
get_bdata(lit.var()).m_assumption = false;
m_assumptions.reset();
}

18
src/smt/smt_context.h
View file

@ -1235,24 +1235,24 @@ namespace smt {
void display_asserted_formulas(std::ostream & out) const;
void display_literal(std::ostream & out, literal l) const;
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()); }
void display_literal_info(std::ostream & out, literal l) const;
void display_literals(std::ostream & out, unsigned num_lits, literal const * lits) const;
std::ostream& display_literals(std::ostream & out, unsigned num_lits, literal const * lits) const;
void display_literals(std::ostream & out, literal_vector const& lits) const {
display_literals(out, lits.size(), lits.c_ptr());
std::ostream& display_literals(std::ostream & out, literal_vector const& lits) const {
return display_literals(out, lits.size(), lits.c_ptr());
}
void display_literal_verbose(std::ostream & out, literal lit) const;
std::ostream& display_literal_verbose(std::ostream & out, literal lit) const;
void display_literals_verbose(std::ostream & out, unsigned num_lits, literal const * lits) const;
void display_literals_verbose(std::ostream & out, literal_vector const& lits) const {
display_literals_verbose(out, lits.size(), lits.c_ptr());
std::ostream& display_literals_verbose(std::ostream & out, unsigned num_lits, literal const * lits) const;
std::ostream& display_literals_verbose(std::ostream & out, literal_vector const& lits) const {
return display_literals_verbose(out, lits.size(), lits.c_ptr());
}
void display_watch_list(std::ostream & out, literal l) const;

58
src/smt/smt_context_pp.cpp
View file

@ -71,11 +71,9 @@ namespace smt {
case NUM_CONFLICTS: r = "max-conflicts-reached"; break;
case THEORY: {
r = "(incomplete (theory";
ptr_vector<theory>::const_iterator it = m_incomplete_theories.begin();
ptr_vector<theory>::const_iterator end = m_incomplete_theories.end();
for (; it != end; ++it) {
for (theory* t : m_incomplete_theories) {
r += " ";
r += (*it)->get_name();
r += t->get_name();
}
r += "))";
break;
@ -91,20 +89,20 @@ namespace smt {
m_asserted_formulas.display_ll(out, get_pp_visited());
}
void context::display_literal(std::ostream & out, literal l) const {
l.display_compact(out, m_bool_var2expr.c_ptr());
std::ostream& context::display_literal(std::ostream & out, literal l) const {
l.display_compact(out, m_bool_var2expr.c_ptr()); return out;
}
void context::display_literals(std::ostream & out, unsigned num_lits, literal const * lits) const {
display_compact(out, num_lits, lits, m_bool_var2expr.c_ptr());
std::ostream& context::display_literals(std::ostream & out, unsigned num_lits, literal const * lits) const {
display_compact(out, num_lits, lits, m_bool_var2expr.c_ptr()); return out;
}
void context::display_literal_verbose(std::ostream & out, literal lit) const {
display_literals_verbose(out, 1, &lit);
std::ostream& context::display_literal_verbose(std::ostream & out, literal lit) const {
return display_literals_verbose(out, 1, &lit);
}
void context::display_literals_verbose(std::ostream & out, unsigned num_lits, literal const * lits) const {
display_verbose(out, m_manager, num_lits, lits, m_bool_var2expr.c_ptr(), "\n");
std::ostream& context::display_literals_verbose(std::ostream & out, unsigned num_lits, literal const * lits) const {
display_verbose(out, m_manager, num_lits, lits, m_bool_var2expr.c_ptr(), "\n"); return out;
}
void context::display_literal_info(std::ostream & out, literal l) const {
@ -136,10 +134,8 @@ namespace smt {
}
void context::display_enode_defs(std::ostream & out) const {
ptr_vector<enode>::const_iterator it = m_enodes.begin();
ptr_vector<enode>::const_iterator end = m_enodes.end();
for (; it != end; ++it) {
expr * n = (*it)->get_owner();
for (enode * x : m_enodes) {
expr * n = x->get_owner();
ast_def_ll_pp(out, m_manager, n, get_pp_visited(), true, false);
}
}
@ -169,10 +165,8 @@ namespace smt {
}
void context::display_clauses(std::ostream & out, ptr_vector<clause> const & v) const {
ptr_vector<clause>::const_iterator it = v.begin();
ptr_vector<clause>::const_iterator end = v.end();
for (; it != end; ++it) {
display_clause(out, *it);
for (clause* cp : v) {
display_clause(out, cp);
out << "\n";
}
}
@ -207,12 +201,10 @@ namespace smt {
void context::display_assignment(std::ostream & out) const {
if (!m_assigned_literals.empty()) {
out << "current assignment:\n";
literal_vector::const_iterator it = m_assigned_literals.begin();
literal_vector::const_iterator end = m_assigned_literals.end();
for (; it != end; ++it) {
display_literal(out, *it);
for (literal lit : m_assigned_literals) {
display_literal(out, lit);
out << ": ";
display_verbose(out, m_manager, 1, &*it, m_bool_var2expr.c_ptr());
display_verbose(out, m_manager, 1, &lit, m_bool_var2expr.c_ptr());
out << "\n";
}
}
@ -223,11 +215,9 @@ namespace smt {
pp.set_benchmark_name("lemma");
pp.set_status("unknown");
pp.set_logic(logic);
literal_vector::const_iterator it = m_assigned_literals.begin();
literal_vector::const_iterator end = m_assigned_literals.end();
for (; it != end; ++it) {
for (literal lit : m_assigned_literals) {
expr_ref n(m_manager);
literal2expr(*it, n);
literal2expr(lit, n);
pp.add_assumption(n);
}
pp.display_smt2(out, m_manager.mk_true());
@ -235,11 +225,9 @@ namespace smt {
void context::display_eqc(std::ostream & out) const {
bool first = true;
ptr_vector<enode>::const_iterator it = m_enodes.begin();
ptr_vector<enode>::const_iterator end = m_enodes.end();
for (; it != end; ++it) {
expr * n = (*it)->get_owner();
expr * r = (*it)->get_root()->get_owner();
for (enode * x : m_enodes) {
expr * n = x->get_owner();
expr * r = x->get_root()->get_owner();
if (n != r) {
if (first) {
out << "equivalence classes:\n";
@ -610,7 +598,7 @@ namespace smt {
break;
}
case b_justification::JUSTIFICATION: {
out << "justification ";
out << "justification " << j.get_justification()->get_from_theory() << ": ";
literal_vector lits;
const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
display_literals(out, lits.size(), lits.c_ptr());

1
src/solver/solver_pool.cpp
View file

@ -143,7 +143,6 @@ public:
}
out << ")\n";
m_base->display(out, num_assumptions, assumptions);
bool first = true;
out << "(check-sat";
for (unsigned i = 0; i < num_assumptions; ++i) {
out << " " << mk_pp(assumptions[i], m);