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

fixing #2448 and #2445 and #2443

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-08-02 19:31:02 +08:00
parent c4480337c4
commit 584eee2cf4
6 changed files with 43 additions and 57 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -478,11 +478,12 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
SASSERT(num_args == 2);
st = mk_seq_at(args[0], args[1], result);
break;
#if 1
case OP_SEQ_NTH:
SASSERT(num_args == 2);
return mk_seq_nth(args[0], args[1], result);
#endif
case OP_SEQ_NTH_I:
SASSERT(num_args == 2);
return mk_seq_nth_i(args[0], args[1], result);
case OP_SEQ_PREFIX:
SASSERT(num_args == 2);
st = mk_seq_prefix(args[0], args[1], result);
@ -991,6 +992,16 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
}
br_status seq_rewriter::mk_seq_nth(expr* a, expr* b, expr_ref& result) {
expr* es[2] = { a, b};
expr* la = m_util.str.mk_length(a);
result = m().mk_ite(m().mk_and(m_autil.mk_le(m_autil.mk_int(0), b), m_autil.mk_lt(b, la)),
m().mk_app(m_util.get_family_id(), OP_SEQ_NTH_I, 2, es),
m().mk_app(m_util.get_family_id(), OP_SEQ_NTH_U, 2, es));
return BR_REWRITE_FULL;
}
br_status seq_rewriter::mk_seq_nth_i(expr* a, expr* b, expr_ref& result) {
zstring c;
rational r;
if (!m_autil.is_numeral(b, r) || !r.is_unsigned()) {

1
src/ast/rewriter/seq_rewriter.h
View file

@ -115,6 +115,7 @@ class seq_rewriter {
br_status mk_seq_contains(expr* a, expr* b, expr_ref& result);
br_status mk_seq_at(expr* a, expr* b, expr_ref& result);
br_status mk_seq_nth(expr* a, expr* b, expr_ref& result);
br_status mk_seq_nth_i(expr* a, expr* b, expr_ref& result);
br_status mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result);
br_status mk_seq_last_index(expr* a, expr* b, expr_ref& result);
br_status mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& result);

12
src/ast/seq_decl_plugin.cpp
View file

@ -559,6 +559,8 @@ void seq_decl_plugin::init() {
m_sigs[OP_SEQ_LAST_INDEX] = alloc(psig, m, "seq.last_indexof", 1, 2, seqAseqA, intT);
m_sigs[OP_SEQ_AT] = alloc(psig, m, "seq.at", 1, 2, seqAintT, seqA);
m_sigs[OP_SEQ_NTH] = alloc(psig, m, "seq.nth", 1, 2, seqAintT, A);
m_sigs[OP_SEQ_NTH_I] = alloc(psig, m, "seq.nth_i", 1, 2, seqAintT, A);
m_sigs[OP_SEQ_NTH_U] = alloc(psig, m, "seq.nth_u", 1, 2, seqAintT, A);
m_sigs[OP_SEQ_LENGTH] = alloc(psig, m, "seq.len", 1, 1, &seqA, intT);
m_sigs[OP_RE_PLUS] = alloc(psig, m, "re.+", 1, 1, &reA, reA);
m_sigs[OP_RE_STAR] = alloc(psig, m, "re.*", 1, 1, &reA, reA);
@ -852,6 +854,8 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
return mk_str_fun(k, arity, domain, range, OP_SEQ_AT);
case OP_SEQ_NTH:
case OP_SEQ_NTH_I:
case OP_SEQ_NTH_U:
match(*m_sigs[k], arity, domain, range, rng);
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
@ -1035,14 +1039,14 @@ bool seq_util::str::is_string(expr const* n, zstring& s) const {
}
}
bool seq_util::str::is_nth(expr const* n, expr*& s, unsigned& idx) const {
bool seq_util::str::is_nth_i(expr const* n, expr*& s, unsigned& idx) const {
expr* i = nullptr;
if (!is_nth(n, s, i)) return false;
if (!is_nth_i(n, s, i)) return false;
return arith_util(m).is_unsigned(i, idx);
}
app* seq_util::str::mk_nth(expr* s, unsigned i) const {
return mk_nth(s, arith_util(m).mk_int(i));
app* seq_util::str::mk_nth_i(expr* s, unsigned i) const {
return mk_nth_i(s, arith_util(m).mk_int(i));
}
void seq_util::str::get_concat(expr* e, expr_ref_vector& es) const {

17
src/ast/seq_decl_plugin.h
View file

@ -41,6 +41,8 @@ enum seq_op_kind {
OP_SEQ_REPLACE,
OP_SEQ_AT,
OP_SEQ_NTH,
OP_SEQ_NTH_I,
OP_SEQ_NTH_U,
OP_SEQ_LENGTH,
OP_SEQ_INDEX,
OP_SEQ_LAST_INDEX,
@ -259,8 +261,8 @@ public:
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;
app* mk_nth_i(expr* s, expr* i) const { expr* es[2] = { s, i }; return m.mk_app(m_fid, OP_SEQ_NTH_I, 2, es); }
app* mk_nth_i(expr* s, unsigned i) const;
app* mk_substr(expr* a, expr* b, expr* c) const { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_SEQ_EXTRACT, 3, es); }
app* mk_contains(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONTAINS, 2, es); }
@ -277,7 +279,8 @@ public:
app* mk_lex_le(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_LE, 2, es); }
bool is_nth(func_decl* f) const { return is_decl_of(f, m_fid, OP_SEQ_NTH); }
bool is_nth_i(func_decl* f) const { return is_decl_of(f, m_fid, OP_SEQ_NTH_I); }
bool is_nth_u(func_decl* f) const { return is_decl_of(f, m_fid, OP_SEQ_NTH_U); }
bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); }
bool is_string(expr const* n, symbol& s) const {
@ -292,8 +295,9 @@ public:
bool is_extract(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_EXTRACT); }
bool is_contains(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_CONTAINS); }
bool is_at(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_AT); }
bool is_nth(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_NTH); }
bool is_nth(expr const* n, expr*& s, unsigned& idx) const;
bool is_nth_i(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_NTH_I); }
bool is_nth_u(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_NTH_U); }
bool is_nth_i(expr const* n, expr*& s, unsigned& idx) const;
bool is_index(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_INDEX); }
bool is_last_index(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_LAST_INDEX); }
bool is_replace(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_REPLACE); }
@ -321,7 +325,8 @@ public:
MATCH_TERNARY(is_extract);
MATCH_BINARY(is_contains);
MATCH_BINARY(is_at);
MATCH_BINARY(is_nth);
MATCH_BINARY(is_nth_i);
MATCH_BINARY(is_nth_u);
MATCH_BINARY(is_index);
MATCH_TERNARY(is_index);
MATCH_BINARY(is_last_index);

