mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix handling of AC operator ++ on regular expressions. Issue #804
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
71ca355257
commit
7a4c20698f
|
@ -335,6 +335,9 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
SASSERT(num_args == 1);
|
||||
return mk_re_opt(args[0], result);
|
||||
case OP_RE_CONCAT:
|
||||
if (num_args == 1) {
|
||||
result = args[0]; return BR_DONE;
|
||||
}
|
||||
SASSERT(num_args == 2);
|
||||
return mk_re_concat(args[0], args[1], result);
|
||||
case OP_RE_UNION:
|
||||
|
|
|
@ -555,7 +555,7 @@ func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* cons
|
|||
}
|
||||
match_right_assoc(*m_sigs[k], arity, domain, range, rng);
|
||||
func_decl_info info(m_family_id, k_seq);
|
||||
info.set_right_associative();
|
||||
info.set_right_associative(true);
|
||||
return m.mk_func_decl(m_sigs[(rng == m_string)?k_string:k_seq]->m_name, rng, rng, rng, info);
|
||||
}
|
||||
|
||||
|
|
|
@ -44,7 +44,8 @@ struct well_sorted_proc {
|
|||
void operator()(app * n) {
|
||||
unsigned num_args = n->get_num_args();
|
||||
func_decl * decl = n->get_decl();
|
||||
if (num_args != decl->get_arity() && !decl->is_associative()) {
|
||||
if (num_args != decl->get_arity() && !decl->is_associative() &&
|
||||
!decl->is_right_associative() && !decl->is_left_associative()) {
|
||||
TRACE("ws", tout << "unexpected number of arguments.\n" << mk_ismt2_pp(n, m_manager););
|
||||
warning_msg("unexpected number of arguments.");
|
||||
m_error = true;
|
||||
|
|
Loading…
Reference in a new issue