mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

fix #4791 - diff is left associative

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-11-11 18:07:05 -08:00
parent 72e57f550d
commit 5d10cb7af4
2 changed files with 19 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/ast/seq_decl_plugin.cpp
View file

@ -451,7 +451,7 @@ bool seq_decl_plugin::match(ptr_vector<sort>& binding, sort* s, sort* sP) {
/* /*
\brief match right associative operator. \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<sort> binding; ptr_vector<sort> binding;
ast_manager& m = *m_manager; ast_manager& m = *m_manager;
if (dsz == 0) { 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; bool is_match = true;
for (unsigned i = 0; is_match && i < dsz; ++i) { for (unsigned i = 0; is_match && i < dsz; ++i) {
SASSERT(dom[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) { if (range && is_match) {
is_match = match(binding, range, sig.m_range); 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) { 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; ast_manager& m = *m_manager;
sort_ref rng(m); sort_ref rng(m);
if (arity == 0) { if (arity == 0) {
m.raise_exception("Invalid function application. At least one argument expected"); 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); 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); 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); 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, func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) { unsigned arity, sort * const * domain, sort * range) {
init(); 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_INTERSECT:
case OP_RE_DIFF: case OP_RE_DIFF:
m_has_re = true; 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_ALL:
case OP_SEQ_REPLACE_RE: case OP_SEQ_REPLACE_RE:

5
src/ast/seq_decl_plugin.h
View file

@ -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(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<sort>& binding, sort* s, sort* sP); bool match(ptr_vector<sort>& 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_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_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_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(); void init();