From 20a28af2255641293a7ea8e0974316fd88746c9a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 23 Nov 2018 21:42:48 -0800 Subject: [PATCH] fix stoi/itos axiom replay Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 80 +++++++++++++++++++++--------------------- src/smt/theory_seq.h | 16 +++++++-- 2 files changed, 54 insertions(+), 42 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 9b79786fd..fb6a95790 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3411,17 +3411,20 @@ void theory_seq::add_int_string(expr* e) { bool theory_seq::check_int_string() { bool change = false; for (expr * e : m_int_string) { - expr* n = nullptr; - if (m_util.str.is_itos(e) && add_itos_val_axiom(e)) { - change = true; - } - else if (m_util.str.is_stoi(e, n) && add_stoi_val_axiom(e)) { + if (check_int_string(e)) { change = true; } } return change; } +bool theory_seq::check_int_string(expr* e) { + return + (m_util.str.is_itos(e) && add_itos_val_axiom(e)) || + (m_util.str.is_stoi(e) && add_stoi_val_axiom(e)); +} + + void theory_seq::add_stoi_axiom(expr* e) { TRACE("seq", tout << mk_pp(e, m) << "\n";); expr* s = nullptr; @@ -3435,7 +3438,7 @@ void theory_seq::add_stoi_axiom(expr* e) { void theory_seq::ensure_digit_axiom() { - if (m_stoi_axioms.empty() && m_itos_axioms.empty()) { + if (m_si_axioms.empty()) { bv_util bv(m); for (unsigned i = 0; i < 10; ++i) { expr_ref cnst(bv.mk_numeral(rational('0'+i), bv.mk_sort(8)), m); @@ -3444,25 +3447,46 @@ void theory_seq::ensure_digit_axiom() { } } +bool theory_seq::add_itos_val_axiom(expr* e) { + context& ctx = get_context(); + rational val; + 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; + } + enforce_length(e); + + if (get_length(e, val) && val.is_pos() && val.is_unsigned() && !m_si_axioms.contains(e)) { + add_si_axiom(e, n, val.get_unsigned()); + m_si_axioms.insert(e); + 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; +} + bool theory_seq::add_stoi_val_axiom(expr* e) { context& ctx = get_context(); expr* n = nullptr; rational val; - TRACE("seq", tout << mk_pp(e, m) << "\n";); + TRACE("seq", tout << mk_pp(e, m) << " " << ctx.get_scope_level () << "\n";); VERIFY(m_util.str.is_stoi(e, n)); if (m_util.str.is_itos(n)) { return false; } - enforce_length(n); - if (get_length(n, val) && val.is_pos() && val.is_unsigned() && !m_stoi_axioms.contains(val)) { - ensure_digit_axiom(); + if (get_length(n, val) && val.is_pos() && val.is_unsigned() && !m_si_axioms.contains(e)) { add_si_axiom(n, e, val.get_unsigned()); - m_stoi_axioms.insert(val); - m_trail_stack.push(insert_map(m_stoi_axioms, val)); - m_trail_stack.push(push_replay(alloc(replay_axiom, m, e))); + m_si_axioms.insert(e); + 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; } @@ -3527,6 +3551,7 @@ void theory_seq::add_si_axiom(expr* e, expr* n, unsigned k) { 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); @@ -3565,31 +3590,6 @@ void theory_seq::add_si_axiom(expr* e, expr* n, unsigned k) { } -bool theory_seq::add_itos_val_axiom(expr* e) { - context& ctx = get_context(); - rational val; - expr* n = nullptr; - TRACE("seq", tout << mk_pp(e, m) << "\n";); - VERIFY(m_util.str.is_itos(e, n)); - bool change = false; - - if (m_util.str.is_stoi(n)) { - return false; - } - enforce_length(e); - - if (get_length(e, val) && val.is_pos() && !m_itos_axioms.contains(val) && val.is_unsigned()) { - add_si_axiom(e, n, val.get_unsigned()); - ensure_digit_axiom(); - m_itos_axioms.insert(val); - m_trail_stack.push(insert_map(m_itos_axioms, val)); - m_trail_stack.push(push_replay(alloc(replay_axiom, m, e))); - return true; - } - - - return false; -} void theory_seq::apply_sort_cnstr(enode* n, sort* s) { mk_var(n); @@ -4209,8 +4209,8 @@ void theory_seq::propagate() { ++m_axioms_head; } while (!m_replay.empty() && !ctx.inconsistent()) { - TRACE("seq", tout << "replay at level: " << ctx.get_scope_level() << "\n";); apply* app = m_replay[m_replay.size() - 1]; + TRACE("seq", tout << "replay at level: " << ctx.get_scope_level() << "\n";); (*app)(*this); m_replay.pop_back(); } @@ -4221,6 +4221,7 @@ void theory_seq::propagate() { } void theory_seq::enque_axiom(expr* e) { + TRACE("seq", tout << "enqueue_axiom " << mk_pp(e, m) << " " << m_axiom_set.contains(e) << "\n";); if (!m_axiom_set.contains(e)) { TRACE("seq", tout << "add axiom " << mk_pp(e, m) << "\n";); m_axioms.push_back(e); @@ -5596,7 +5597,6 @@ bool theory_seq::add_accept2step(expr* acc, bool& change) { ctx.mark_as_relevant(slit); // ctx.force_phase(slit); // return true; - // std::cout << mk_pp(step, m) << " is undef\n"; has_undef = true; break; default: diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 2c99d8fd1..2f1767ba7 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -259,6 +259,18 @@ namespace smt { } }; + + class replay_is_axiom : public apply { + expr_ref m_e; + public: + replay_is_axiom(ast_manager& m, expr* e) : m_e(e, m) {} + ~replay_is_axiom() override {} + void operator()(theory_seq& th) override { + th.check_int_string(m_e); + m_e.reset(); + } + }; + class push_replay : public trail { apply* m_apply; public: @@ -321,8 +333,7 @@ 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; - rational_set m_itos_axioms; - rational_set m_stoi_axioms; + obj_hashtable m_si_axioms; obj_hashtable m_length; // is length applied scoped_ptr_vector m_replay; // set of actions to replay model_generator* m_mg; @@ -544,6 +555,7 @@ namespace smt { // model-check the functions that convert integers to strings and the other way. void add_int_string(expr* e); bool check_int_string(); + bool check_int_string(expr* e); expr_ref add_elim_string_axiom(expr* n); void add_at_axiom(expr* n);