mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

fix co-factoring'

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-12-14 10:12:38 -08:00
parent 5348af3c4c
commit b1d167de5b
5 changed files with 17 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/seq_regex.cpp
View file

@ -524,9 +524,10 @@ namespace smt {
sort* seq_sort = nullptr;
VERIFY(u().is_re(r1, seq_sort));
expr_ref r = symmetric_diff(r1, r2);
expr_ref s(m.mk_fresh_const("re.member", seq_sort), m);
expr_ref is_member(re().mk_in_re(s, r), m);
th.add_axiom(th.mk_eq(r1, r2, false), th.mk_literal(is_member));
expr_ref emp(re().mk_empty(r->get_sort()), m);
expr_ref n(m.mk_fresh_const("re.char", seq_sort), m);
expr_ref is_non_empty = sk().mk_is_non_empty(r, r, n);
th.add_axiom(th.mk_eq(r1, r2, false), th.mk_literal(is_non_empty));
}
bool seq_regex::is_member(expr* r, expr* u) {

4
src/smt/seq_regex.h
View file

@ -184,8 +184,6 @@ namespace smt {
bool block_if_empty(expr* r, literal lit);
void propagate_is_non_empty(literal lit);
public:
seq_regex(theory_seq& th);
@ -206,6 +204,8 @@ namespace smt {
void propagate_ne(expr* r1, expr* r2);
void propagate_is_empty(literal lit);
void propagate_is_non_empty(literal lit);
};

4
src/smt/theory_seq.cpp
View file

@ -3033,6 +3033,10 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
propagate_length_limit(e);
}
}
else if (m_sk.is_is_non_empty(e)) {
if (is_true)
m_regex.propagate_is_non_empty(lit);
}
else if (m_util.str.is_lt(e) || m_util.str.is_le(e)) {
m_lts.push_back(e);
}