mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

optimize for enumeration datatypes

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-02-28 21:28:13 -08:00
parent caae0ba569
commit f725989225
4 changed files with 125 additions and 82 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -135,13 +135,13 @@ namespace dt {
...
(= (acc_m n) a_m)
*/
void solver::assert_accessor_axioms(enode* n) {
m_stats.m_assert_accessor++;
void solver::assert_accessor_axioms(enode* n) {
SASSERT(is_constructor(n));
expr* e = n->get_expr();
func_decl* d = n->get_decl();
unsigned i = 0;
for (func_decl* acc : *dt.get_constructor_accessors(d)) {
m_stats.m_assert_accessor++;
app_ref acc_app(m.mk_app(acc, e), m);
assert_eq_axiom(n->get_arg(i), acc_app);
++i;
@ -214,12 +214,9 @@ namespace dt {
d->m_constructor = n;
assert_accessor_axioms(n);
}
else if (is_update_field(n)) {
assert_update_field_axioms(n);
}
else if (is_recognizer(n))
;
else {
else if (is_update_field(n))
assert_update_field_axioms(n);
else if (!is_recognizer(n)) {
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));
@ -245,52 +242,33 @@ namespace dt {
}
func_decl* non_rec_c = dt.get_non_rec_constructor(srt);
unsigned non_rec_idx = dt.get_constructor_idx(non_rec_c);
unsigned non_rec_idx = dt.get_constructor_idx(non_rec_c);
var_data* d = m_var_data[v];
SASSERT(d->m_constructor == nullptr);
enode* recognizer = d->m_recognizers.get(non_rec_idx, nullptr);
func_decl* r = nullptr;
SASSERT(!d->m_constructor);
SASSERT(!recognizer || ctx.value(recognizer) == l_false || !is_final);
TRACE("dt", tout << "non_rec_c: " << non_rec_c->get_name() << " #rec: " << d->m_recognizers.size() << "\n";);
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;
if (!recognizer && non_rec_c->get_arity() == 0) {
sat::literal eq = eq_internalize(n->get_expr(), m.mk_const(non_rec_c));
s().set_phase(eq);
if (s().value(eq) == l_false)
mk_enum_split(v);
}
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;
auto const& constructors = *dt.get_datatype_constructors(srt);
else if (!recognizer)
mk_recognizer_constructor_literal(non_rec_c, n);
else if (ctx.value(recognizer) == l_false)
mk_enum_split(v);
}
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) {
VERIFY(!is_final);
return; // all recognizers are asserted to false... conflict will be detected...
}
}
SASSERT(r != nullptr);
sat::literal solver::mk_recognizer_constructor_literal(func_decl* c, euf::enode* n) {
func_decl* r = dt.get_constructor_is(c);
app_ref r_app(m.mk_app(r, n->get_expr()), m);
TRACE("dt", tout << "creating split: " << mk_pp(r_app, m) << "\n";);
sat::literal lit = mk_literal(r_app);
s().set_phase(lit);
return lit;
}
void solver::mk_enum_split(theory_var v) {
@ -301,54 +279,59 @@ namespace dt {
unsigned sz = constructors.size();
int start = s().rand()();
m_lits.reset();
sat::literal lit;
for (unsigned i = 0; i < sz; ++i) {
unsigned j = (i + start) % sz;
sat::literal lit = eq_internalize(n->get_expr(), m.mk_const(constructors[j]));
switch (s().value(lit)) {
case l_undef:
s().set_phase(lit);
return;
case l_true:
return;
case l_false:
func_decl* c = constructors[j];
if (c->get_arity() > 0) {
enode* curr = d->m_recognizers.get(j, nullptr);
if (curr && ctx.value(curr) != l_false)
return;
lit = mk_recognizer_constructor_literal(c, n);
if (!curr)
return;
if (s().value(lit) != l_false)
return;
m_lits.push_back(~lit);
break;
}
else {
lit = eq_internalize(n->get_expr(), m.mk_const(c));
switch (s().value(lit)) {
case l_undef:
s().set_phase(lit);
return;
case l_true:
return;
case l_false:
m_lits.push_back(~lit);
break;
}
}
}
ctx.set_conflict(euf::th_explain::conflict(*this, m_lits));
}
/**
* Remark: If s is an infinite sort, then it is not necessary to create
* a theory variable.
*
* Actually, when the logical context has quantifiers, it is better to
* disable this optimization.
* Example:
*
* (forall (l list) (a Int) (= (len (cons a l)) (+ (len l) 1)))
* (assert (> (len a) 1)
*
* If the theory variable is not created for 'a', then a wrong model will be generated.
*
*/
void solver::apply_sort_cnstr(enode* n, sort* s) {
TRACE("dt", tout << "apply_sort_cnstr: #" << ctx.bpp(n) << "\n";);
force_push();
// Remark: If s is an infinite sort, then it is not necessary to create
// a theory variable.
//
// Actually, when the logical context has quantifiers, it is better to
// disable this optimization.
// Example:
//
// (forall (l list) (a Int) (= (len (cons a l)) (+ (len l) 1)))
// (assert (> (len a) 1)
//
// If the theory variable is not created for 'a', then a wrong model will be generated.
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";);
if (!is_attached_to_var(n) &&
(/*ctx.has_quantifiers()*/ true ||
(dt.is_datatype(s) && dt.has_nested_arrays()) ||
(dt.is_datatype(s) && !s->is_infinite()))) {
mk_var(n);
}
if (!is_attached_to_var(n))
mk_var(n);
}
void solver::new_eq_eh(euf::th_eq const& eq) {
force_push();
m_find.merge(eq.v1(), eq.v2());

2
src/sat/smt/dt_solver.h
View file

@ -129,6 +129,8 @@ namespace dt {
bool visited(expr* e) override;
bool post_visit(expr* e, bool sign, bool root) override;
void clone_var(solver& src, theory_var v);
sat::literal mk_recognizer_constructor_literal(func_decl* c, euf::enode* n);
public:
solver(euf::solver& ctx, theory_id id);

57
src/smt/theory_datatype.cpp
View file

@ -483,7 +483,7 @@ namespace smt {
for (int v = 0; v < num_vars; v++) {
if (v == static_cast<int>(m_find.find(v))) {
enode * node = get_enode(v);
if (!oc_cycle_free(node) && occurs_check(node)) {
if (m_util.is_recursive(node->get_sort()) && !oc_cycle_free(node) && occurs_check(node)) {
// conflict was detected...
// return...
return FC_CONTINUE;
@ -956,6 +956,10 @@ namespace smt {
v = m_find.find(v);
enode * n = get_enode(v);
sort * s = n->get_sort();
if (m_util.is_enum_sort(s)) {
mk_enum_split(v);
return;
}
func_decl * non_rec_c = m_util.get_non_rec_constructor(s);
unsigned non_rec_idx = m_util.get_constructor_idx(non_rec_c);
var_data * d = m_var_data[v];
@ -1015,4 +1019,55 @@ namespace smt {
ctx.mark_as_relevant(bv);
}
literal theory_datatype::mk_recognizer_constructor_literal(func_decl* c, enode* n) {
func_decl* r = m_util.get_constructor_is(c);
app_ref r_app(m.mk_app(r, n->get_expr()), m);
bool_var bv = ctx.get_bool_var(r_app);
ctx.set_true_first_flag(bv);
ctx.mark_as_relevant(bv);
return literal(bv, false);
}
void theory_datatype::mk_enum_split(theory_var v) {
enode* n = get_enode(v);
var_data* d = m_var_data[v];
sort* srt = n->get_sort();
auto const& constructors = *m_util.get_datatype_constructors(srt);
unsigned sz = constructors.size();
int start = ctx.get_random_value();
m_lits.reset();
literal lit;
for (unsigned i = 0; i < sz; ++i) {
unsigned j = (i + start) % sz;
func_decl* c = constructors[j];
if (c->get_arity() > 0) {
enode* curr = d->m_recognizers.get(j, nullptr);
if (curr && ctx.get_assignment(curr) != l_false)
return;
lit = mk_recognizer_constructor_literal(c, n);
if (!curr)
return;
if (ctx.get_assignment(lit) != l_false)
return;
m_lits.push_back(~lit);
}
else {
lit = mk_eq(n->get_expr(), m.mk_const(c), false);
switch (ctx.get_assignment(lit)) {
case l_undef:
ctx.set_true_first_flag(lit.var());
return;
case l_true:
return;
case l_false:
m_lits.push_back(~lit);
break;
}
}
}
region& reg = ctx.get_region();
ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), reg, m_lits.size(), m_lits.c_ptr(), 0, nullptr)));
}
};

3
src/smt/theory_datatype.h
View file

@ -80,6 +80,7 @@ namespace smt {
enode_pair_vector m_used_eqs; // conflict, if any
parent_tbl m_parent; // parent explanation for occurs_check
svector<stack_entry> m_stack; // stack for DFS for occurs_check
literal_vector m_lits;
void clear_mark();
@ -108,6 +109,8 @@ namespace smt {
void explain_is_child(enode* parent, enode* child);
void mk_split(theory_var v);
literal mk_recognizer_constructor_literal(func_decl* c, enode* n);
void mk_enum_split(theory_var v);
void display_var(std::ostream & out, theory_var v) const;