mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 07:13:41 +00:00
Code Activity

seq, API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-04 22:06:32 -08:00
parent d7dcd022b9
commit 2c1d2aad44
3 changed files with 20 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1023,27 +1023,17 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
} }
else if (!change) { else if (!change) {
// skip // skip
SASSERT(lhs.empty());
} }
else { else {
// could solve if either side is fixed size. // could solve if either side is fixed size.
SASSERT(szl > 0 && szr > 0); SASSERT(szl > 0 && szr > 0);
if (head1 > 0) { lhs.push_back(m_util.str.mk_concat(szl, ls.c_ptr() + head1));
for (unsigned i = 0; i < szl; ++i) { rhs.push_back(m_util.str.mk_concat(szr, rs.c_ptr() + head2));
ls[i] = ls[i + head1];
}
}
ls.shrink(szl);
if (head2 > 0) {
for (unsigned i = 0; i < szr; ++i) {
rs[i] = rs[i + head2];
}
}
rs.shrink(szr);
lhs.push_back(m_util.str.mk_concat(ls.size(), ls.c_ptr()));
rhs.push_back(m_util.str.mk_concat(rs.size(), rs.c_ptr()));
ls.reset(); ls.reset();
rs.reset(); rs.reset();
} }
SASSERT(lhs.empty() || ls.empty());
return true; return true;
} }
@ -1054,16 +1044,9 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
m_util.str.get_concat(r, m_rhs); m_util.str.get_concat(r, m_rhs);
if (reduce_eq(m_lhs, m_rhs, lhs, rhs)) { if (reduce_eq(m_lhs, m_rhs, lhs, rhs)) {
SASSERT(lhs.size() == rhs.size()); SASSERT(lhs.size() == rhs.size());
if (!m_lhs.empty()) { if (lhs.empty()) {
SASSERT(!m_rhs.empty()); lhs.push_back(l);
lhs.push_back(m_util.str.mk_concat(m_lhs.size(), m_lhs.c_ptr())); rhs.push_back(r);
rhs.push_back(m_util.str.mk_concat(m_rhs.size(), m_rhs.c_ptr()));
}
for (unsigned i = 0; i < lhs.size(); ++i) {
SASSERT(is_well_sorted(m(), lhs[i].get()));
SASSERT(is_well_sorted(m(), rhs[i].get()));
SASSERT(m().get_sort(lhs[i].get()) == m().get_sort(rhs[i].get()));
TRACE("seq", tout << mk_pp(lhs[i].get(), m()) << " = " << mk_pp(rhs[i].get(), m()) << "\n";);
} }
return true; return true;
} }

16
src/smt/theory_seq.cpp
View file

@ -166,6 +166,8 @@ theory_seq::theory_seq(ast_manager& m):
m_autil(m), m_autil(m),
m_trail_stack(*this), m_trail_stack(*this),
m_atoms_qhead(0), m_atoms_qhead(0),
m_ls(m), m_rs(m),
m_lhs(m), m_rhs(m),
m_new_solution(false), m_new_solution(false),
m_new_propagation(false) { m_new_propagation(false) {
m_prefix = "seq.prefix.suffix"; m_prefix = "seq.prefix.suffix";
@ -874,17 +876,21 @@ void theory_seq::solve_ne(unsigned idx) {
} }
} }
for (unsigned i = 0; i < n.m_lhs.size(); ++i) { for (unsigned i = 0; i < n.m_lhs.size(); ++i) {
expr_ref_vector lhs(m), rhs(m); expr_ref_vector& ls = m_ls;
expr_ref_vector& rs = m_rs;
expr_ref_vector& lhs = m_lhs;
expr_ref_vector& rhs = m_rhs;
ls.reset(); rs.reset(); lhs.reset(); rhs.reset();
dependency* deps = 0; dependency* deps = 0;
expr* l = n.m_lhs[i]; expr* l = n.m_lhs[i];
expr* r = n.m_rhs[i]; expr* r = n.m_rhs[i];
expr_ref lh = canonize(l, deps); canonize(l, ls, deps);
expr_ref rh = canonize(r, deps); canonize(r, rs, deps);
if (!rw.reduce_eq(lh, rh, lhs, rhs)) { if (!rw.reduce_eq(ls, rs, lhs, rhs)) {
mark_solved(idx); mark_solved(idx);
return; return;
} }
else if (unchanged(l, lhs, r, rhs) ) { else if (lhs.empty() || (lhs.size() == 1 && lhs[0].get() == l)) {
// continue // continue
} }
else { else {

1
src/smt/theory_seq.h
View file

@ -318,6 +318,7 @@ namespace smt {
symbol m_tail, m_nth, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step; symbol m_tail, m_nth, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step;
symbol m_extract_prefix, m_at_left, m_at_right; symbol m_extract_prefix, m_at_left, m_at_right;
ptr_vector<expr> m_todo; ptr_vector<expr> m_todo;
expr_ref_vector m_ls, m_rs, m_lhs, m_rhs;
// maintain automata with regular expressions. // maintain automata with regular expressions.
scoped_ptr_vector<eautomaton> m_automata; scoped_ptr_vector<eautomaton> m_automata;