mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-29 11:58:51 +00:00
Code Activity

reuse char extraction from seq_util

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-06-09 15:19:15 -07:00
parent 867dc175c5
commit 72575ff962
2 changed files with 7 additions and 64 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/rewriter/seq_derive.h
View file

@ -150,7 +150,6 @@ namespace seq {
// Predicate implication for character range conditions.
bool pred_implies(bool sign_a, expr* a, bool sign_b, expr* b);
bool pred_implies(expr* a, expr* b);
bool extract_char_range(expr* cond, unsigned& lo, unsigned& hi);
// Normalize reverse(r) by pushing reverse inward
expr_ref normalize_reverse(expr* r);