Skip to content

Commit

Permalink
solve for fold, expand rewrites under fold/map
Browse files Browse the repository at this point in the history 
Occurrences of map and fold are interpreted.
They are defined when the seq argument is expanded into a finite
concatenation. The ensure this expansion takes place, each fold/map term
is registered and defined through rewrites when the seq argument simplifies.
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Sep 11, 2022
1 parent 53611f4 commit 809838f
Show file tree
Hide file tree
Showing 2 changed files with 84 additions and 20 deletions.
102 changes: 82 additions & 20 deletions src/smt/theory_seq.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -418,6 +418,10 @@ final_check_status theory_seq::final_check_eh() {
TRACEFIN("fixed_length");
return FC_CONTINUE;
}
if (solve_recfuns()) {
TRACEFIN("solve_recfun");
return FC_CONTINUE;
}
if (m_unhandled_expr) {
TRACEFIN("give_up");
TRACE("seq", tout << "unhandled: " << mk_pp(m_unhandled_expr, m) << "\n";);
Expand Down Expand Up @@ -642,11 +646,9 @@ bool theory_seq::check_extensionality() {
\brief check negated contains constraints.
*/
bool theory_seq::check_contains() {
for (unsigned i = 0; !ctx.inconsistent() && i < m_ncs.size(); ++i) {
if (solve_nc(i)) {
for (unsigned i = 0; !ctx.inconsistent() && i < m_ncs.size(); ++i)
if (solve_nc(i))
m_ncs.erase_and_swap(i--);
}
}
return m_new_propagation || ctx.inconsistent();
}

Expand Down Expand Up @@ -809,9 +811,9 @@ void theory_seq::set_conflict(enode_pair_vector const& eqs, literal_vector const
}

bool theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) {
if (n1->get_root() == n2->get_root()) {
if (n1->get_root() == n2->get_root())
return false;
}

literal_vector lits;
enode_pair_vector eqs;
linearize(dep, eqs, lits);
Expand Down Expand Up @@ -985,9 +987,8 @@ bool theory_seq::is_var(expr* a) const {


bool theory_seq::add_solution(expr* l, expr* r, dependency* deps) {
if (l == r) {
if (l == r)
return false;
}
m_new_solution = true;
m_rep.update(l, r, deps);
enode* n1 = ensure_enode(l);
Expand All @@ -1000,11 +1001,11 @@ bool theory_seq::add_solution(expr* l, expr* r, dependency* deps) {
}

bool theory_seq::propagate_max_length(expr* l, expr* r, dependency* deps) {
unsigned idx;
expr* s;
if (m_util.str.is_empty(l)) {
if (m_util.str.is_empty(l))
std::swap(l, r);
}

unsigned idx;
expr* s = nullptr;
rational hi;
if (m_sk.is_tail_u(l, s, idx) && has_length(s) && m_util.str.is_empty(r) && !upper_bound(s, hi)) {
propagate_lit(deps, 0, nullptr, m_ax.mk_le(mk_len(s), idx+1));
Expand Down Expand Up @@ -1240,12 +1241,31 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
return false;
}


/**
* solve for fold/map (recursive function that depends on a sequence)
* Assumption: the Seq argument of fold/map expands into a concatentation of units
* The assumption is enforced by tracking the length of the seq argument.
* This is ensured in relevant_eh.
* Under the assumption, evern occurrence of fold/map gets simplified by expanding
* arguments.
*/
bool theory_seq::solve_recfuns() {
for (unsigned i = 0; i < m_recfuns.size() && !ctx.inconsistent(); ++i) {
expr* t = m_recfuns[i];
dependency* dep = nullptr;
expr_ref r(m);
if (canonize(t, dep, r) && r != t) {
add_solution(t, r, dep);
m_recfuns.erase_and_swap(i--);
}
}
return m_new_propagation || ctx.inconsistent();
}


bool theory_seq::solve_nc(unsigned idx) {
nc const& n = m_ncs[idx];
literal len_gt = n.len_gt();
literal len_gt = n.len_gt();
expr_ref c(m);
expr* a = nullptr, *b = nullptr;
VERIFY(m_util.str.is_contains(n.contains(), a, b));
Expand All @@ -1263,10 +1283,12 @@ bool theory_seq::solve_nc(unsigned idx) {
m_new_propagation = true;
return false;
case l_false:
break;
if (!m_sk.is_tail(a))
add_length_limit(a, m_max_unfolding_depth, true);
m_ax.unroll_not_contains(n.contains());
return true;
}
m_ax.unroll_not_contains(n.contains());
return true;
return false;
}

theory_seq::cell* theory_seq::mk_cell(cell* p, expr* e, dependency* d) {
Expand Down Expand Up @@ -1456,7 +1478,7 @@ bool theory_seq::internalize_term(app* term) {
mk_var(ctx.get_enode(term));
return true;
}

if (m.is_bool(term) &&
(m_util.str.is_in_re(term) || m_sk.is_skolem(term))) {
bool_var bv = ctx.mk_bool_var(term);
Expand Down Expand Up @@ -2500,8 +2522,8 @@ bool theory_seq::expand1(expr* e0, dependency*& eqs, expr_ref& result) {
dependency* deps = nullptr;
expr* e = m_rep.find(e0, deps);

expr* e1, *e2, *e3;
expr_ref arg1(m), arg2(m);
expr* e1, *e2, *e3, *e4;
expr_ref arg1(m), arg2(m), arg3(m), arg4(m);
if (m_util.str.is_concat(e, e1, e2)) {
arg1 = try_expand(e1, deps);
arg2 = try_expand(e2, deps);
Expand Down Expand Up @@ -2546,6 +2568,30 @@ bool theory_seq::expand1(expr* e0, dependency*& eqs, expr_ref& result) {
if (!arg1 || !arg2) return true;
result = m_util.str.mk_index(arg1, arg2, e3);
}
else if (m_util.str.is_map(e, e1, e2)) {
arg2 = try_expand(e2, deps);
if (!arg2) return true;
result = m_util.str.mk_map(e1, arg2);
ctx.get_rewriter()(result);
}
else if (m_util.str.is_mapi(e, e1, e2, e3)) {
arg3 = try_expand(e3, deps);
if (!arg3) return true;
result = m_util.str.mk_mapi(e1, e2, arg3);
ctx.get_rewriter()(result);
}
else if (m_util.str.is_foldl(e, e1, e2, e3)) {
arg3 = try_expand(e3, deps);
if (!arg3) return true;
result = m_util.str.mk_foldl(e1, e2, arg3);
ctx.get_rewriter()(result);
}
else if (m_util.str.is_foldli(e, e1, e2, e3, e4)) {
arg4 = try_expand(e4, deps);
if (!arg4) return true;
result = m_util.str.mk_foldli(e1, e2, e3, arg4);
ctx.get_rewriter()(result);
}
#if 0
else if (m_util.str.is_nth_i(e, e1, e2)) {
arg1 = try_expand(e1, deps);
Expand Down Expand Up @@ -2890,6 +2936,11 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter

void theory_seq::add_axiom(literal_vector & lits) {
TRACE("seq", ctx.display_literals_verbose(tout << "assert " << lits << " :", lits) << "\n";);

for (literal lit : lits)
if (ctx.get_assignment(lit) == l_true)
return;

for (literal lit : lits)
ctx.mark_as_relevant(lit);

Expand Down Expand Up @@ -3164,6 +3215,7 @@ void theory_seq::push_scope_eh() {
m_nqs.push_scope();
m_ncs.push_scope();
m_lts.push_scope();
m_recfuns.push_scope();
m_regex.push_scope();
}

Expand All @@ -3177,6 +3229,7 @@ void theory_seq::pop_scope_eh(unsigned num_scopes) {
m_nqs.pop_scope(num_scopes);
m_ncs.pop_scope(num_scopes);
m_lts.pop_scope(num_scopes);
m_recfuns.pop_scope(num_scopes);
m_regex.pop_scope(num_scopes);
m_rewrite.reset();
if (ctx.get_base_level() > ctx.get_scope_level() - num_scopes) {
Expand Down Expand Up @@ -3214,6 +3267,15 @@ void theory_seq::relevant_eh(app* n) {
add_int_string(n);
}

expr* fn, *acc, *i, *s;
if (m_util.str.is_foldl(n, fn, acc, s) ||
m_util.str.is_foldli(n, fn, i, acc, s) ||
m_util.str.is_map(n, fn, s) ||
m_util.str.is_mapi(n, fn, i, s)) {
add_length_to_eqc(s);
m_recfuns.push_back(n);
}

if (m_util.str.is_ubv2s(n))
add_ubv_string(n);

Expand Down
2 changes: 2 additions & 0 deletions src/smt/theory_seq.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -328,6 +328,7 @@ namespace smt {
scoped_vector<ne> m_nqs; // set of current disequalities.
scoped_vector<nc> m_ncs; // set of non-contains constraints.
scoped_vector<expr*> m_lts; // set of asserted str.<, str.<= literals
scoped_vector<expr*> m_recfuns; // set of recursive functions that are defined by unfolding seq argument (map/fold)
bool m_lts_checked;
unsigned m_eq_id;
th_union_find m_find;
Expand Down Expand Up @@ -484,6 +485,7 @@ namespace smt {
bool solve_nqs(unsigned i);
bool solve_ne(unsigned i);
bool solve_nc(unsigned i);
bool solve_recfuns();
bool check_ne_literals(unsigned idx, unsigned& num_undef_lits);
bool propagate_ne2lit(unsigned idx);
bool propagate_ne2eq(unsigned idx);
Expand Down

0 comments on commit 809838f

Please sign in to comment.