mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

seq

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-23 15:30:06 -08:00
parent beb4c0f27b
commit 38f74297a9
2 changed files with 12 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/grobner/pdd_grobner.cpp
View file

@ -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);
}
}

15
src/smt/theory_seq.cpp
View file

@ -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;
}