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

Merge branch 'str-at-semantics' into develop

Browse source
This commit is contained in:
Murphy Berzish 2017-03-13 14:40:40 -04:00
commit 94d5f242b8
35 changed files with 799 additions and 66 deletions
Download patch file Download diff file Expand all files Collapse all files

84
src/smt/smt_context.cpp
View file

@ -306,7 +306,6 @@ namespace smt {
TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " ";
display_literal_verbose(tout, l); tout << " level: " << m_scope_lvl << "\n";
display(tout, j););
SASSERT(l.var() < static_cast<int>(m_b_internalized_stack.size()));
m_assigned_literals.push_back(l);
m_assignment[l.index()] = l_true;
m_assignment[(~l).index()] = l_false;
@ -321,14 +320,23 @@ namespace smt {
d.m_phase_available = true;
d.m_phase = !l.sign();
TRACE("phase_selection", tout << "saving phase, is_pos: " << d.m_phase << " l: " << l << "\n";);
TRACE("relevancy",
tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(bool_var2expr(l.var())) << "\n";);
if (d.is_atom() && (m_fparams.m_relevancy_lvl == 0 || (m_fparams.m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(bool_var2expr(l.var()))))
tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(l) << "\n";);
if (d.is_atom() && (m_fparams.m_relevancy_lvl == 0 || (m_fparams.m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(l)))
m_atom_propagation_queue.push_back(l);
if (m_manager.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() {
@ -1637,7 +1645,7 @@ namespace smt {
m_atom_propagation_queue.push_back(literal(v, val == l_false));
}
}
TRACE("propagate_relevancy", tout << "marking as relevant:\n" << mk_bounded_pp(n, m_manager) << "\n";);
TRACE("propagate_relevancy", tout << "marking as relevant:\n" << mk_bounded_pp(n, m_manager) << " " << m_scope_lvl << "\n";);
#ifndef SMTCOMP
m_case_split_queue->relevant_eh(n);
#endif
@ -3895,6 +3903,7 @@ namespace smt {
// I invoke pop_scope_core instead of pop_scope because I don't want
// to reset cached generations... I need them to rebuild the literals
// of the new conflict clause.
if (relevancy()) record_relevancy(num_lits, lits);
unsigned num_bool_vars = pop_scope_core(m_scope_lvl - new_lvl);
SASSERT(m_scope_lvl == new_lvl);
// the logical context may still be in conflict after
@ -3926,6 +3935,7 @@ namespace smt {
}
}
}
if (relevancy()) restore_relevancy(num_lits, lits);
// Resetting the cache manually because I did not invoke pop_scope, but pop_scope_core
reset_cache_generation();
TRACE("resolve_conflict_bug",
@ -4008,6 +4018,28 @@ namespace smt {
}
return false;
}
/*
\brief we record and restore relevancy information for literals in conflict clauses.
A literal may have been marked relevant within the scope that gets popped during
conflict resolution. In this case, the literal is no longer marked as relevant after
the pop. This can cause quantifier instantiation to miss relevant triggers and thereby
cause incmpleteness.
*/
void context::record_relevancy(unsigned n, literal const* lits) {
m_relevant_conflict_literals.reset();
for (unsigned i = 0; i < n; ++i) {
m_relevant_conflict_literals.push_back(is_relevant(lits[i]));
}
}
void context::restore_relevancy(unsigned n, literal const* lits) {
for (unsigned i = 0; i < n; ++i) {
if (m_relevant_conflict_literals[i] && !is_relevant(lits[i])) {
mark_as_relevant(lits[i]);
}
}
}
void context::get_relevant_labels(expr* cnstr, buffer<symbol> & result) {
if (m_fparams.m_check_at_labels) {
@ -4281,6 +4313,7 @@ namespace smt {
if (fcs == FC_DONE) {
mk_proto_model(l_true);
m_model = m_proto_model->mk_model();
add_rec_funs_to_model();
}
return fcs == FC_DONE;
@ -4333,8 +4366,51 @@ namespace smt {
return m_last_search_failure;
}
void context::add_rec_funs_to_model() {
ast_manager& m = m_manager;
SASSERT(m_model);
for (unsigned i = 0; i < m_asserted_formulas.get_num_formulas(); ++i) {
expr* e = m_asserted_formulas.get_formula(i);
if (is_quantifier(e)) {
quantifier* q = to_quantifier(e);
if (!m.is_rec_fun_def(q)) continue;
SASSERT(q->get_num_patterns() == 1);
expr* fn = to_app(q->get_pattern(0))->get_arg(0);
SASSERT(is_app(fn));
func_decl* f = to_app(fn)->get_decl();
expr* eq = q->get_expr();
expr_ref body(m);
if (is_fun_def(fn, q->get_expr(), body)) {
func_interp* fi = alloc(func_interp, m, f->get_arity());
fi->set_else(body);
m_model->register_decl(f, fi);
}
}
}
}
bool context::is_fun_def(expr* f, expr* body, expr_ref& result) {
expr* t1, *t2, *t3;
if (m_manager.is_eq(body, t1, t2) || m_manager.is_iff(body, t1, t2)) {
if (t1 == f) return result = t2, true;
if (t2 == f) return result = t1, true;
return false;
}
if (m_manager.is_ite(body, t1, t2, t3)) {
expr_ref body1(m_manager), body2(m_manager);
if (is_fun_def(f, t2, body1) && is_fun_def(f, t3, body2)) {
// f is not free in t1
result = m_manager.mk_ite(t1, body1, body2);
return true;
}
}
return false;
}
};
#ifdef Z3DEBUG
void pp(smt::context & c) {
c.display(std::cout);