diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index f4a890a2c..aea27b6e7 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -30,6 +30,7 @@ Revision History: #include"fpa_rewriter.h" #include"rewriter_def.h" #include"cooperate.h" +#include"ast_pp.h" struct evaluator_cfg : public default_rewriter_cfg { @@ -42,6 +43,7 @@ struct evaluator_cfg : public default_rewriter_cfg { pb_rewriter m_pb_rw; fpa_rewriter m_f_rw; seq_rewriter m_seq_rw; + array_util m_ar; unsigned long long m_max_memory; unsigned m_max_steps; bool m_model_completion; @@ -59,7 +61,8 @@ struct evaluator_cfg : public default_rewriter_cfg { m_dt_rw(m), m_pb_rw(m), m_f_rw(m), - m_seq_rw(m) { + m_seq_rw(m), + m_ar(m) { bool flat = true; m_b_rw.set_flat(flat); m_a_rw.set_flat(flat); @@ -146,6 +149,8 @@ struct evaluator_cfg : public default_rewriter_cfg { st = m_f_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_seq_rw.get_fid()) st = m_seq_rw.mk_eq_core(args[0], args[1], result); + else if (fid == m_ar_rw.get_fid()) + st = mk_array_eq(args[0], args[1], result); if (st != BR_FAILED) return st; } @@ -182,6 +187,7 @@ struct evaluator_cfg : public default_rewriter_cfg { return st; } + bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) { #define TRACE_MACRO TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";); @@ -230,6 +236,85 @@ struct evaluator_cfg : public default_rewriter_cfg { bool cache_results() const { return m_cache; } + + br_status mk_array_eq(expr* a, expr* b, expr_ref& result) { + if (a == b) { + result = m().mk_true(); + return BR_DONE; + } + vector stores; + expr_ref else1(m()), else2(m()); + if (extract_array_func_interp(a, stores, else1) && + extract_array_func_interp(b, stores, else2)) { + expr_ref_vector conj(m()), args1(m()), args2(m()); + conj.push_back(m().mk_eq(else1, else2)); + args1.push_back(a); + args2.push_back(b); + for (unsigned i = 0; i < stores.size(); ++i) { + args1.resize(1); args1.append(stores[i].size() - 1, stores[i].c_ptr()); + args2.resize(1); args2.append(stores[i].size() - 1, stores[i].c_ptr()); + expr* s1 = m_ar.mk_select(args1.size(), args1.c_ptr()); + expr* s2 = m_ar.mk_select(args2.size(), args2.c_ptr()); + conj.push_back(m().mk_eq(s1, s2)); + } + result = m().mk_and(conj.size(), conj.c_ptr()); + return BR_REWRITE_FULL; + } + return BR_FAILED; + } + + bool extract_array_func_interp(expr* a, vector& stores, expr_ref& else_case) { + SASSERT(m_ar.is_array(a)); + + while (m_ar.is_store(a)) { + expr_ref_vector store(m()); + store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1); + stores.push_back(store); + a = to_app(a)->get_arg(0); + } + + if (m_ar.is_const(a)) { + else_case = to_app(a)->get_arg(0); + return true; + } + + if (m_ar.is_as_array(a)) { + func_decl* f = m_ar.get_as_array_func_decl(to_app(a)); + func_interp* g = m_model.get_func_interp(f); + unsigned sz = g->num_entries(); + unsigned arity = f->get_arity(); + for (unsigned i = 0; i < sz; ++i) { + expr_ref_vector store(m()); + func_entry const* fe = g->get_entry(i); + store.append(arity, fe->get_args()); + store.push_back(fe->get_result()); + for (unsigned j = 0; j < store.size(); ++j) { + if (!is_ground(store[j].get())) { + TRACE("model_evaluator", tout << "could not extract array interpretation: " << mk_pp(a, m()) << "\n" << mk_pp(store[j].get(), m()) << "\n";); + return false; + } + } + stores.push_back(store); + } + else_case = g->get_else(); + if (!else_case) { + TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m()) << "\n";); + return false; + } + if (!is_ground(else_case)) { + TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m()) << "\n" << mk_pp(else_case, m()) << "\n";); + return false; + } + TRACE("model_evaluator", tout << "else case: " << mk_pp(else_case, m()) << "\n";); + return true; + } + TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m()) << "\n";); + + return false; + } + + + }; template class rewriter_tpl; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index adff16c35..7aa92f315 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -258,7 +258,7 @@ final_check_status theory_seq::final_check_eh() { TRACE("seq", tout << ">>fixed_length\n";); return FC_CONTINUE; } - if (branch_variable()) { + if (reduce_length_eq() || branch_variable_mb() || branch_variable()) { ++m_stats.m_branch_variable; TRACE("seq", tout << ">>branch_variable\n";); return FC_CONTINUE; @@ -291,8 +291,7 @@ final_check_status theory_seq::final_check_eh() { return FC_GIVEUP; } - -bool theory_seq::branch_variable() { +bool theory_seq::reduce_length_eq() { context& ctx = get_context(); unsigned sz = m_eqs.size(); int start = ctx.get_random_value(); @@ -304,7 +303,182 @@ bool theory_seq::branch_variable() { return true; } } + return false; +} +bool theory_seq::branch_variable_mb() { + context& ctx = get_context(); + unsigned sz = m_eqs.size(); + int start = ctx.get_random_value(); + bool change = false; + for (unsigned i = 0; i < sz; ++i) { + unsigned k = (i + start) % sz; + eq const& e = m_eqs[i]; + vector len1, len2; + if (!enforce_length(e.ls(), len1) || !enforce_length(e.rs(), len2)) { + change = true; + continue; + } + if (e.ls().empty() || e.rs().empty() || (!is_var(e.ls()[0]) && !is_var(e.rs()[0]))) { + continue; + } + rational l1, l2; + for (unsigned i = 0; i < len1.size(); ++i) l1 += len1[i]; + for (unsigned i = 0; i < len2.size(); ++i) l2 += len2[i]; + if (l1 != l2) { + TRACE("seq", tout << "lengths are not compatible\n";); + expr_ref l = mk_concat(e.ls().size(), e.ls().c_ptr()); + expr_ref r = mk_concat(e.rs().size(), e.rs().c_ptr()); + expr_ref lnl(m_util.str.mk_length(l), m), lnr(m_util.str.mk_length(r), m); + add_axiom(~mk_eq(l, r, false), mk_eq(lnl, lnr, false)); + change = true; + continue; + } + if (split_lengths(e.dep(), e.ls(), e.rs(), len1, len2)) { + return true; + } + } + + return change; +} + +/* + \brief Decompose ls = rs into Xa = bYc, such that + 1. + - X != Y + - |b| <= |X| <= |bY| in currrent model + - b is non-empty. + 2. X != Y + - b is empty + - |X| <= |Y| + 3. |X| = 0 + - propagate X = empty +*/ +bool theory_seq::split_lengths(dependency* dep, + expr_ref_vector const& ls, expr_ref_vector const& rs, + vector const& ll, vector const& rl) { + context& ctx = get_context(); + expr_ref X(m), Y(m), b(m); + if (ls.empty() || rs.empty()) { + return false; + } + if (is_var(ls[0]) && ll[0].is_zero()) { + return set_empty(ls[0]); + } + if (is_var(rs[0]) && rl[0].is_zero()) { + return set_empty(rs[0]); + } + if (is_var(rs[0]) && !is_var(ls[0])) { + return split_lengths(dep, rs, ls, rl, ll); + } + if (!is_var(ls[0])) { + return false; + } + X = ls[0]; + rational lenX = ll[0]; + expr_ref_vector bs(m); + SASSERT(lenX.is_pos()); + rational lenB(0), lenY(0); + for (unsigned i = 0; lenX > lenB && i < rs.size(); ++i) { + bs.push_back(rs[i]); + lenY = rl[i]; + lenB += lenY; + } + SASSERT(lenX <= lenB); + SASSERT(!bs.empty()); + Y = bs.back(); + bs.pop_back(); + if (!is_var(Y) && !m_util.str.is_unit(Y)) { + TRACE("seq", tout << "TBD: non variable or unit split: " << Y << "\n";); + return false; + } + if (X == Y) { + TRACE("seq", tout << "Cycle: " << X << "\n";); + return false; + } + if (lenY.is_zero()) { + return set_empty(Y); + } + b = mk_concat(bs, m.get_sort(X)); + + SASSERT(X != Y); + expr_ref split_pred = mk_skolem(symbol("seq.split"), X, b, Y, m.mk_bool_sort()); + literal split_predl = mk_literal(split_pred); + lbool is_split = ctx.get_assignment(split_predl); + if (is_split != l_true) { + // split_pred <=> |b| < |X| <= |b| + |Y| + expr_ref lenX(m_util.str.mk_length(X), m); + expr_ref lenY(m_util.str.mk_length(Y), m); + expr_ref lenb(m_util.str.mk_length(b), m); + expr_ref le1(m_autil.mk_le(mk_sub(lenX, lenb), m_autil.mk_int(0)), m); + expr_ref le2(m_autil.mk_le(mk_sub(mk_sub(lenX, lenb), lenY), + m_autil.mk_int(0)), m); + literal lit1(~mk_literal(le1)); + literal lit2(mk_literal(le2)); + add_axiom(~split_predl, lit1); + add_axiom(~split_predl, lit2); + add_axiom(split_predl, ~lit1, ~lit2); + } + else if (m_util.str.is_unit(Y)) { + SASSERT(lenB == lenX); + SASSERT(is_split == l_true); + bs.push_back(Y); + expr_ref bY(m_util.str.mk_concat(bs), m); + literal_vector lits; + lits.push_back(split_predl); + propagate_eq(dep, lits, X, bY, true); + } + else { + SASSERT(is_var(Y)); + // split_pred => X = bY1, Y = Y1Y2 + SASSERT(is_split == l_true); + expr_ref Y1(mk_skolem(symbol("seq.left"), Y), m); + expr_ref Y2(mk_skolem(symbol("seq.right"), Y), m); + expr_ref bY1(m_util.str.mk_concat(b, Y1), m); + expr_ref Y1Y2(m_util.str.mk_concat(Y1, Y2), m); + literal_vector lits; + lits.push_back(split_predl); + propagate_eq(dep, lits, X, bY1, true); + propagate_eq(dep, lits, Y, Y1Y2, true); + } + return true; +} + +bool theory_seq::set_empty(expr* x) { + add_axiom(~mk_eq(m_autil.mk_int(0), m_util.str.mk_length(x), false), mk_eq_empty(x)); + return true; +} + +bool theory_seq::enforce_length(expr_ref_vector const& es, vector & len) { + bool all_have_length = true; + rational val; + zstring s; + for (unsigned i = 0; i < es.size(); ++i) { + expr* e = es[i]; + if (m_util.str.is_unit(e)) { + len.push_back(rational(1)); + } + else if (m_util.str.is_empty(e)) { + len.push_back(rational(0)); + } + else if (m_util.str.is_string(e, s)) { + len.push_back(rational(s.length())); + } + else if (get_length(e, val)) { + len.push_back(val); + } + else { + enforce_length(ensure_enode(e)); + all_have_length = false; + } + } + return all_have_length; +} + +bool theory_seq::branch_variable() { + context& ctx = get_context(); + unsigned sz = m_eqs.size(); + int start = ctx.get_random_value(); unsigned s = 0; for (unsigned i = 0; i < sz; ++i) { @@ -3050,6 +3224,9 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { else if (m_util.str.is_in_re(e)) { propagate_in_re(e, is_true); } + else if (is_skolem(symbol("seq.split"), e)) { + // propagate equalities + } else { UNREACHABLE(); } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 8206eeca4..1af809d8e 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -358,6 +358,8 @@ namespace smt { void init_model(expr_ref_vector const& es); // final check bool simplify_and_solve_eqs(); // solve unitary equalities + bool reduce_length_eq(); + bool branch_variable_mb(); // branch on a variable, model based on length bool branch_variable(); // branch on a variable bool split_variable(); // split a variable bool is_solved(); @@ -367,6 +369,10 @@ namespace smt { bool fixed_length(); bool fixed_length(expr* e); bool propagate_length_coherence(expr* e); + bool split_lengths(dependency* dep, + expr_ref_vector const& ls, expr_ref_vector const& rs, + vector const& ll, vector const& rl); + bool set_empty(expr* x); bool check_extensionality(); bool check_contains(); @@ -465,6 +471,7 @@ namespace smt { bool has_length(expr *e) const { return m_length.contains(e); } void add_length(expr* e); void enforce_length(enode* n); + bool enforce_length(expr_ref_vector const& es, vector& len); void enforce_length_coherence(enode* n1, enode* n2); void add_elim_string_axiom(expr* n);