mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-01 11:51:20 +00:00
Code Activity

fix #4982

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-01-29 06:43:33 -08:00
parent 5c9b205dfc
commit b402268d35
3 changed files with 21 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/rewriter/seq_rewriter.cpp
View file

@ -1383,6 +1383,12 @@ br_status seq_rewriter::mk_seq_nth_i(expr* a, expr* b, expr_ref& result) {
} }
unsigned len = r.get_unsigned(); unsigned len = r.get_unsigned();
expr* a2, *i2;
if (len == 0 && str().is_at(a, a2, i2) && m_autil.is_numeral(i2, r) && r.is_zero()) {
result = str().mk_nth_i(a2, i2);
return BR_REWRITE1;
}
expr_ref_vector as(m()); expr_ref_vector as(m());
str().get_concat_units(a, as); str().get_concat_units(a, as);

14
src/smt/seq_eq_solver.cpp
View file

@ -1577,6 +1577,16 @@ bool theory_seq::is_ternary_eq_lhs(expr_ref_vector const& ls, expr_ref_vector co
return false; return false;
} }
struct remove_obj_pair_map : public trail<context> {
obj_pair_hashtable<expr, expr> & m_map;
expr* a, *b;
remove_obj_pair_map(obj_pair_hashtable<expr, expr> & map, expr* a, expr* b):
m_map(map), a(a), b(b) {}
void undo(context& ctx) override {
m_map.erase(std::make_pair(a, b));
}
};
/** /**
nth(x,idx) = rhs => nth(x,idx) = rhs =>
x = pre(x, idx) ++ unit(rhs) ++ post(x, idx + 1) x = pre(x, idx) ++ unit(rhs) ++ post(x, idx + 1)
@ -1591,6 +1601,10 @@ bool theory_seq::solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const&
expr_ref idx1(m_autil.mk_add(idx, m_autil.mk_int(1)), m); expr_ref idx1(m_autil.mk_add(idx, m_autil.mk_int(1)), m);
m_rewrite(idx1); m_rewrite(idx1);
expr_ref rhs = mk_concat(rs.size(), rs.c_ptr(), m.get_sort(ls[0])); expr_ref rhs = mk_concat(rs.size(), rs.c_ptr(), m.get_sort(ls[0]));
if (m_nth_eq2_cache.contains(std::make_pair(rhs, ls[0])))
return false;
m_nth_eq2_cache.insert(std::make_pair(rhs, ls[0]));
ctx.push_trail(remove_obj_pair_map(m_nth_eq2_cache, rhs, ls[0]));
ls1.push_back(s); ls1.push_back(s);
if (!idx_is_zero) rs1.push_back(m_sk.mk_pre(s, idx)); if (!idx_is_zero) rs1.push_back(m_sk.mk_pre(s, idx));
rs1.push_back(m_util.str.mk_unit(rhs)); rs1.push_back(m_util.str.mk_unit(rhs));

1
src/smt/theory_seq.h
View file

@ -459,6 +459,7 @@ namespace smt {
bool solve_unit_eq(expr* l, expr* r, dependency* dep); bool solve_unit_eq(expr* l, expr* r, dependency* dep);
bool solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep); bool solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
bool solve_nth_eq1(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep); bool solve_nth_eq1(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
obj_pair_hashtable<expr, expr> m_nth_eq2_cache;
bool solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep); bool solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
bool solve_itos(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep); bool solve_itos(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
bool solve_itos(expr* n, expr_ref_vector const& rs, dependency* dep); bool solve_itos(expr* n, expr_ref_vector const& rs, dependency* dep);