mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

fixes to dt_solver and related

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-02-27 11:03:20 -08:00
parent f7b1469462
commit 830f314a3f
20 changed files with 250 additions and 187 deletions
Download patch file Download diff file Expand all files Collapse all files

228
src/sat/smt/dt_solver.cpp
View file

@ -103,9 +103,11 @@ namespace dt {
expr* e1 = n1->get_expr();
if (antecedent == sat::null_literal)
add_unit(eq_internalize(e1, e2));
else if (s().value(antecedent) == l_true)
ctx.propagate(n1, e_internalize(e2), euf::th_propagation::mk(*this, antecedent));
else
else if (s().value(antecedent) == l_true) {
euf::enode* n2 = e_internalize(e2);
ctx.propagate(n1, n2, euf::th_propagation::propagate(*this, antecedent, n1, n2));
}
else
add_clause(~antecedent, eq_internalize(e1, e2));
}
@ -114,24 +116,17 @@ namespace dt {
where acc_i are the accessors of constructor c.
*/
void solver::assert_is_constructor_axiom(enode* n, func_decl* c, literal antecedent) {
expr* e = n->get_expr();
TRACE("dt", tout << "creating axiom (= n (c (acc_1 n) ... (acc_m n))) for\n"
<< mk_pp(c, m) << " " << mk_pp(e, m) << "\n";);
TRACE("dt", tout << mk_pp(c, m) << " " << ctx.bpp(n) << "\n";);
m_stats.m_assert_cnstr++;
expr* e = n->get_expr();
SASSERT(dt.is_constructor(c));
SASSERT(is_datatype(e));
SASSERT(c->get_range() == e->get_sort());
m_args.reset();
ptr_vector<func_decl> const& accessors = *dt.get_constructor_accessors(c);
SASSERT(c->get_arity() == accessors.size());
for (func_decl* d : accessors)
for (func_decl* d : *dt.get_constructor_accessors(c))
m_args.push_back(m.mk_app(d, e));
expr_ref con(m.mk_app(c, m_args), m);
assert_eq_axiom(n, con, antecedent);
enode* n2 = e_internalize(con);
theory_var v1 = n->get_th_var(get_id());
theory_var v2 = n2->get_th_var(get_id());
m_find.merge(v1, v2);
}
/**
@ -142,13 +137,11 @@ namespace dt {
*/
void solver::assert_accessor_axioms(enode* n) {
m_stats.m_assert_accessor++;
expr* e = n->get_expr();
SASSERT(is_constructor(n));
expr* e = n->get_expr();
func_decl* d = n->get_decl();
ptr_vector<func_decl> const& accessors = *dt.get_constructor_accessors(d);
SASSERT(n->num_args() == accessors.size());
unsigned i = 0;
for (func_decl* acc : accessors) {
for (func_decl* acc : *dt.get_constructor_accessors(d)) {
app_ref acc_app(m.mk_app(acc, e), m);
assert_eq_axiom(n->get_arg(i), acc_app);
++i;
@ -167,8 +160,7 @@ namespace dt {
literal l = ctx.enode2literal(r);
SASSERT(s().value(l) == l_false);
clear_mark();
auto* jst = euf::th_propagation::mk(*this, ~l, c, r->get_arg(0));
ctx.set_conflict(jst);
ctx.set_conflict(euf::th_propagation::conflict(*this, ~l, c, r->get_arg(0)));
}
/**
@ -228,11 +220,11 @@ namespace dt {
else if (is_recognizer(n))
;
else {
sort* s = n->get_expr()->get_sort();
sort* s = n->get_sort();
if (dt.get_datatype_num_constructors(s) == 1)
assert_is_constructor_axiom(n, dt.get_datatype_constructors(s)->get(0));
else if (get_config().m_dt_lazy_splits == 0 || (get_config().m_dt_lazy_splits == 1 && !s->is_infinite()))
mk_split(r);
mk_split(r, false);
}
return r;
}
@ -242,12 +234,12 @@ namespace dt {
\brief Create a new case split for v. That is, create the atom (is_mk v) and mark it as relevant.
If first is true, it means that v does not have recognizer yet.
*/
void solver::mk_split(theory_var v) {
void solver::mk_split(theory_var v, bool is_final) {
m_stats.m_splits++;
v = m_find.find(v);
enode* n = var2enode(v);
sort* srt = n->get_expr()->get_sort();
sort* srt = n->get_sort();
func_decl* non_rec_c = dt.get_non_rec_constructor(srt);
unsigned non_rec_idx = dt.get_constructor_idx(non_rec_c);
var_data* d = m_var_data[v];
@ -258,32 +250,37 @@ namespace dt {
enode* recognizer = d->m_recognizers.get(non_rec_idx, nullptr);
if (recognizer == nullptr)
r = dt.get_constructor_is(non_rec_c);
else if (ctx.value(recognizer) != l_false) {
// if is l_true, then we are done
// otherwise wait for recognizer to be assigned.
if (is_final) s().display(std::cout);
VERIFY(!is_final);
return;
}
else {
// look for a slot of d->m_recognizers that is 0, or it is not marked as relevant and is unassigned.
unsigned idx = 0;
ptr_vector<func_decl> const& constructors = *dt.get_datatype_constructors(srt);
for (enode* curr : d->m_recognizers) {
auto const& constructors = *dt.get_datatype_constructors(srt);
for (enode* curr : d->m_recognizers) {
if (curr == nullptr) {
// found empty slot...
r = dt.get_constructor_is(constructors[idx]);
break;
}
else if (ctx.value(curr) != l_false) {
VERIFY(!is_final);
return;
}
++idx;
}
if (r == nullptr)
if (r == nullptr) {
VERIFY(!is_final);
return; // all recognizers are asserted to false... conflict will be detected...
}
}
SASSERT(r != nullptr);
app_ref r_app(m.mk_app(r, n->get_expr()), m);
@ -308,10 +305,10 @@ namespace dt {
TRACE("dt", tout << "apply_sort_cnstr: #" << n->get_expr_id() << " " << mk_pp(n->get_expr(), m) << "\n";);
TRACE("dt_bug",
tout << "apply_sort_cnstr:\n" << mk_pp(n->get_expr(), m) << " ";
tout << dt.is_datatype(s) << " ";
if (dt.is_datatype(s)) tout << "is-infinite: " << s->is_infinite() << " ";
if (dt.is_datatype(s)) tout << "attached: " << is_attached_to_var(n) << " ";
tout << "\n";);
tout << dt.is_datatype(s) << " ";
if (dt.is_datatype(s)) tout << "is-infinite: " << s->is_infinite() << " ";
if (dt.is_datatype(s)) tout << "attached: " << is_attached_to_var(n) << " ";
tout << "\n";);
if (!is_attached_to_var(n) &&
(/*ctx.has_quantifiers()*/ true ||
@ -342,52 +339,52 @@ namespace dt {
func_decl* c = dt.get_recognizer_constructor(r);
if (!lit.sign()) {
SASSERT(tv != euf::null_theory_var);
if (d->m_constructor != nullptr && d->m_constructor->get_decl() == c)
if (d->m_constructor && d->m_constructor->get_decl() == c)
return; // do nothing
assert_is_constructor_axiom(arg, c, lit);
}
else if (d->m_constructor == nullptr) // make sure a constructor is attached
propagate_recognizer(tv, n);
else if (d->m_constructor == nullptr) // make sure a constructor is attached
propagate_recognizer(tv, n);
else if (d->m_constructor->get_decl() == c) // conflict
sign_recognizer_conflict(d->m_constructor, n);
}
void solver::add_recognizer(theory_var v, enode* recognizer) {
TRACE("dt", tout << "add recognizer " << v << " " << mk_pp(recognizer->get_expr(), m) << "\n";);
SASSERT(is_recognizer(recognizer));
v = m_find.find(v);
var_data* d = m_var_data[v];
sort* s = recognizer->get_decl()->get_domain(0);
if (d->m_recognizers.empty()) {
SASSERT(dt.is_datatype(s));
SASSERT(is_recognizer(recognizer));
SASSERT(dt.is_datatype(s));
if (d->m_recognizers.empty())
d->m_recognizers.resize(dt.get_datatype_num_constructors(s), nullptr);
}
SASSERT(d->m_recognizers.size() == dt.get_datatype_num_constructors(s));
unsigned c_idx = dt.get_recognizer_constructor_idx(recognizer->get_decl());
if (d->m_recognizers[c_idx] == nullptr) {
lbool val = ctx.value(recognizer);
TRACE("dt", tout << "adding recognizer to v" << v << " rec: #" << recognizer->get_expr_id() << " val: " << val << "\n";);
if (val == l_true) {
// do nothing...
// If recognizer assignment was already processed, then
// d->m_constructor is already set.
// Otherwise, it will be set when asserted is invoked.
return;
}
if (val == l_false && d->m_constructor != nullptr) {
func_decl* c_decl = dt.get_recognizer_constructor(recognizer->get_decl());
if (d->m_constructor->get_decl() == c_decl) {
// conflict
sign_recognizer_conflict(d->m_constructor, recognizer);
}
return;
}
SASSERT(val == l_undef || (val == l_false && d->m_constructor == nullptr));
d->m_recognizers[c_idx] = recognizer;
ctx.push(set_vector_idx_trail<enode>(d->m_recognizers, c_idx));
if (val == l_false)
propagate_recognizer(v, recognizer);
if (d->m_recognizers[c_idx])
return;
lbool val = ctx.value(recognizer);
TRACE("dt", tout << "adding recognizer to v" << v << " rec: #" << recognizer->get_expr_id() << " val: " << val << "\n";);
// do nothing...
// If recognizer assignment was already processed, then
// d->m_constructor is already set.
// Otherwise, it will be set when asserted is invoked.
if (val == l_true)
return;
if (val == l_false && d->m_constructor) {
// conflict
if (d->m_constructor->get_decl() == dt.get_recognizer_constructor(recognizer->get_decl()))
sign_recognizer_conflict(d->m_constructor, recognizer);
return;
}
SASSERT(val == l_undef || (val == l_false && !d->m_constructor));
ctx.push(set_vector_idx_trail<enode>(d->m_recognizers, c_idx));
d->m_recognizers[c_idx] = recognizer;
if (val == l_false)
propagate_recognizer(v, recognizer);
}
/**
@ -400,27 +397,22 @@ namespace dt {
unsigned num_unassigned = 0;
unsigned unassigned_idx = UINT_MAX;
enode* n = var2enode(v);
sort* srt = n->get_expr()->get_sort();
sort* srt = n->get_sort();
var_data* d = m_var_data[v];
if (d->m_recognizers.empty()) {
theory_var w = recognizer->get_arg(0)->get_th_var(get_id());
SASSERT(w != euf::null_theory_var);
add_recognizer(w, recognizer);
add_recognizer(v, recognizer);
return;
}
CTRACE("dt", d->m_recognizers.empty(), ctx.display(tout););
SASSERT(!d->m_recognizers.empty());
literal_vector lits;
enode_pair_vector eqs;
unsigned idx = 0;
for (enode* r : d->m_recognizers) {
if (!r) {
if (num_unassigned == 0)
unassigned_idx = idx;
num_unassigned++;
}
else if (ctx.value(r) == l_true)
if (r && ctx.value(r) == l_true)
return; // nothing to be propagated
else if (ctx.value(r) == l_false) {
if (r && ctx.value(r) == l_false) {
SASSERT(r->num_args() == 1);
lits.push_back(~ctx.enode2literal(r));
if (n != r->get_arg(0)) {
@ -431,30 +423,35 @@ namespace dt {
eqs.push_back(euf::enode_pair(n, r->get_arg(0)));
}
}
else {
if (num_unassigned == 0)
unassigned_idx = idx;
++num_unassigned;
}
++idx;
}
TRACE("dt", tout << "propagate " << num_unassigned << " eqs: " << eqs.size() << "\n";);
if (num_unassigned == 0)
ctx.set_conflict(euf::th_propagation::mk(*this, lits, eqs));
ctx.set_conflict(euf::th_propagation::conflict(*this, lits, eqs));
else if (num_unassigned == 1) {
// propagate remaining recognizer
SASSERT(!lits.empty());
enode* r = d->m_recognizers[unassigned_idx];
literal consequent;
if (!r) {
ptr_vector<func_decl> const& constructors = *dt.get_datatype_constructors(srt);
func_decl* rec = dt.get_constructor_is(constructors[unassigned_idx]);
if (r)
consequent = ctx.enode2literal(r);
else {
func_decl* con = (*dt.get_datatype_constructors(srt))[unassigned_idx];
func_decl* rec = dt.get_constructor_is(con);
app_ref rec_app(m.mk_app(rec, n->get_expr()), m);
consequent = mk_literal(rec_app);
}
else
consequent = ctx.enode2literal(r);
ctx.propagate(consequent, euf::th_propagation::mk(*this, lits, eqs));
ctx.propagate(consequent, euf::th_propagation::propagate(*this, lits, eqs, consequent));
}
else if (get_config().m_dt_lazy_splits == 0 || (!srt->is_infinite() && get_config().m_dt_lazy_splits == 1))
// there are more than 2 unassigned recognizers...
// if eager splits are enabled... create new case split
mk_split(v);
mk_split(v, false);
}
void solver::merge_eh(theory_var v1, theory_var v2, theory_var, theory_var) {
@ -465,22 +462,20 @@ namespace dt {
var_data* d2 = m_var_data[v2];
auto* con1 = d1->m_constructor;
auto* con2 = d2->m_constructor;
if (con2 != nullptr) {
if (con1 == nullptr) {
ctx.push(set_ptr_trail<enode>(con1));
// check whether there is a recognizer in d1 that conflicts with con2;
if (!d1->m_recognizers.empty()) {
unsigned c_idx = dt.get_constructor_idx(con2->get_decl());
enode* recognizer = d1->m_recognizers[c_idx];
if (recognizer != nullptr && ctx.value(recognizer) == l_false) {
sign_recognizer_conflict(con2, recognizer);
return;
}
if (con1 && con2 && con1->get_decl() != con2->get_decl())
ctx.set_conflict(euf::th_propagation::conflict(*this, con1, con2));
else if (con2 && !con1) {
ctx.push(set_ptr_trail<enode>(d1->m_constructor));
// check whether there is a recognizer in d1 that conflicts with con2;
if (!d1->m_recognizers.empty()) {
unsigned c_idx = dt.get_constructor_idx(con2->get_decl());
enode* recognizer = d1->m_recognizers[c_idx];
if (recognizer && ctx.value(recognizer) == l_false) {
sign_recognizer_conflict(con2, recognizer);
return;
}
d1->m_constructor = con2;
}
else if (con1->get_decl() != con2->get_decl())
add_unit(~eq_internalize(con1->get_expr(), con2->get_expr()));
d1->m_constructor = con2;
}
for (enode* e : d2->m_recognizers)
if (e)
@ -523,7 +518,7 @@ namespace dt {
};
for (enode* arg : euf::enode_args(parentc)) {
add(arg);
sort* s = arg->get_expr()->get_sort();
sort* s = arg->get_sort();
if (m_autil.is_array(s) && dt.is_datatype(get_array_range(s)))
for (enode* aarg : get_array_args(arg))
add(aarg);
@ -638,7 +633,7 @@ namespace dt {
if (res) {
clear_mark();
ctx.set_conflict(euf::th_propagation::mk(*this, m_used_eqs));
ctx.set_conflict(euf::th_propagation::conflict(*this, m_used_eqs));
TRACE("dt", tout << "occurs check conflict: " << ctx.bpp(n) << "\n";);
}
return res;
@ -652,23 +647,20 @@ namespace dt {
int start = s().rand()();
for (int i = 0; i < num_vars; i++) {
theory_var v = (i + start) % num_vars;
if (v == static_cast<int>(m_find.find(v))) {
enode* node = var2enode(v);
if (!is_datatype(node))
continue;
if (!oc_cycle_free(node) && occurs_check(node))
// conflict was detected...
return sat::check_result::CR_CONTINUE;
if (get_config().m_dt_lazy_splits > 0) {
// using lazy case splits...
var_data* d = m_var_data[v];
if (d->m_constructor == nullptr) {
clear_mark();
mk_split(v);
r = sat::check_result::CR_CONTINUE;
}
}
}
if (v != static_cast<int>(m_find.find(v)))
continue;
enode* node = var2enode(v);
if (!is_datatype(node))
continue;
if (dt.is_recursive(node->get_sort()) && !oc_cycle_free(node) && occurs_check(node))
return sat::check_result::CR_CONTINUE;
if (get_config().m_dt_lazy_splits == 0)
continue;
if (m_var_data[v]->m_constructor)
continue;
clear_mark();
mk_split(v, true);
r = sat::check_result::CR_CONTINUE;
}
return r;
}
@ -704,7 +696,7 @@ namespace dt {
return;
euf::enode* con = m_var_data[m_find.find(v)]->m_constructor;
if (con->num_args() == 0)
dep.insert(n, nullptr);
dep.insert(n, nullptr);
for (enode* arg : euf::enode_args(con))
dep.add(n, arg->get_root());
}
@ -750,7 +742,7 @@ namespace dt {
SASSERT(!n->is_attached_to(get_id()));
if (is_constructor(term) || is_update_field(term)) {
for (enode* arg : euf::enode_args(n)) {
sort* s = arg->get_expr()->get_sort();
sort* s = arg->get_sort();
if (dt.is_datatype(s))
mk_var(arg);
else if (m_autil.is_array(s) && dt.is_datatype(get_array_range(s))) {
@ -759,20 +751,20 @@ namespace dt {
}
}
mk_var(n);
}
else if (is_recognizer(term)) {
mk_var(n);
enode* arg = n->get_arg(0);
theory_var v = mk_var(arg);
add_recognizer(v, n);
add_recognizer(v, n);
}
else {
SASSERT(is_accessor(term));
SASSERT(n->num_args() == 1);
mk_var(n->get_arg(0));
}
return true;
}