diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp index 4dfa3fef2..387922dab 100644 --- a/src/sat/smt/dt_solver.cpp +++ b/src/sat/smt/dt_solver.cpp @@ -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()); diff --git a/src/sat/smt/dt_solver.h b/src/sat/smt/dt_solver.h index 785912170..2dd4929d3 100644 --- a/src/sat/smt/dt_solver.h +++ b/src/sat/smt/dt_solver.h @@ -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); diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 26eb4bc6e..47d9ebf3e 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -483,7 +483,7 @@ namespace smt { for (int v = 0; v < num_vars; v++) { if (v == static_cast(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))); + } + }; diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h index 155a18a63..6c4f1f4c8 100644 --- a/src/smt/theory_datatype.h +++ b/src/smt/theory_datatype.h @@ -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 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;