Skip to content

Commit

Permalink
simplify has-fixed-length
Browse files Browse the repository at this point in the history
Signed-off-by: Nikolaj Bjorner <[email protected]>
  • Loading branch information
NikolajBjorner committed Jul 31, 2020
1 parent 97ed1cd commit 566a0d5
Showing 1 changed file with 2 additions and 9 deletions.
11 changes: 2 additions & 9 deletions src/ast/rewriter/seq_rewriter.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
unsigned minl = re().min_length(a), maxl = re().max_length(a);
if (minl == maxl) {
len = minl;
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;
len = minl;
return minl == maxl;
}

br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) {
Expand Down

0 comments on commit 566a0d5

Please sign in to comment.