From fca8ffd9480a743209e7038041b1d26182c77361 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 23 Mar 2019 16:37:50 -0700 Subject: [PATCH] fix #2199 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 69c90c3f6..e5ab83187 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -10316,3 +10316,15 @@ def Loop(re, lo, hi=0): False """ return ReRef(Z3_mk_re_loop(re.ctx_ref(), re.as_ast(), lo, hi), re.ctx) + +def Range(lo, hi, ctx = None): + """Create the range regular expression over two sequences of length 1 + >>> range = Range("a","z") + >>> print(simplify(InRe("b", range))) + True + >>> print(simplify(InRe("bb", range))) + False + """ + lo = _coerce_seq(lo, ctx) + hi = _coerce_seq(hi, ctx) + return ReRef(Z3_mk_re_range(lo.ctx_ref(), lo.ast, hi.ast), lo.ctx)