47
src/smt/theory_seq.cpp
View file

@ -274,7 +274,6 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params):
m_overlap(m),
m_overlap2(m),
m_len_prop_lvl(-1),
m_internal_nth_es(m),
m_factory(nullptr),
m_exclude(m),
m_axioms(m),
@ -1985,16 +1984,9 @@ bool theory_seq::propagate_is_conc(expr* e, expr* conc) {
bool theory_seq::is_unit_nth(expr* e) const {
expr *s = nullptr;
return m_util.str.is_unit(e, s) && is_nth(s);
return m_util.str.is_unit(e, s) && m_util.str.is_nth_i(s);
}
bool theory_seq::is_nth(expr* e) const {
return m_util.str.is_nth(e);
}
bool theory_seq::is_nth(expr* e, expr*& e1, expr*& e2) const {
return m_util.str.is_nth(e, e1, e2);
}
bool theory_seq::is_tail(expr* e, expr*& s, unsigned& idx) const {
rational r;
@ -2017,14 +2009,8 @@ bool theory_seq::is_post(expr* e, expr*& s, expr*& i) {
return is_skolem(m_post, e) && (s = to_app(e)->get_arg(0), i = to_app(e)->get_arg(1), true);
}
expr_ref theory_seq::mk_nth(expr* s, expr* idx) {
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);
}
expr_ref result(m_util.str.mk_nth_i(s, idx), m);
return result;
}
@ -2445,7 +2431,7 @@ bool theory_seq::solve_nth_eq(expr_ref_vector const& ls, expr_ref_vector const&
for (unsigned i = 0; i < rs.size(); ++i) {
unsigned k = 0;
expr* ru = nullptr, *r = nullptr;
if (m_util.str.is_unit(rs.get(i), ru) && m_util.str.is_nth(ru, r, k) && k == i && r == l) {
if (m_util.str.is_unit(rs.get(i), ru) && m_util.str.is_nth_i(ru, r, k) && k == i && r == l) {
continue;
}
return false;
@ -2461,10 +2447,6 @@ bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const&
if (r.size() == 1 && is_var(r[0]) && !occurs(r[0], l) && add_solution(r[0], mk_concat(l, m.get_sort(r[0])), deps)) {
return true;
}
// if (l.size() == 1 && r.size() == 1 && l[0] != r[0] && is_nth(l[0]) && add_solution(l[0], r[0], deps))
// return true;
// if (l.size() == 1 && r.size() == 1 && l[0] != r[0] && is_nth(r[0]) && add_solution(r[0], l[0], deps))
// return true;
return false;
}
@ -2493,10 +2475,6 @@ bool theory_seq::solve_unit_eq(expr* l, expr* r, dependency* deps) {
if (is_var(r) && !occurs(r, l) && add_solution(r, l, deps)) {
return true;
}
// if (is_nth(l) && !occurs(l, r) && add_solution(l, r, deps))
// return true;
// if (is_nth(r) && !occurs(r, l) && add_solution(r, l, deps))
// return true;
return false;
}
@ -2529,7 +2507,7 @@ bool theory_seq::occurs(expr* a, expr* b) {
else if (m_util.str.is_unit(b, e1)) {
m_todo.push_back(e1);
}
else if (m_util.str.is_nth(b, e1, e2)) {
else if (m_util.str.is_nth_i(b, e1, e2)) {
m_todo.push_back(e1);
}
}
@ -4440,7 +4418,7 @@ void theory_seq::deque_axiom(expr* n) {
else if (m_util.str.is_at(n)) {
add_at_axiom(n);
}
else if (m_util.str.is_nth(n)) {
else if (m_util.str.is_nth_i(n)) {
add_nth_axiom(n);
}
else if (m_util.str.is_string(n)) {
@ -5207,12 +5185,12 @@ void theory_seq::add_nth_axiom(expr* e) {
expr* s = nullptr, *i = nullptr;
rational n;
zstring str;
VERIFY(m_util.str.is_nth(e, s, i));
VERIFY(m_util.str.is_nth_i(e, s, i));
if (m_util.str.is_string(s, str) && m_autil.is_numeral(i, n) && n.is_unsigned() && n.get_unsigned() < str.length()) {
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)) {
else {
expr_ref zero(m_autil.mk_int(0), m);
literal i_ge_0 = mk_simplified_literal(m_autil.mk_ge(i, zero));
literal i_ge_len_s = mk_simplified_literal(m_autil.mk_ge(mk_sub(i, mk_len(s)), zero));
@ -5563,7 +5541,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
else if (m_util.str.is_lt(e) || m_util.str.is_le(e)) {
m_lts.push_back(e);
}
else if (is_nth(e)) {
else if (m_util.str.is_nth_i(e)) {
// no-op
}
else {
@ -5693,7 +5671,6 @@ void theory_seq::push_scope_eh() {
m_nqs.push_scope();
m_ncs.push_scope();
m_lts.push_scope();
m_internal_nth_lim.push_back(m_internal_nth_es.size());
}
void theory_seq::pop_scope_eh(unsigned num_scopes) {
@ -5715,12 +5692,6 @@ 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() {
@ -5731,7 +5702,7 @@ void theory_seq::relevant_eh(app* n) {
m_util.str.is_replace(n) ||
m_util.str.is_extract(n) ||
m_util.str.is_at(n) ||
m_util.str.is_nth(n) ||
m_util.str.is_nth_i(n) ||
m_util.str.is_empty(n) ||
m_util.str.is_string(n) ||
m_util.str.is_itos(n) ||

8
src/smt/theory_seq.h
View file

@ -338,10 +338,6 @@ 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.
@ -399,7 +395,7 @@ namespace smt {
void add_theory_assumptions(expr_ref_vector & assumptions) override;
theory* mk_fresh(context* new_ctx) override { return alloc(theory_seq, new_ctx->get_manager(), m_params); }
char const * get_name() const override { return "seq"; }
bool include_func_interp(func_decl* f) override { return false; } // m_util.str.is_nth(f); }
bool include_func_interp(func_decl* f) override { return m_util.str.is_nth_u(f); }
theory_var mk_var(enode* n) override;
void apply_sort_cnstr(enode* n, sort* s) override;
void display(std::ostream & out) const override;
@ -532,8 +528,6 @@ namespace smt {
bool is_var(expr* b) const;
bool add_solution(expr* l, expr* r, dependency* dep);
bool is_unit_nth(expr* a) const;
bool is_nth(expr* a) const;
bool is_nth(expr* a, expr*& e1, expr*& e2) const;
bool is_tail(expr* a, expr*& s, unsigned& idx) const;
bool is_eq(expr* e, expr*& a, expr*& b) const;
bool is_pre(expr* e, expr*& s, expr*& i);