From 60711bb0cd4365de375524a4cd7239304dfdded0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Jul 2016 12:18:07 -0700 Subject: [PATCH] deal with model construction, issue #684. fix model construction for ite #678. WIth this version, issue #686 does not repro Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 4 +++- src/smt/theory_seq.cpp | 38 +++++++++++++++++++++++++++------ src/smt/theory_seq.h | 1 + src/smt/theory_seq_empty.h | 16 ++++++++++++++ 4 files changed, 51 insertions(+), 8 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 5f9de116d..2811153c0 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1634,6 +1634,7 @@ void cmd_context::validate_model() { scoped_ctrl_c ctrlc(eh); ptr_vector::const_iterator it = begin_assertions(); ptr_vector::const_iterator end = end_assertions(); + bool invalid_model = false; for (; it != end; ++it) { expr * a = *it; if (is_ground(a)) { @@ -1654,9 +1655,10 @@ void cmd_context::validate_model() { continue; } TRACE("model_validate", model_smt2_pp(tout, *this, *(md.get()), 0);); - throw cmd_exception("an invalid model was generated"); + invalid_model = true; } } + throw cmd_exception("an invalid model was generated"); } } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 0702bac69..8b6c5baba 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -196,6 +196,7 @@ theory_seq::theory_seq(ast_manager& m): theory(m.mk_family_id("seq")), m(m), m_rep(m, m_dm), + m_reset_cache(false), m_eq_id(0), m_find(*this), m_factory(0), @@ -242,6 +243,10 @@ void theory_seq::init(context* ctx) { } final_check_status theory_seq::final_check_eh() { + if (m_reset_cache) { + m_rep.reset_cache(); + m_reset_cache = false; + } m_new_propagation = false; TRACE("seq", display(tout << "level: " << get_context().get_scope_level() << "\n");); if (simplify_and_solve_eqs()) { @@ -1366,7 +1371,7 @@ bool theory_seq::solve_unit_eq(expr* l, expr* r, dependency* deps) { bool theory_seq::occurs(expr* a, expr_ref_vector const& b) { for (unsigned i = 0; i < b.size(); ++i) { - if (a == b[i]) return true; + if (a == b[i] || m.is_ite(b[i])) return true; } return false; } @@ -1379,7 +1384,7 @@ bool theory_seq::occurs(expr* a, expr* b) { m_todo.push_back(b); while (!m_todo.empty()) { b = m_todo.back(); - if (a == b) { + if (a == b || m.is_ite(b)) { m_todo.reset(); return true; } @@ -2421,6 +2426,11 @@ void theory_seq::init_model(expr_ref_vector const& es) { void theory_seq::init_model(model_generator & mg) { m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model()); mg.register_factory(m_factory); + for (unsigned j = 0; j < m_nqs.size(); ++j) { + ne const& n = m_nqs[j]; + m_factory->register_value(n.l()); + m_factory->register_value(n.r()); + } for (unsigned j = 0; j < m_nqs.size(); ++j) { ne const& n = m_nqs[j]; for (unsigned i = 0; i < n.ls().size(); ++i) { @@ -2452,6 +2462,13 @@ public: virtual void get_dependencies(buffer & result) { result.append(m_dependencies.size(), m_dependencies.c_ptr()); } + + void add_buffer(svector& sbuffer, zstring const& zs) { + for (unsigned l = 0; l < zs.length(); ++l) { + sbuffer.push_back(zs[l]); + } + } + virtual app * mk_value(model_generator & mg, ptr_vector & values) { SASSERT(values.size() == m_dependencies.size()); expr_ref_vector args(th.m); @@ -2470,12 +2487,16 @@ public: sbuffer.push_back(val.get_unsigned()); } else { + dependency* deps = 0; + expr_ref tmp = th.canonize(m_strings[k], deps); zstring zs; - if (th.m_util.str.is_string(m_strings[k++], zs)) { - for (unsigned l = 0; l < zs.length(); ++l) { - sbuffer.push_back(zs[l]); - } + if (th.m_util.str.is_string(tmp, zs)) { + add_buffer(sbuffer, zs); } + else { + TRACE("seq", tout << "Not a string: " << tmp << "\n";); + } + ++k; } } result = th.m_util.str.mk_string(zstring(sbuffer.size(), sbuffer.c_ptr())); @@ -2657,7 +2678,10 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) { result = expand(e3, deps); break; case l_undef: - result = e; + result = e; + m_reset_cache = true; + TRACE("seq", tout << "undef: " << result << "\n"; + tout << lit << "@ level: " << ctx.get_scope_level() << "\n";); break; } } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index c1e179f67..187573623 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -294,6 +294,7 @@ namespace smt { ast_manager& m; dependency_manager m_dm; solution_map m_rep; // unification representative. + bool m_reset_cache; // invalidate cache. scoped_vector m_eqs; // set of current equations. scoped_vector m_nqs; // set of current disequalities. scoped_vector m_ncs; // set of non-contains constraints. diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h index 27c72cc97..3f6c7f3e2 100644 --- a/src/smt/theory_seq_empty.h +++ b/src/smt/theory_seq_empty.h @@ -126,6 +126,22 @@ namespace smt { symbol sym; if (u.str.is_string(n, sym)) { m_strings.insert(sym); + if (sym.str().find(m_unique_delim) != std::string::npos) { + add_new_delim(); + } + } + } + private: + + void add_new_delim() { + bool found = true; + while (found) { + found = false; + m_unique_delim += "!"; + symbol_set::iterator it = m_strings.begin(), end = m_strings.end(); + for (; it != end && !found; ++it) { + found = it->str().find(m_unique_delim) != std::string::npos; + } } } };