mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

fix regressions exposed by build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-12 11:18:52 -08:00
parent db746e0c2f
commit 22fbed18cc
2 changed files with 13 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/api/python/z3.py
View file

@ -9320,8 +9320,10 @@ def Union(*args):
args = _get_args(args) args = _get_args(args)
sz = len(args) sz = len(args)
if __debug__: if __debug__:
_z3_assert(sz >= 2, "At least two arguments expected.") _z3_assert(sz > 0, "At least one argument expected.")
_z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
if sz == 1:
return args[0]
ctx = args[0].ctx ctx = args[0].ctx
v = (Ast * sz)() v = (Ast * sz)()
for i in range(sz): for i in range(sz):

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

@ -40,10 +40,9 @@ re2automaton::re2automaton(ast_manager& m): m(m), u(m) {}
eautomaton* re2automaton::operator()(expr* e) { eautomaton* re2automaton::operator()(expr* e) {
eautomaton* r = re2aut(e); eautomaton* r = re2aut(e);
if (r) { if (r) {
//display_expr1 disp(m); display_expr1 disp(m);
//r->display(std::cout, disp);
r->compress(); r->compress();
//r->display(std::cout, disp); TRACE("seq", r->display(tout, disp););
} }
return r; return r;
} }
@ -664,6 +663,7 @@ void seq_rewriter::add_next(u_map<expr*>& next, unsigned idx, expr* cond) {
} }
bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) { bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) {
seq.reset();
unsigned state = aut.init(); unsigned state = aut.init();
uint_set visited; uint_set visited;
eautomaton::moves mvs; eautomaton::moves mvs;
@ -675,6 +675,9 @@ bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) {
if (visited.contains(state)) { if (visited.contains(state)) {
return false; return false;
} }
if (aut.is_final_state(mvs[0].src())) {
return false;
}
visited.insert(state); visited.insert(state);
expr* t = mvs[0].t(); expr* t = mvs[0].t();
if (!t) { if (!t) {
@ -689,6 +692,7 @@ bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) {
} }
bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) { bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
seq.reset();
zstring s; zstring s;
ptr_vector<expr> todo; ptr_vector<expr> todo;
expr *e1, *e2; expr *e1, *e2;
@ -728,6 +732,8 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
} }
if (is_sequence(*aut, seq)) { if (is_sequence(*aut, seq)) {
TRACE("seq", tout << seq << "\n";);
if (seq.empty()) { if (seq.empty()) {
result = m().mk_eq(a, m_util.str.mk_empty(m().get_sort(a))); result = m().mk_eq(a, m_util.str.mk_empty(m().get_sort(a)));
} }
@ -873,8 +879,7 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) {
br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) { br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {
sort* s; sort* s;
VERIFY(m_util.is_re(a, s)); VERIFY(m_util.is_re(a, s));
sort_ref seq(m_util.str.mk_seq(s), m()); result = m_util.re.mk_union(m_util.re.mk_to_re(m_util.str.mk_empty(s)), a);
result = m_util.re.mk_union(m_util.re.mk_to_re(m_util.str.mk_empty(seq)), a);
return BR_REWRITE1; return BR_REWRITE1;
} }