From 38f74297a93b546a9ab2e807b85ac2b6e3a81e40 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Dec 2019 15:30:06 -0800 Subject: [PATCH] seq Signed-off-by: Nikolaj Bjorner --- src/math/grobner/pdd_grobner.cpp | 3 ++- src/smt/theory_seq.cpp | 15 ++++++++++----- 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/src/math/grobner/pdd_grobner.cpp b/src/math/grobner/pdd_grobner.cpp index 3adc5555e..5327e2cd6 100644 --- a/src/math/grobner/pdd_grobner.cpp +++ b/src/math/grobner/pdd_grobner.cpp @@ -295,8 +295,9 @@ namespace dd { void grobner::add_to_watch(equation& eq) { SASSERT(!eq.is_processed()); + SASSERT(is_tuned()); pdd const& p = eq.poly(); - if (is_tuned() && !p.is_val()) { + if (!p.is_val()) { m_watch[p.var()].push_back(&eq); } } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 1b906c8f6..66c3fd9b1 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2540,13 +2540,18 @@ bool theory_seq::solve_itos(expr_ref_vector const& ls, expr_ref_vector const& rs } bool theory_seq::solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps) { - rational n; expr* s = nullptr, *idx = nullptr; - if (ls.size() == 1 && m_util.str.is_nth_i(ls[0], s, idx)) { - expr_ref lhs(m_util.str.mk_at(s, idx), m); + if (false && ls.size() == 1 && m_util.str.is_nth_i(ls[0], s, idx)) { + expr_ref idx1(m_autil.mk_add(m_autil.mk_int(1), idx), m); + m_rewrite(idx1); + expr_ref hd = mk_skolem(m_pre, s, idx); + expr_ref tl = mk_skolem(m_tail, s, idx1); expr_ref rhs(m_util.str.mk_concat(rs.size(), rs.c_ptr()), m); - expr_ref_vector ls1(m); ls1.push_back(lhs); - expr_ref_vector rs1(m); rs1.push_back(m_util.str.mk_unit(rhs)); + rhs = m_util.str.mk_unit(rhs); + expr_ref_vector rs1(m); rs1.push_back(hd); rs1.push_back(rhs); rs1.push_back(tl); + expr_ref_vector ls1(m); ls1.push_back(s); + std::cout << ls << "\n" << rs << "\n-> \n" << rs1 << "\n" << ls1 << "\n"; + m_eqs.push_back(eq(m_eq_id++, ls1, rs1, deps)); return true; }