mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
add general purpose emptiness/non-emptiness check
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
88e36c6bf3
commit
0c2c1861f1
|
@ -280,8 +280,8 @@ namespace smt {
|
|||
VERIFY(u().is_re(r, seq_sort));
|
||||
expr_ref emp(re().mk_empty(seq_sort), m);
|
||||
literal lit = ~th.mk_eq(r, emp, false);
|
||||
expr_ref is_non_empty = sk().mk_is_non_empty(r, emp);
|
||||
th.add_axiom(~lit, th.mk_literal(is_non_empty));
|
||||
expr_ref is_empty = sk().mk_is_empty(r, emp);
|
||||
th.add_axiom(~lit, th.mk_literal(is_empty));
|
||||
}
|
||||
|
||||
void seq_regex::propagate_ne(expr* r1, expr* r2) {
|
||||
|
@ -297,8 +297,8 @@ namespace smt {
|
|||
VERIFY(u().is_re(r, seq_sort));
|
||||
expr_ref emp(re().mk_empty(seq_sort), m);
|
||||
literal lit = ~th.mk_eq(r, emp, false);
|
||||
expr_ref is_empty = sk().mk_is_empty(r, emp);
|
||||
th.add_axiom(~lit, th.mk_literal(is_empty));
|
||||
expr_ref is_non_empty = sk().mk_is_non_empty(r, emp);
|
||||
th.add_axiom(~lit, th.mk_literal(is_non_empty));
|
||||
}
|
||||
|
||||
bool seq_regex::is_member(expr* r, expr* u) {
|
||||
|
|
Loading…
Reference in a new issue