From 3e9479d01a8c709138e051ad1932697db9a9913e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 17 Apr 2020 18:21:40 -0700 Subject: [PATCH] a lot of seq churn Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bv_trailing.cpp | 92 +++++++- src/ast/rewriter/bv_trailing.h | 2 + src/smt/seq_axioms.cpp | 147 ++++++++++++- src/smt/seq_axioms.h | 12 +- src/smt/seq_skolem.cpp | 22 +- src/smt/seq_skolem.h | 8 +- src/smt/smt_theory.h | 6 + src/smt/theory_seq.cpp | 356 ++++++++----------------------- src/smt/theory_seq.h | 14 +- src/util/trail.h | 11 + 10 files changed, 388 insertions(+), 282 deletions(-) diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp index da962b729..85578db39 100644 --- a/src/ast/rewriter/bv_trailing.cpp +++ b/src/ast/rewriter/bv_trailing.cpp @@ -5,15 +5,24 @@ bv_trailing.cpp - Abstract: - - Author: Mikolas Janota (MikolasJanota) Revision History: + +NSB code review: +This code needs to be rewritten or just removed. + +The main issue is that the analysis and extraction steps are separated. +They are out of sync and therefore buggy. +A saner implementation does the trailing elimination on a pair of vectors. +The vectors are initially singltons. They are expanded when processing a concat. +The vector with the largest bit-width is reduced maximally. +If it cannot be reduced, then bits are padded to align the two vectors. + --*/ + #include "ast/rewriter/bv_trailing.h" #include "ast/bv_decl_plugin.h" #include "ast/ast_pp.h" @@ -39,12 +48,11 @@ struct bv_trailing::imp { , m(mk_extract.m()) { TRACE("bv-trailing", tout << "ctor\n";); - for (unsigned i = 0; i <= TRAILING_DEPTH; ++i) - m_count_cache[i] = nullptr; + for (unsigned i = 0; i <= TRAILING_DEPTH; ++i) + m_count_cache[i] = nullptr; } virtual ~imp() { - TRACE("bv-trailing", tout << "dtor\n";); reset_cache(0); } @@ -73,6 +81,10 @@ struct bv_trailing::imp { TRACE("bv-trailing", tout << min << "\n";); VERIFY(min == remove_trailing(e1, min, out1, TRAILING_DEPTH)); VERIFY(min == remove_trailing(e2, min, out2, TRAILING_DEPTH)); + if (m.get_sort(out1) != m.get_sort(out2)) { + TRACE("bv-trailing", tout << "bug\n";); + return BR_FAILED; + } const bool are_eq = m.are_equal(out1, out2); result = are_eq ? m.mk_true() : m.mk_eq(out1, out2); return are_eq ? BR_DONE : BR_REWRITE2; @@ -413,3 +425,71 @@ unsigned bv_trailing::remove_trailing(expr * e, unsigned n, expr_ref& result) { void bv_trailing::reset_cache(unsigned condition) { m_imp->reset_cache(condition); } + +#if 0 +sketch + + + void remove_trailing(expr* e1, expr* e2, expr_ref& result) { + SASSERT(m_util.is_bv(e1) && m_util.is_bv(e2)); + SASSERT(m_util.get_bv_size(e1) == m_util.get_bv_size(e2)); + unsigned sz1 = m_util.get_bv_size(e1); + unsigned sz2 = sz1; + expr_ref_vector ls(m), rs(m); + ls.push_back(e1); + rs.push_back(e2); + while (true) { + if (sz1 < sz2) { + std::swap(sz1, sz2); + ls.swap(rs); + } + if (sz2 == 0) { + result = m.mk_true(); + return BR_DONE; + } + if (try_remove(sz1, ls)) + continue; + if (sz1 == m_util.get_bv_size(e1)) + return BR_FAILED; + if (sz1 > sz2) { + rs.push_back(m_util.mk_numeral(0, sz1 - sz2)); + } + expr_ref l(m_util.mk_concat(ls.size(), ls.c_ptr()), m); + expr_ref r(m_util.mk_concat(rs.size(), rs.c_ptr()), m); + result = m.mk_eq(l, r); + return BR_REWRITE3; + } + } + + bool try_remove(unsigned& sz, expr_ref_vector& es) { + SASSERT(!es.empty()); + expr_ref b(es.back(), m); + if (m_util.is_concat(b)) { + es.pop_back(); + for (expr* arg : *to_app(b)) { + es.push_back(arg); + } + return true; + } + if (m_util.is_numeral(e, e_val, e_sz)) { + unsigned new_sz = remove_trailing(e_sz, a); + if (new_sz == 0) { + es.pop_back(b); + sz -= e_sz; + return true; + } + if (new_sz == e_sz) { + return false; + } + sz -= (e_sz - new_sz); + es.pop_back(b); + es.push_back(m_util.mk_numeral(a, new_sz)); + return true; + } + if (m_util.is_bv_mul(e)) { + + } + return false; + } + +#endif diff --git a/src/ast/rewriter/bv_trailing.h b/src/ast/rewriter/bv_trailing.h index 3ad46cb5d..1b42dd9c1 100644 --- a/src/ast/rewriter/bv_trailing.h +++ b/src/ast/rewriter/bv_trailing.h @@ -29,6 +29,7 @@ class bv_trailing { // Remove trailing zeros from both sides of an equality (might give False). br_status eq_remove_trailing(expr * e1, expr * e2, expr_ref& result); + private: // Gives a lower and upper bound on trailing zeros in e. void count_trailing(expr * e, unsigned& min, unsigned& max); @@ -37,6 +38,7 @@ class bv_trailing { // Removing the bit-width of e, sets result to NULL. unsigned remove_trailing(expr * e, unsigned n, expr_ref& result); + public: // Reset cache(s) if it exceeded size condition. void reset_cache(unsigned condition); protected: diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp index d93a9524a..97db818dd 100644 --- a/src/smt/seq_axioms.cpp +++ b/src/smt/seq_axioms.cpp @@ -32,7 +32,8 @@ seq_axioms::seq_axioms(theory& th, th_rewriter& r): m(r.m()), a(m), seq(m), - m_sk(m, r) + m_sk(m, r), + m_digits_initialized(false) {} literal seq_axioms::mk_eq(expr* a, expr* b) { @@ -45,6 +46,13 @@ expr_ref seq_axioms::mk_sub(expr* x, expr* y) { return result; } +expr_ref seq_axioms::mk_len(expr* s) { + expr_ref result(seq.str.mk_length(s), m); + m_rewrite(result); + return result; +} + + literal seq_axioms::mk_literal(expr* _e) { expr_ref e(_e, m); @@ -546,6 +554,34 @@ void seq_axioms::add_stoi_axiom(expr* e) { add_axiom(~mk_literal(seq.str.mk_is_empty(s)), mk_eq(seq.str.mk_stoi(s), a.mk_int(-1))); } +/** + stoi(s) >= 0 => + s != empty + s = unit(head) + tail + stoi(s) = 10*digit(head) + stoi(tail) or tail = empty + stoi(s) = digit(head) or tail != empty + is_digit(head) + (tail = empty or stoi(tail) >= 0) + */ +void seq_axioms::add_stoi_non_empty_axiom(expr* e) { + expr* s = nullptr; + VERIFY (seq.str.is_stoi(e, s)); + expr_ref head(m), tail(m); + m_sk.decompose(s, head, tail); + expr_ref first_char = mk_nth(s, a.mk_int(0)); + literal ge0 = mk_literal(a.mk_ge(e, a.mk_int(0))); + literal tail_empty = mk_eq_empty(tail); + expr_ref first_digit = m_sk.mk_digit2int(first_char); + expr_ref stoi_tail(seq.str.mk_stoi(tail), m); + add_axiom(~ge0, ~mk_literal(seq.str.mk_is_empty(s))); + add_axiom(~ge0, mk_seq_eq(s, mk_concat(head, tail))); + add_axiom(~ge0, tail_empty, mk_eq(a.mk_add(a.mk_mul(a.mk_int(10), first_digit), stoi_tail), e)); + add_axiom(~ge0, ~tail_empty, mk_eq(first_digit, e)); + add_axiom(~ge0, is_digit(first_char)); + add_axiom(~ge0, tail_empty, mk_literal(a.mk_ge(stoi_tail, a.mk_int(0)))); +} + + /** e1 < e2 => prefix(e1, e2) or e1 = xcy e1 < e2 => prefix(e1, e2) or c < d e1 < e2 => prefix(e1, e2) or e2 = xdz e1 < e2 => e1 != e2 @@ -604,3 +640,112 @@ void seq_axioms::add_unit_axiom(expr* n) { add_axiom(mk_eq(u, m_sk.mk_unit_inv(n))); } +void seq_axioms::add_suffix_axiom(expr* e) { + expr* e1 = nullptr, *e2 = nullptr; + VERIFY(seq.str.is_suffix(e, e1, e2)); + literal lit = mk_literal(e); + literal e1_gt_e2 = mk_literal(a.mk_ge(mk_sub(mk_len(e1), mk_len(e2)), a.mk_int(1))); + sort* char_sort = nullptr; + VERIFY(seq.is_seq(m.get_sort(e1), char_sort)); + expr_ref x = m_sk.mk(symbol("seq.suffix.x"), e1, e2); + expr_ref y = m_sk.mk(symbol("seq.suffix.y"), e1, e2); + expr_ref z = m_sk.mk(symbol("seq.suffix.z"), e1, e2); + expr_ref c = m_sk.mk(symbol("seq.suffix.c"), e1, e2, nullptr, nullptr, char_sort); + expr_ref d = m_sk.mk(symbol("seq.suffix.d"), e1, e2, nullptr, nullptr, char_sort); + add_axiom(lit, e1_gt_e2, mk_seq_eq(e1, mk_concat(y, seq.str.mk_unit(c), x))); + add_axiom(lit, e1_gt_e2, mk_seq_eq(e2, mk_concat(z, seq.str.mk_unit(d), x))); + add_axiom(lit, e1_gt_e2, ~mk_eq(c, d)); +} + +void seq_axioms::add_prefix_axiom(expr* e) { + expr* e1 = nullptr, *e2 = nullptr; + VERIFY(seq.str.is_prefix(e, e1, e2)); + literal lit = mk_literal(e); + literal e1_gt_e2 = mk_literal(a.mk_ge(mk_sub(mk_len(e1), mk_len(e2)), a.mk_int(1))); + sort* char_sort = nullptr; + VERIFY(seq.is_seq(m.get_sort(e1), char_sort)); + expr_ref x = m_sk.mk(symbol("seq.prefix.x"), e1, e2); + expr_ref y = m_sk.mk(symbol("seq.prefix.y"), e1, e2); + expr_ref z = m_sk.mk(symbol("seq.prefix.z"), e1, e2); + expr_ref c = m_sk.mk(symbol("seq.prefix.c"), e1, e2, nullptr, nullptr, char_sort); + expr_ref d = m_sk.mk(symbol("seq.prefix.d"), e1, e2, nullptr, nullptr, char_sort); + add_axiom(lit, e1_gt_e2, mk_seq_eq(e1, mk_concat(x, seq.str.mk_unit(c), y))); + add_axiom(lit, e1_gt_e2, mk_seq_eq(e2, mk_concat(x, seq.str.mk_unit(d), z)), mk_seq_eq(e2, x)); + add_axiom(lit, e1_gt_e2, ~mk_eq(c, d)); +} + +literal seq_axioms::is_digit(expr* ch) { + literal isd = mk_literal(m_sk.mk_is_digit(ch)); + expr_ref d2i = m_sk.mk_digit2int(ch); + expr_ref _lo(seq.mk_le(seq.mk_char('0'), ch), m); + expr_ref _hi(seq.mk_le(ch, seq.mk_char('9')), m); + literal lo = mk_literal(_lo); + literal hi = mk_literal(_hi); + add_axiom(~lo, ~hi, isd); + add_axiom(~isd, lo); + add_axiom(~isd, hi); + return isd; +} +// n >= 0 & len(e) >= i + 1 => is_digit(e_i) for i = 0..k-1 +// n >= 0 & len(e) = k => n = sum 10^i*digit(e_i) +// n < 0 & len(e) = k => \/_i ~is_digit(e_i) for i = 0..k-1 +// 10^k <= n < 10^{k+1}-1 => len(e) => k + +void seq_axioms::add_si_axiom(expr* e, expr* n, unsigned k) { + zstring s; + expr_ref ith_char(m), num(m), coeff(m); + expr_ref_vector nums(m), chars(m); + expr_ref len = mk_len(e); + literal len_eq_k = th.mk_preferred_eq(len, a.mk_int(k)); + literal ge0 = mk_literal(a.mk_ge(n, a.mk_int(0))); + literal_vector digits; + digits.push_back(~len_eq_k); + digits.push_back(ge0); + ensure_digit_axiom(); + for (unsigned i = 0; i < k; ++i) { + ith_char = mk_nth(e, a.mk_int(i)); + literal isd = is_digit(ith_char); + literal len_ge_i1 = mk_literal(a.mk_ge(len, a.mk_int(i+1))); + add_axiom(~len_ge_i1, ~ge0, isd); + digits.push_back(~isd); + chars.push_back(seq.str.mk_unit(ith_char)); + nums.push_back(m_sk.mk_digit2int(ith_char)); + } + ctx().mk_th_axiom(th.get_id(), digits.size(), digits.c_ptr()); + rational c(1); + for (unsigned i = k; i-- > 0; c *= rational(10)) { + coeff = a.mk_int(c); + nums[i] = a.mk_mul(coeff, nums.get(i)); + } + num = a.mk_add(nums.size(), nums.c_ptr()); + m_rewrite(num); + add_axiom(~len_eq_k, ~ge0, th.mk_preferred_eq(n, num)); + add_axiom(~len_eq_k, ~ge0, th.mk_preferred_eq(e, seq.str.mk_concat(chars))); + + SASSERT(k > 0); + rational lb = power(rational(10), k - 1); + rational ub = power(rational(10), k) - 1; + literal lbl = mk_literal(a.mk_ge(n, a.mk_int(lb))); + literal ge_k = mk_literal(a.mk_ge(len, a.mk_int(k))); + // n >= lb => len(s) >= k + add_axiom(~lbl, ge_k); +} + +void seq_axioms::ensure_digit_axiom() { + if (!m_digits_initialized) { + for (unsigned i = 0; i < 10; ++i) { + expr_ref cnst(seq.mk_char('0'+i), m); + add_axiom(mk_eq(m_sk.mk_digit2int(cnst), a.mk_int(i))); + } + ctx().push_trail(value_trail(m_digits_initialized)); + m_digits_initialized = true; + } +} + + +expr_ref seq_axioms::add_length_limit(expr* s, unsigned k) { + expr_ref bound_tracker = m_sk.mk_length_limit(s, k); + literal bound_predicate = mk_literal(a.mk_le(mk_len(s), a.mk_int(k))); + add_axiom(~mk_literal(bound_tracker), bound_predicate); + return bound_tracker; +} diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h index 693159b83..8b6b57d16 100644 --- a/src/smt/seq_axioms.h +++ b/src/smt/seq_axioms.h @@ -34,6 +34,7 @@ namespace smt { arith_util a; seq_util seq; seq_skolem m_sk; + bool m_digits_initialized; literal mk_eq_empty(expr* e, bool phase = true) { return mk_eq_empty2(e, phase); } context& ctx() { return th.get_context(); } @@ -41,7 +42,7 @@ namespace smt { literal mk_literal(expr* e); literal mk_seq_eq(expr* a, expr* b) { SASSERT(seq.is_seq(a) && seq.is_seq(b)); return mk_literal(m_sk.mk_eq(a, b)); } - expr_ref mk_len(expr* s) { return expr_ref(seq.str.mk_length(s), m); } + expr_ref mk_len(expr* s); expr_ref mk_sub(expr* x, expr* y); expr_ref mk_concat(expr* e1, expr* e2, expr* e3) { return expr_ref(seq.str.mk_concat(e1, e2, e3), m); } expr_ref mk_concat(expr* e1, expr* e2) { return expr_ref(seq.str.mk_concat(e1, e2), m); } @@ -58,7 +59,7 @@ namespace smt { void add_extract_prefix_axiom(expr* e, expr* s, expr* l); void add_extract_suffix_axiom(expr* e, expr* s, expr* i); void tightest_prefix(expr* s, expr* x); - + void ensure_digit_axiom(); public: seq_axioms(theory& th, th_rewriter& r); @@ -67,6 +68,8 @@ namespace smt { std::function add_axiom5; std::function mk_eq_empty2; + void add_suffix_axiom(expr* n); + void add_prefix_axiom(expr* n); void add_extract_axiom(expr* n); void add_indexof_axiom(expr* n); void add_last_indexof_axiom(expr* n); @@ -75,9 +78,14 @@ namespace smt { void add_nth_axiom(expr* n); void add_itos_axiom(expr* n); void add_stoi_axiom(expr* n); + void add_stoi_non_empty_axiom(expr* e); void add_lt_axiom(expr* n); void add_le_axiom(expr* n); void add_unit_axiom(expr* n); + literal is_digit(expr* ch); + void add_si_axiom(expr* e, expr* n, unsigned k); + + expr_ref add_length_limit(expr* s, unsigned k); }; }; diff --git a/src/smt/seq_skolem.cpp b/src/smt/seq_skolem.cpp index ab9a8fc68..5e1c6e448 100644 --- a/src/smt/seq_skolem.cpp +++ b/src/smt/seq_skolem.cpp @@ -36,6 +36,7 @@ seq_skolem::seq_skolem(ast_manager& m, th_rewriter& rw): m_eq = "seq.eq"; m_seq_align = "seq.align"; m_max_unfolding = "seq.max_unfolding"; + m_length_limit = "seq.length_limit"; } expr_ref seq_skolem::mk(symbol const& s, expr* e1, expr* e2, expr* e3, expr* e4, sort* range) { @@ -53,6 +54,21 @@ expr_ref seq_skolem::mk_max_unfolding_depth(unsigned depth) { return expr_ref(m.mk_const(f), m); } +expr_ref seq_skolem::mk_length_limit(expr* e, unsigned d) { + parameter ps[3] = { parameter(m_length_limit), parameter(d), parameter(e) }; + func_decl* f = m.mk_func_decl(seq.get_family_id(), _OP_SEQ_SKOLEM, 3, ps, 0, (sort*const*) nullptr, m.mk_bool_sort()); + return expr_ref(m.mk_const(f), m); +} + +bool seq_skolem::is_length_limit(expr* p, unsigned& lim, expr*& s) const { + if (!is_length_limit(p)) + return false; + lim = to_app(p)->get_parameter(1).get_int(); + s = to_expr(to_app(p)->get_parameter(2).get_ast()); + return true; +} + + bool seq_skolem::is_skolem(symbol const& s, expr* e) const { return seq.is_skolem(e) && to_app(e)->get_decl()->get_parameter(0).get_symbol() == s; } @@ -64,7 +80,7 @@ void seq_skolem::decompose(expr* e, expr_ref& head, expr_ref& tail) { decompose_main: if (seq.str.is_empty(e)) { - head = seq.str.mk_unit(seq.str.mk_nth(e, a.mk_int(0))); + head = seq.str.mk_unit(seq.str.mk_nth_i(e, a.mk_int(0))); tail = e; } else if (seq.str.is_string(e, s)) { @@ -93,12 +109,12 @@ decompose_main: else if (is_skolem(m_tail, e) && a.is_numeral(to_app(e)->get_arg(1), r)) { expr* s = to_app(e)->get_arg(0); expr* idx = a.mk_int(r.get_unsigned() + 1); - head = seq.str.mk_unit(seq.str.mk_nth(s, idx)); + head = seq.str.mk_unit(seq.str.mk_nth_i(s, idx)); tail = mk(m_tail, s, idx); m_rewrite(head); } else { - head = seq.str.mk_unit(seq.str.mk_nth(e, a.mk_int(0))); + head = seq.str.mk_unit(seq.str.mk_nth_i(e, a.mk_int(0))); tail = mk(m_tail, e, a.mk_int(0)); m_rewrite(head); m_rewrite(tail); diff --git a/src/smt/seq_skolem.h b/src/smt/seq_skolem.h index 60dc5b565..306d99863 100644 --- a/src/smt/seq_skolem.h +++ b/src/smt/seq_skolem.h @@ -39,7 +39,7 @@ namespace smt { symbol m_pre, m_post; // inverse of at: (pre s i) + (at s i) + (post s i) = s if 0 <= i < (len s) symbol m_eq; // equality atom symbol m_seq_align; - symbol m_max_unfolding; + symbol m_max_unfolding, m_length_limit; public: @@ -79,8 +79,8 @@ namespace smt { expr_ref mk_digit2int(expr* ch) { return mk(symbol("seq.digit2int"), ch, nullptr, nullptr, nullptr, a.mk_int()); } expr_ref mk_left(expr* x, expr* y, expr* z = nullptr) { return mk("seq.left", x, y, z); } expr_ref mk_right(expr* x, expr* y, expr* z = nullptr) { return mk("seq.right", x, y, z); } - bool is_max_unfolding(expr* e) const { return is_skolem(m_max_unfolding, e); } expr_ref mk_max_unfolding_depth(unsigned d); + expr_ref mk_length_limit(expr* e, unsigned d); bool is_skolem(symbol const& s, expr* e) const; bool is_skolem(expr* e) const { return seq.is_skolem(e); } @@ -98,6 +98,10 @@ namespace smt { bool is_tail_match(expr* e, expr*& s, expr*& idx) const; bool is_tail(expr* e, expr*& s, unsigned& idx) const; bool is_digit(expr* e) const { return is_skolem(symbol("seq.is_digit"), e); } + bool is_max_unfolding(expr* e) const { return is_skolem(m_max_unfolding, e); } + bool is_length_limit(expr* e) const { return is_skolem(m_length_limit, e); } + bool is_length_limit(expr* p, unsigned& lim, expr*& s) const; + void decompose(expr* e, expr_ref& head, expr_ref& tail); diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index 466eb7c56..b34a41cff 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -113,6 +113,12 @@ namespace smt { } } + scoped_trace_stream(theory& th, literal_vector const& lits): m(th.get_manager()) { + if (m.has_trace_stream()) { + th.log_axiom_instantiation(lits); + } + } + scoped_trace_stream(theory& th, std::function& fn): m(th.get_manager()) { if (m.has_trace_stream()) { literal_vector ls; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index f9fbd8f58..ce6c512ae 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -292,6 +292,7 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params): m_axioms_head(0), m_int_string(m), m_length(m), + m_length_limit(m), m_mg(nullptr), m_rewrite(m), m_str_rewrite(m), @@ -1926,13 +1927,6 @@ bool theory_seq::check_length_coherence0(expr* e) { if (!p) { r = assume_equality(e, emp); - expr* t; - unsigned idx; - if (r != l_true && m_sk.is_tail(e, t, idx) && - idx > m_max_unfolding_depth && m_max_unfolding_lit != null_literal) { - TRACE("seq", tout << "limit unfolding " << m_max_unfolding_depth << " " << mk_pp(e, m) << "\n";); - add_axiom(~m_max_unfolding_lit, mk_eq(e, emp, false)); - } } if (p || r != l_false) { @@ -2250,35 +2244,20 @@ bool theory_seq::is_solved() { /** \brief while extracting dependency literals ensure that they have all been asserted on the context. */ -bool theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const { +void theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const { context & ctx = get_context(); DEBUG_CODE(for (literal lit : lits) SASSERT(ctx.get_assignment(lit) == l_true); ); - bool asserted = true; svector assumptions; const_cast(m_dm).linearize(dep, assumptions); for (assumption const& a : assumptions) { if (a.lit != null_literal) { lits.push_back(a.lit); - asserted &= ctx.get_assignment(a.lit) == l_true; + SASSERT(ctx.get_assignment(a.lit) == l_true); } if (a.n1 != nullptr) { eqs.push_back(enode_pair(a.n1, a.n2)); } } - if (!asserted) { - IF_VERBOSE(0, verbose_stream() << "not asserted\n";); - context& ctx = get_context(); - for (assumption const& a : assumptions) { - if (a.lit != null_literal) { - IF_VERBOSE(0, - verbose_stream() << a.lit << " " << ctx.get_assignment(a.lit) << " "; - ctx.display_literal_info(verbose_stream(), a.lit); - ctx.display_detailed_literal(verbose_stream(), a.lit) << "\n";); - } - } - exit(0); - } - return asserted; } @@ -2296,8 +2275,7 @@ void theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits ctx.mark_as_relevant(lit); enode_pair_vector eqs; - if (!linearize(dep, eqs, lits)) - return; + linearize(dep, eqs, lits); TRACE("seq", tout << "scope: " << ctx.get_scope_level() << "\n"; tout << lits << "\n"; @@ -2312,19 +2290,12 @@ void theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits m_new_propagation = true; ctx.assign(lit, js); validate_assign(lit, eqs, lits); - std::function fn = [&]() { - expr* r = ctx.bool_var2expr(lit.var()); - if (lit.sign()) r = m.mk_not(r); - return r; - }; - scoped_trace_stream _sts(*this, fn); } void theory_seq::set_conflict(dependency* dep, literal_vector const& _lits) { enode_pair_vector eqs; literal_vector lits(_lits); - if (!linearize(dep, eqs, lits)) - return; + linearize(dep, eqs, lits); m_new_propagation = true; set_conflict(eqs, lits); } @@ -2346,10 +2317,7 @@ bool theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) { context& ctx = get_context(); literal_vector lits; enode_pair_vector eqs; - if (!linearize(dep, eqs, lits)) { - TRACE("seq", tout << "not linearized\n";); - return false; - } + linearize(dep, eqs, lits); TRACE("seq_verbose", tout << "assert: " << mk_bounded_pp(n1->get_owner(), m) << " = " << mk_bounded_pp(n2->get_owner(), m) << " <-\n"; display_deps(tout, dep); @@ -3450,79 +3418,6 @@ bool theory_seq::solve_nc(unsigned idx) { add_axiom(emp, mk_eq(a, m_util.str.mk_concat(head, tail), false)); return true; -#else - dependency* deps = n.deps(); - if (!canonize(n.contains(), deps, c)) { - return false; - } - expr* a = nullptr, *b = nullptr; - - CTRACE("seq", c != n.contains(), - tout << n.contains() << " =>\n" << c << "\n"; - display_deps(tout, deps);); - if (c != n.contains()) { - IF_VERBOSE(0, verbose_stream() << n.contains() << " =>\n" << c << "\n"; - display_deps(verbose_stream(), deps);); - } - - if (m.is_true(c)) { - literal_vector lits; - set_conflict(deps, lits); - return true; - } - - if (m.is_false(c)) { - return true; - } - - if (m.is_eq(c, a, b)) { - literal eq = mk_eq(a, b, false); - ctx.mark_as_relevant(eq); - propagate_lit(deps, 0, nullptr, ~eq); - return true; - } - - if (m.is_or(c)) { - for (expr* arg : *to_app(c)) { - expr_ref ci(arg, m); - m_ncs.push_back(nc(ci, len_gt, deps)); - } - m_new_propagation = true; - return true; - } - - if (m.is_and(c)) { - enode_pair_vector eqs; - literal_vector lits; - if (!linearize(deps, eqs, lits)) { - return false; - } - for (literal& lit : lits) { - lit.neg(); - } - for (enode_pair const& p : eqs) { - lits.push_back(~mk_eq(p.first->get_owner(), p.second->get_owner(), false)); - } - for (expr* arg : *to_app(c)) { - if (m.is_eq(arg, a, b)) { - lits.push_back(~mk_eq(a, b, false)); - } - else { - lits.push_back(~mk_literal(arg)); - } - } - TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()) << "\n";); - std::function fn = [&]() { return lits; } - scoped_trace_stream(*this, fn); - ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); - return true; - } - - if (c != n.contains()) { - m_ncs.push_back(nc(c, len_gt, deps)); - m_new_propagation = true; - return true; - } #endif return false; } @@ -3749,6 +3644,32 @@ void theory_seq::add_length(expr* e, expr* l) { m_trail_stack.push(push_back_vector(m_length)); } +/** + Add length limit restrictions to sequence s. + + */ +void theory_seq::add_length_limit(expr* s, unsigned k, bool is_searching) { + expr_ref lim_e = m_ax.add_length_limit(s, k); + unsigned k0 = 0; + if (m_length_limit_map.find(s, k0)) { + SASSERT(k0 != 0); + if (k <= k0) + return; + } + m_length_limit_map.insert(s, k); + m_length_limit.push_back(lim_e); + m_trail_stack.push(push_back_vector(m_length_limit)); + if (k0 != 0) { + m_trail_stack.push(remove_obj_map(m_length_limit_map, s, k0)); + } + // std::cout << mk_pp(s, m) << " <= " << k << "\n"; + m_trail_stack.push(insert_obj_map(m_length_limit_map, s)); + if (is_searching && !get_context().at_base_level()) { + expr_ref dlimit = m_sk.mk_max_unfolding_depth(m_max_unfolding_depth); + add_axiom(~mk_literal(dlimit), mk_literal(lim_e)); + } +} + /* ensure that all elements in equivalence class occur under an application of 'length' @@ -3794,130 +3715,42 @@ bool theory_seq::check_int_string(expr* e) { (m_util.str.is_stoi(e) && add_stoi_val_axiom(e)); } - -void theory_seq::ensure_digit_axiom() { - - if (m_si_axioms.empty()) { - for (unsigned i = 0; i < 10; ++i) { - expr_ref cnst(m_util.mk_char('0'+i), m); - add_axiom(mk_eq(m_sk.mk_digit2int(cnst), m_autil.mk_int(i), false)); - } - } -} - bool theory_seq::add_itos_val_axiom(expr* e) { - rational val, val2; expr* n = nullptr; TRACE("seq", tout << mk_pp(e, m) << "\n";); VERIFY(m_util.str.is_itos(e, n)); - if (m_util.str.is_stoi(n)) { return false; } add_length_to_eqc(e); - - if (get_length(e, val) && val.is_pos() && val.is_unsigned() && - (!m_si_axioms.find(e, val2) || val != val2)) { - add_si_axiom(e, n, val.get_unsigned()); - m_si_axioms.insert(e, val); - m_trail_stack.push(push_replay(alloc(replay_is_axiom, m, e))); - m_trail_stack.push(insert_map, expr*>(m_si_axioms, e)); - return true; - } - - return false; + return add_si_axiom(e, n); } bool theory_seq::add_stoi_val_axiom(expr* e) { expr* n = nullptr; - rational val, val2; VERIFY(m_util.str.is_stoi(e, n)); - - TRACE("seq", tout << mk_pp(e, m) << " " << get_context().get_scope_level () << " " << get_length(n, val) << " " << val << "\n";); - + TRACE("seq", tout << mk_pp(e, m) << "\n";); if (m_util.str.is_itos(n)) { return false; } add_length_to_eqc(n); + return add_si_axiom(n, e); +} - if (get_length(n, val) && val.is_pos() && val.is_unsigned() && - (!m_si_axioms.find(e, val2) || val2 != val)) { - add_si_axiom(n, e, val.get_unsigned()); - m_si_axioms.insert(e, val); +bool theory_seq::add_si_axiom(expr* e, expr* n) { + rational val1; + unsigned val2 = UINT_MAX; + if (get_length(e, val1) && val1.is_pos() && val1.is_unsigned() && + (!m_si_axioms.find(e, val2) || val1.get_unsigned() != val2)) { + m_ax.add_si_axiom(e, n, val1.get_unsigned()); + m_si_axioms.insert(e, val1.get_unsigned()); m_trail_stack.push(push_replay(alloc(replay_is_axiom, m, e))); - m_trail_stack.push(insert_map, expr*>(m_si_axioms, e)); + m_trail_stack.push(insert_map, expr*>(m_si_axioms, e)); return true; } - return false; } -literal theory_seq::is_digit(expr* ch) { - literal isd = mk_literal(m_sk.mk_is_digit(ch)); - expr_ref d2i = m_sk.mk_digit2int(ch); - expr_ref _lo(m_util.mk_le(m_util.mk_char('0'), ch), m); - expr_ref _hi(m_util.mk_le(ch, m_util.mk_char('9')), m); - literal lo = mk_literal(_lo); - literal hi = mk_literal(_hi); - add_axiom(~lo, ~hi, isd); - add_axiom(~isd, lo); - add_axiom(~isd, hi); - return isd; -} - -// n >= 0 & len(e) >= i + 1 => is_digit(e_i) for i = 0..k-1 -// n >= 0 & len(e) = k => n = sum 10^i*digit(e_i) -// n < 0 & len(e) = k => \/_i ~is_digit(e_i) for i = 0..k-1 -// 10^k <= n < 10^{k+1}-1 => len(e) => k - -void theory_seq::add_si_axiom(expr* e, expr* n, unsigned k) { - - context& ctx = get_context(); - zstring s; - expr_ref ith_char(m), num(m), coeff(m); - expr_ref_vector nums(m), chars(m); - expr_ref len = mk_len(e); - literal len_eq_k = mk_preferred_eq(len, m_autil.mk_int(k)); - literal ge0 = mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0))); - literal_vector digits; - digits.push_back(~len_eq_k); - digits.push_back(ge0); - ensure_digit_axiom(); - for (unsigned i = 0; i < k; ++i) { - ith_char = mk_nth(e, m_autil.mk_int(i)); - literal isd = is_digit(ith_char); - literal len_ge_i1 = mk_literal(m_autil.mk_ge(len, m_autil.mk_int(i+1))); - add_axiom(~len_ge_i1, ~ge0, isd); - digits.push_back(~isd); - chars.push_back(m_util.str.mk_unit(ith_char)); - nums.push_back(m_sk.mk_digit2int(ith_char)); - } - ++m_stats.m_add_axiom; - ctx.mk_th_axiom(get_id(), digits.size(), digits.c_ptr()); - rational c(1); - for (unsigned i = k; i-- > 0; c *= rational(10)) { - coeff = m_autil.mk_int(c); - nums[i] = m_autil.mk_mul(coeff, nums.get(i)); - } - num = m_autil.mk_add(nums.size(), nums.c_ptr()); - ctx.get_rewriter()(num); - m_new_propagation = true; - add_axiom(~len_eq_k, ~ge0, mk_preferred_eq(n, num)); - - add_axiom(~len_eq_k, ~ge0, mk_preferred_eq(e, m_util.str.mk_concat(chars))); - - SASSERT(k > 0); - rational lb = power(rational(10), k - 1); - rational ub = power(rational(10), k) - 1; - arith_util& a = m_autil; - literal lbl = mk_literal(a.mk_ge(n, a.mk_int(lb))); - literal ge_k = mk_literal(a.mk_ge(len, a.mk_int(k))); - // n >= lb => len(s) >= k - add_axiom(~lbl, ge_k); -} - - - void theory_seq::apply_sort_cnstr(enode* n, sort* s) { mk_var(n); } @@ -4497,7 +4330,7 @@ void theory_seq::validate_conflict(enode_pair_vector const& eqs, literal_vector } void theory_seq::validate_assign(literal lit, enode_pair_vector const& eqs, literal_vector const& lits) { - IF_VERBOSE(10, display_deps(verbose_stream() << "; assign\n", lits, eqs); display_lit(verbose_stream(), ~lit)); + IF_VERBOSE(10, display_deps(verbose_stream() << "; assign\n", lits, eqs); display_lit(verbose_stream(), ~lit) << "\n"); if (get_context().get_fparams().m_seq_validate) { literal_vector _lits(lits); _lits.push_back(~lit); @@ -4815,6 +4648,7 @@ void theory_seq::deque_axiom(expr* n) { } else if (m_util.str.is_itos(n)) { m_ax.add_itos_axiom(n); + add_length_limit(n, m_max_unfolding_depth, true); } else if (m_util.str.is_stoi(n)) { m_ax.add_stoi_axiom(n); @@ -5006,12 +4840,10 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) { unsigned_vector states; a->get_epsilon_closure(a->init(), states); lits.push_back(~lit); - expr_ref_vector exprs(m); for (unsigned st : states) { literal acc = mk_accept(s, zero, re, st); lits.push_back(acc); - exprs.push_back(ctx.bool_var2expr(acc.var())); } if (lits.size() == 2) { propagate_lit(nullptr, 1, &lit, lits[1]); @@ -5019,13 +4851,11 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) { else { TRACE("seq", ctx.display_literals_verbose(tout, lits) << "\n";); - std::function fn = [&]() { return m.mk_implies(n, m.mk_or(exprs.size(), exprs.c_ptr())); }; - scoped_trace_stream _sts(*this, fn); + scoped_trace_stream _sts(*this, lits); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); } } - expr_ref theory_seq::mk_sub(expr* a, expr* b) { expr_ref result(m_autil.mk_sub(a, b), m); m_rewrite(result); @@ -5280,8 +5110,7 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter m_new_propagation = true; ++m_stats.m_add_axiom; - std::function fn = [&]() { return lits; }; - scoped_trace_stream _sts(*this, fn); + scoped_trace_stream _sts(*this, lits); validate_axiom(lits); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); } @@ -5317,10 +5146,7 @@ bool theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp literal_vector lits(_lits); enode_pair_vector eqs; - if (!linearize(deps, eqs, lits)) { - IF_VERBOSE(10, verbose_stream() << "not linearized " << mk_bounded_pp(e1, m, 2) << " " << mk_bounded_pp(e2, m, 2) << "\n"); - return false; - } + linearize(deps, eqs, lits); if (add_to_eqs) { deps = mk_join(deps, _lits); new_eq_eh(deps, n1, n2); @@ -5357,7 +5183,6 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { literal lit(v, !is_true); TRACE("seq", tout << (is_true?"":"not ") << mk_bounded_pp(e, m) << "\n";); - if (m_util.str.is_prefix(e, e1, e2)) { if (is_true) { f = m_sk.mk_prefix_inv(e1, e2); @@ -5492,9 +5317,7 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) { case l_true: break; case l_false: - if (!linearize(deps, eqs, lits)) { - throw default_exception("could not linearlize assumptions"); - } + linearize(deps, eqs, lits); eqs.push_back(enode_pair(n1, n2)); set_conflict(eqs, lits); break; @@ -5603,6 +5426,12 @@ void theory_seq::relevant_eh(app* n) { add_int_string(n); } + expr* s; + unsigned idx; + if (m_sk.is_tail(n, s, idx)) { + add_length_limit(s, m_max_unfolding_depth, true); + } + expr* arg; if (m_util.str.is_length(n, arg) && !has_length(arg) && get_context().e_internalized(arg)) { add_length_to_eqc(arg); @@ -5703,7 +5532,6 @@ void theory_seq::propagate_accept(literal lit, expr* acc) { return; } - expr_ref len = mk_len(e); literal_vector lits; lits.push_back(~lit); @@ -5715,27 +5543,26 @@ void theory_seq::propagate_accept(literal lit, expr* acc) { propagate_lit(nullptr, 1, &lit, ~mk_literal(m_autil.mk_le(len, idx))); } - eautomaton::moves mvs; aut->get_moves_from(src, mvs); TRACE("seq", tout << mk_pp(acc, m) << " #moves " << mvs.size() << "\n";); - expr_ref_vector exprs(m); for (auto const& mv : mvs) { expr_ref nth = mk_nth(e, idx); expr_ref t = mv.t()->accept(nth); get_context().get_rewriter()(t); expr_ref step_e(m_sk.mk_step(e, idx, re, src, mv.dst(), t), m); - literal step = mk_literal(step_e); - lits.push_back(step); - exprs.push_back(step_e); + lits.push_back(mk_literal(step_e)); } { - std::function fn = [&]() { return m.mk_implies(acc, m.mk_or(exprs.size(), exprs.c_ptr())); }; - scoped_trace_stream _sts(*this, fn); + scoped_trace_stream _sts(*this, lits); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); } + // NB. use instead a length tracking assumption on e to limit unfolding. + // that is, use add_length_limit when the atomaton is instantiated. + // and track the assignment to the length literal (mk_le(len, idx)). + // if (_idx.get_unsigned() > m_max_unfolding_depth && m_max_unfolding_lit != null_literal && ctx.get_scope_level() > 0) { propagate_lit(nullptr, 1, &lit, ~m_max_unfolding_lit); @@ -5745,11 +5572,13 @@ void theory_seq::propagate_accept(literal lit, expr* acc) { void theory_seq::add_theory_assumptions(expr_ref_vector & assumptions) { if (m_has_seq) { TRACE("seq", tout << "add_theory_assumption\n";); - expr_ref dlimit(m); - dlimit = m_sk.mk_max_unfolding_depth(m_max_unfolding_depth); + expr_ref dlimit = m_sk.mk_max_unfolding_depth(m_max_unfolding_depth); m_trail_stack.push(value_trail(m_max_unfolding_lit)); m_max_unfolding_lit = mk_literal(dlimit); assumptions.push_back(dlimit); + for (auto const& kv : m_length_limit_map) { + assumptions.push_back(m_sk.mk_length_limit(kv.m_key, kv.m_value)); + } } } @@ -5758,12 +5587,34 @@ bool theory_seq::should_research(expr_ref_vector & unsat_core) { if (!m_has_seq) { return false; } + unsigned k_min = UINT_MAX, k = 0, n = 0; + expr* s_min = nullptr, *s = nullptr; + bool has_max_unfolding = false; for (auto & e : unsat_core) { if (m_sk.is_max_unfolding(e)) { - m_max_unfolding_depth = (3 * m_max_unfolding_depth) / 2 + 1; - IF_VERBOSE(1, verbose_stream() << "(smt.seq :increase-depth " << m_max_unfolding_depth << ")\n"); - return true; + has_max_unfolding = true; } + else if (m_sk.is_length_limit(e, k, s)) { + if (k < k_min) { + k_min = k; + s_min = s; + n = 0; + } + else if (k == k_min && get_context().get_random_value() % (++n) == 0) { + s_min = s; + } + } + } + if (k_min < UINT_MAX) { + m_max_unfolding_depth++; + IF_VERBOSE(1, verbose_stream() << "(smt.seq :increase-length " << k_min << ")\n"); + add_length_limit(s, 2*k_min, false); + return true; + } + else if (has_max_unfolding) { + m_max_unfolding_depth = (1 + 3*m_max_unfolding_depth)/2; + IF_VERBOSE(1, verbose_stream() << "(smt.seq :increase-depth " << m_max_unfolding_depth << ")\n"); + return true; } return false; } @@ -5787,17 +5638,7 @@ void theory_seq::propagate_not_prefix(expr* e) { return; } propagate_non_empty(~lit, e1); - literal e1_gt_e2 = mk_simplified_literal(m_autil.mk_ge(mk_sub(mk_len(e1), mk_len(e2)), m_autil.mk_int(1))); - sort* char_sort = nullptr; - VERIFY(m_util.is_seq(m.get_sort(e1), char_sort)); - expr_ref x = m_sk.mk(symbol("seq.prefix.x"), e1, e2); - expr_ref y = m_sk.mk(symbol("seq.prefix.y"), e1, e2); - expr_ref z = m_sk.mk(symbol("seq.prefix.z"), e1, e2); - expr_ref c = m_sk.mk(symbol("seq.prefix.c"), e1, e2, nullptr, nullptr, char_sort); - expr_ref d = m_sk.mk(symbol("seq.prefix.d"), e1, e2, nullptr, nullptr, char_sort); - add_axiom(lit, e1_gt_e2, mk_seq_eq(e1, mk_concat(x, m_util.str.mk_unit(c), y))); - add_axiom(lit, e1_gt_e2, mk_seq_eq(e2, mk_concat(x, m_util.str.mk_unit(d), z)), mk_seq_eq(e2, x)); - add_axiom(lit, e1_gt_e2, ~mk_eq(c, d, false)); + m_ax.add_prefix_axiom(e); } /* @@ -5819,17 +5660,8 @@ void theory_seq::propagate_not_suffix(expr* e) { return; } propagate_non_empty(~lit, e1); - literal e1_gt_e2 = mk_simplified_literal(m_autil.mk_ge(mk_sub(mk_len(e1), mk_len(e2)), m_autil.mk_int(1))); - sort* char_sort = nullptr; - VERIFY(m_util.is_seq(m.get_sort(e1), char_sort)); - expr_ref x = m_sk.mk(symbol("seq.suffix.x"), e1, e2); - expr_ref y = m_sk.mk(symbol("seq.suffix.y"), e1, e2); - expr_ref z = m_sk.mk(symbol("seq.suffix.z"), e1, e2); - expr_ref c = m_sk.mk(symbol("seq.suffix.c"), e1, e2, nullptr, nullptr, char_sort); - expr_ref d = m_sk.mk(symbol("seq.suffix.d"), e1, e2, nullptr, nullptr, char_sort); - add_axiom(lit, e1_gt_e2, mk_seq_eq(e1, mk_concat(y, m_util.str.mk_unit(c), x))); - add_axiom(lit, e1_gt_e2, mk_seq_eq(e2, mk_concat(z, m_util.str.mk_unit(d), x))); - add_axiom(lit, e1_gt_e2, ~mk_eq(c, d, false)); + m_ax.add_suffix_axiom(e); + } bool theory_seq::canonizes(bool is_true, expr* e) { diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 2eeb1f752..81d78bd5f 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -390,9 +390,11 @@ namespace smt { unsigned m_axioms_head; // index of first axiom to add. bool m_incomplete; // is the solver (clearly) incomplete for the fragment. expr_ref_vector m_int_string; - obj_map m_si_axioms; - obj_hashtable m_has_length; // is length applied + obj_map m_si_axioms; + obj_hashtable m_has_length; // is length applied expr_ref_vector m_length; // length applications themselves + obj_map m_length_limit_map; // sequences that have length limit predicates + expr_ref_vector m_length_limit; // length limit predicates scoped_ptr_vector m_replay; // set of actions to replay model_generator* m_mg; th_rewriter m_rewrite; // rewriter that converts strings to character concats @@ -556,7 +558,7 @@ namespace smt { bool explain_empty(expr_ref_vector& es, dependency*& dep); // asserting consequences - bool linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const; + void linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const; void propagate_lit(dependency* dep, literal lit) { propagate_lit(dep, 0, nullptr, lit); } void propagate_lit(dependency* dep, unsigned n, literal const* lits, literal lit); bool propagate_eq(dependency* dep, enode* n1, enode* n2); @@ -611,6 +613,8 @@ namespace smt { bool enforce_length(expr_ref_vector const& es, vector& len); void enforce_length_coherence(enode* n1, enode* n2); + void add_length_limit(expr* s, unsigned k, bool is_searching); + // model-check the functions that convert integers to strings and the other way. void add_int_string(expr* e); bool check_int_string(); @@ -620,9 +624,7 @@ namespace smt { void add_in_re_axiom(expr* n); bool add_itos_val_axiom(expr* n); bool add_stoi_val_axiom(expr* n); - void add_si_axiom(expr* s, expr* i, unsigned sz); - void ensure_digit_axiom(); - literal is_digit(expr* ch); + bool add_si_axiom(expr* e, expr* n); void add_itos_length_axiom(expr* n); literal mk_literal(expr* n); literal mk_simplified_literal(expr* n); diff --git a/src/util/trail.h b/src/util/trail.h index ada4d263f..6f0bf6fb6 100644 --- a/src/util/trail.h +++ b/src/util/trail.h @@ -138,6 +138,17 @@ public: void undo(Ctx & ctx) override { m_map.remove(m_obj); } }; +template +class remove_obj_map : public trail { + obj_map& m_map; + D* m_obj; + R m_value; +public: + remove_obj_map(obj_map& t, D* o, R v) : m_map(t), m_obj(o), m_value(v) {} + ~remove_obj_map() override {} + void undo(Ctx & ctx) override { m_map.insert(m_obj, m_value); } +}; + template class insert_map : public trail { M& m_map;