3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-04 22:14:45 -08:00
parent 2c1d2aad44
commit 2f9fda45c3

View file

@ -931,9 +931,9 @@ def _to_expr_ref(a, ctx):
if sk == Z3_ROUNDING_MODE_SORT:
return FPRMRef(a, ctx)
if sk == Z3_SEQ_SORT:
return SeqRef(a, ctx)
return SeqRef(a, ctx)
if sk == Z3_RE_SORT:
return ReRef(a, ctx)
return ReRef(a, ctx)
return ExprRef(a, ctx)
def _coerce_expr_merge(s, a):
@ -3573,24 +3573,24 @@ def Concat(*args):
ctx = args[0].ctx
if is_seq(args[0]):
if __debug__:
_z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.")
v = (Ast * sz)()
if __debug__:
_z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.")
v = (Ast * sz)()
for i in range(sz):
v[i] = args[i].as_ast()
return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx)
return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx)
if is_re(args[0]):
if __debug__:
_z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
v = (Ast * sz)()
for i in range(sz):
v[i] = args[i].as_ast()
return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx)
if __debug__:
_z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
v = (Ast * sz)()
for i in range(sz):
v[i] = args[i].as_ast()
return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx)
if __debug__:
_z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
r = args[0]
r = args[0]
for i in range(sz - 1):
r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx)
return r
@ -3607,14 +3607,14 @@ def Extract(high, low, a):
"c"
"""
if isinstance(high, str):
high = StringVal(high)
high = StringVal(high)
if is_seq(high):
s = high
offset = _py2expr(low, high.ctx)
length = _py2expr(a, high.ctx)
if __debug__:
_z3_assert(is_int(offset) and is_int(length), "Second and third arguments must be integers")
s = high
offset = _py2expr(low, high.ctx)
length = _py2expr(a, high.ctx)
if __debug__:
_z3_assert(is_int(offset) and is_int(length), "Second and third arguments must be integers")
return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
if __debug__:
_z3_assert(low <= high, "First argument must be greater than or equal to second argument")
@ -8951,15 +8951,15 @@ class SeqSortRef(SortRef):
"""Sequence sort."""
def is_string(self):
"""Determine if sort is a string
>>> s = StringSort()
>>> s.is_string()
True
>>> s = SeqSort(IntSort())
>>> s.is_string()
False
"""
return Z3_is_string_sort(self.ctx_ref(), self.ast)
"""Determine if sort is a string
>>> s = StringSort()
>>> s.is_string()
True
>>> s = SeqSort(IntSort())
>>> s.is_string()
False
"""
return Z3_is_string_sort(self.ctx_ref(), self.ast)
def StringSort(ctx=None):
"""Create a string sort
@ -8983,19 +8983,19 @@ class SeqRef(ExprRef):
"""Sequence expression."""
def sort(self):
return SeqSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
return SeqSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
def __add__(self, other):
return Concat(self, other)
return Concat(self, other)
def __getitem__(self, i):
return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
def is_string(self):
return Z3_is_string_sort(self.ctx_ref(), Z3_get_sort(self.ctx_ref(), self.as_ast()))
return Z3_is_string_sort(self.ctx_ref(), Z3_get_sort(self.ctx_ref(), self.as_ast()))
def is_string_value(self):
return Z3_is_string(self.ctx_ref(), self.as_ast())
return Z3_is_string(self.ctx_ref(), self.as_ast())
def as_string(self):
"""Return a string representation of sequence expression."""
@ -9004,17 +9004,17 @@ class SeqRef(ExprRef):
def _coerce_seq(s, ctx=None):
if isinstance(s, str):
ctx = _get_ctx(ctx)
s = StringVal(s, ctx)
ctx = _get_ctx(ctx)
s = StringVal(s, ctx)
return s
def _get_ctx2(a, b, ctx=None):
if is_expr(a):
return a.ctx
return a.ctx
if is_expr(b):
return b.ctx
return b.ctx
if ctx is None:
ctx = main_ctx()
ctx = main_ctx()
return ctx
def is_seq(a):
@ -9136,7 +9136,7 @@ def Replace(s, src, dst):
"""
ctx = _get_ctx2(dst, s)
if ctx is None and is_expr(src):
ctx = src.ctx
ctx = src.ctx
src = _coerce_seq(src, ctx)
dst = _coerce_seq(dst, ctx)
s = _coerce_seq(s, ctx)
@ -9154,12 +9154,12 @@ def IndexOf(s, substr, offset):
"""
ctx = None
if is_expr(offset):
ctx = offset.ctx
ctx = offset.ctx
ctx = _get_ctx2(s, substr, ctx)
s = _coerce_seq(s, ctx)
substr = _coerce_seq(substr, ctx)
if isinstance(offset, int):
offset = IntVal(offset, ctx)
offset = IntVal(offset, ctx)
return SeqRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)
def Length(s):
@ -9191,10 +9191,10 @@ class ReSortRef(SortRef):
def ReSort(s):
if is_ast(s):
return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.as_ast()), ctx)
return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.as_ast()), ctx)
if s is None or isinstance(s, Context):
ctx = _get_ctx(s)
return ReSortRef(Z3_mk_re_sort(ctx.ref(), Z3_mk_string_sort(ctx.ref())), ctx)
ctx = _get_ctx(s)
return ReSortRef(Z3_mk_re_sort(ctx.ref(), Z3_mk_string_sort(ctx.ref())), ctx)
raise Z3Exception("Regular expression sort constructor expects either a string or a context or no argument")
@ -9202,7 +9202,7 @@ class ReRef(ExprRef):
"""Regular expressions."""
def __add__(self, other):
return Union(self, other)
return Union(self, other)
def is_re(s):
@ -9232,13 +9232,12 @@ def Union(*args):
sz = len(args)
if __debug__:
_z3_assert(sz >= 2, "At least two arguments expected.")
_z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
_z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
ctx = args[0].ctx
v = (Ast * sz)()
for i in range(sz):
v[i] = args[i].as_ast()
v[i] = args[i].as_ast()
return ReRef(Z3_mk_re_union(ctx.ref(), sz, v), ctx)
def Plus(re):
"""Create the regular expression accepting one or more repetitions of argument.