mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

simplify has-fixed-length

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-31 11:57:07 -07:00
parent 97ed1cd07d
commit 566a0d540a
1 changed files with 2 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/ast/rewriter/seq_rewriter.cpp
View file

@ -3094,15 +3094,8 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
bool seq_rewriter::has_fixed_length_constraint(expr* a, unsigned& len) { bool seq_rewriter::has_fixed_length_constraint(expr* a, unsigned& len) {
unsigned minl = re().min_length(a), maxl = re().max_length(a); unsigned minl = re().min_length(a), maxl = re().max_length(a);
if (minl == maxl) { len = minl;
len = minl; return minl == maxl;
return true;
}
expr* b = nullptr, *c = nullptr;
if (re().is_intersection(a, b, c)) {
return has_fixed_length_constraint(b, len) || has_fixed_length_constraint(c, len);
}
return false;
} }
br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) { br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) {