mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

fix #2314

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-06-01 20:34:48 -07:00
parent 14923bad52
commit cccd37101e
3 changed files with 25 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/seq_decl_plugin.h
View file

@ -255,6 +255,7 @@ public:
expr* mk_concat(unsigned n, expr* const* es) const { if (n == 1) return es[0]; SASSERT(n > 1); return m.mk_app(m_fid, OP_SEQ_CONCAT, n, es); }
expr* mk_concat(expr_ref_vector const& es) const { return mk_concat(es.size(), es.c_ptr()); }
app* mk_length(expr* a) const { return m.mk_app(m_fid, OP_SEQ_LENGTH, 1, &a); }
app* mk_at(expr* s, expr* i) const { expr* es[2] = { s, i }; return m.mk_app(m_fid, OP_SEQ_AT, 2, es); }
app* mk_nth(expr* s, expr* i) const { expr* es[2] = { s, i }; return m.mk_app(m_fid, OP_SEQ_NTH, 2, es); }
app* mk_nth(expr* s, unsigned i) const;

30
src/smt/theory_seq.cpp
View file

@ -272,6 +272,7 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params):
m_find(*this),
m_overlap(m),
m_overlap2(m),
m_internal_nth_es(m),
m_len_prop_lvl(-1),
m_factory(nullptr),
m_exclude(m),
@ -298,7 +299,6 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params):
m_suffix = "seq.s.prefix";
m_accept = "aut.accept";
m_tail = "seq.tail";
m_nth = "seq.nth";
m_seq_first = "seq.first";
m_seq_last = "seq.last";
m_indexof_left = "seq.idx.left";
@ -1985,18 +1985,10 @@ bool theory_seq::is_unit_nth(expr* e) const {
bool theory_seq::is_nth(expr* e) const {
return m_util.str.is_nth(e);
// return is_skolem(m_nth, e);
}
bool theory_seq::is_nth(expr* e, expr*& e1, expr*& e2) const {
if (is_nth(e)) {
e1 = to_app(e)->get_arg(0);
e2 = to_app(e)->get_arg(1);
return true;
}
else {
return false;
}
return m_util.str.is_nth(e, e1, e2);
}
bool theory_seq::is_tail(expr* e, expr*& s, unsigned& idx) const {
@ -2023,7 +2015,12 @@ bool theory_seq::is_post(expr* e, expr*& s, expr*& i) {
expr_ref theory_seq::mk_nth(expr* s, expr* idx) {
return expr_ref(m_util.str.mk_nth(s, idx), m);
expr_ref result(m_util.str.mk_nth(s, idx), m);
if (!m_internal_nth_table.contains(result)) {
m_internal_nth_table.insert(result);
m_internal_nth_es.push_back(result);
}
return result;
}
expr_ref theory_seq::mk_sk_ite(expr* c, expr* t, expr* e) {
@ -5132,6 +5129,10 @@ void theory_seq::add_nth_axiom(expr* e) {
app_ref ch(m_util.str.mk_char(str[n.get_unsigned()]), m);
add_axiom(mk_eq(ch, e, false));
}
else if (!m_internal_nth_table.contains(e)) {
expr_ref emp(m_util.str.mk_empty(m.get_sort(s)), m);
add_axiom(mk_eq(s, emp, false), mk_eq(m_util.str.mk_unit(e), m_util.str.mk_at(s, i), false));
}
}
@ -5597,6 +5598,7 @@ void theory_seq::push_scope_eh() {
m_eqs.push_scope();
m_nqs.push_scope();
m_ncs.push_scope();
m_internal_nth_lim.push_back(m_internal_nth_es.size());
}
void theory_seq::pop_scope_eh(unsigned num_scopes) {
@ -5617,6 +5619,12 @@ void theory_seq::pop_scope_eh(unsigned num_scopes) {
m_len_prop_lvl = ctx.get_scope_level();
m_len_offset.reset();
}
unsigned old_sz = m_internal_nth_lim[m_internal_nth_lim.size() - num_scopes];
for (unsigned i = m_internal_nth_es.size(); i-- > old_sz; ) {
m_internal_nth_table.erase(m_internal_nth_es.get(i));
}
m_internal_nth_es.shrink(old_sz);
m_internal_nth_lim.shrink(m_internal_nth_lim.size() - num_scopes);
}
void theory_seq::restart_eh() {

7
src/smt/theory_seq.h
View file

@ -336,13 +336,16 @@ namespace smt {
obj_map<enode, obj_map<enode, int>> m_len_offset;
int m_len_prop_lvl;
obj_hashtable<expr> m_internal_nth_table;
expr_ref_vector m_internal_nth_es;
unsigned_vector m_internal_nth_lim;
seq_factory* m_factory; // value factory
exclusion_table m_exclude; // set of asserted disequalities.
expr_ref_vector m_axioms; // list of axioms to add.
obj_hashtable<expr> m_axiom_set;
unsigned m_axioms_head; // index of first axiom to add.
bool m_incomplete; // is the solver (clearly) incomplete for the fragment.
bool m_incomplete; // is the solver (clearly) incomplete for the fragment.
expr_ref_vector m_int_string;
obj_map<expr, rational> m_si_axioms;
obj_hashtable<expr> m_has_length; // is length applied
@ -357,7 +360,7 @@ namespace smt {
th_trail_stack m_trail_stack;
stats m_stats;
symbol m_prefix, m_suffix, m_accept, m_reject;
symbol m_tail, m_nth, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step;
symbol m_tail, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step;
symbol m_pre, m_post, m_eq, m_seq_align;
ptr_vector<expr> m_todo;
expr_ref_vector m_ls, m_rs, m_lhs, m_rhs;