From 5d10cb7af4f264c40e102071b3f4d788bfb5d5b6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 Nov 2020 18:07:05 -0800 Subject: [PATCH] fix #4791 - diff is left associative Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 20 +++++++++++++++----- src/ast/seq_decl_plugin.h | 5 ++++- 2 files changed, 19 insertions(+), 6 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 5c3202e8a..ea47bc455 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -451,7 +451,7 @@ bool seq_decl_plugin::match(ptr_vector& binding, sort* s, sort* sP) { /* \brief match right associative operator. */ -void seq_decl_plugin::match_right_assoc(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) { +void seq_decl_plugin::match_assoc(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) { ptr_vector binding; ast_manager& m = *m_manager; if (dsz == 0) { @@ -463,7 +463,7 @@ void seq_decl_plugin::match_right_assoc(psig& sig, unsigned dsz, sort *const* do bool is_match = true; for (unsigned i = 0; is_match && i < dsz; ++i) { SASSERT(dom[i]); - is_match = match(binding, dom[i], sig.m_dom[0].get()); + is_match = match(binding, dom[i], sig.m_dom.get(0)); } if (range && is_match) { is_match = match(binding, range, sig.m_range); @@ -722,18 +722,28 @@ func_decl* seq_decl_plugin::mk_str_fun(decl_kind k, unsigned arity, sort* const* } func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_seq, decl_kind k_string) { + return mk_assoc_fun(k, arity, domain, range, k_seq, k_string, true); +} + +func_decl* seq_decl_plugin::mk_left_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_seq, decl_kind k_string) { + return mk_assoc_fun(k, arity, domain, range, k_seq, k_string, false); +} + +func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_seq, decl_kind k_string, bool is_right) { ast_manager& m = *m_manager; sort_ref rng(m); if (arity == 0) { m.raise_exception("Invalid function application. At least one argument expected"); } - match_right_assoc(*m_sigs[k], arity, domain, range, rng); + match_assoc(*m_sigs[k], arity, domain, range, rng); func_decl_info info(m_family_id, k_seq); - info.set_right_associative(true); + if (is_right) + info.set_right_associative(true); info.set_left_associative(true); return m.mk_func_decl(m_sigs[(rng == m_string)?k_string:k_seq]->m_name, rng, rng, rng, info); } + func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { init(); @@ -854,7 +864,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_RE_INTERSECT: case OP_RE_DIFF: m_has_re = true; - return mk_assoc_fun(k, arity, domain, range, k, k); + return mk_left_assoc_fun(k, arity, domain, range, k, k); case OP_SEQ_REPLACE_RE_ALL: case OP_SEQ_REPLACE_RE: diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 10b3014d2..690bfb19d 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -177,7 +177,7 @@ class seq_decl_plugin : public decl_plugin { void match(psig& sig, unsigned dsz, sort* const* dom, sort* range, sort_ref& rng); - void match_right_assoc(psig& sig, unsigned dsz, sort* const* dom, sort* range, sort_ref& rng); + void match_assoc(psig& sig, unsigned dsz, sort* const* dom, sort* range, sort_ref& rng); bool match(ptr_vector& binding, sort* s, sort* sP); @@ -188,6 +188,9 @@ class seq_decl_plugin : public decl_plugin { func_decl* mk_seq_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string); func_decl* mk_str_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_seq); func_decl* mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq); + func_decl* mk_left_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq); + func_decl* mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq, bool is_right); + void init();