mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

Bugfix for finite domains in Python API.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-12-02 22:34:09 +00:00
parent b77f20fb0c
commit d23dce4f7b
1 changed files with 9 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/api/python/z3.py
View file

@ -6417,13 +6417,15 @@ class FiniteDomainSortRef(SortRef):
def FiniteDomainSort(name, sz, ctx=None): def FiniteDomainSort(name, sz, ctx=None):
"""Create a named finite domain sort of a given size sz""" """Create a named finite domain sort of a given size sz"""
if not isinstance(name, Symbol):
name = to_symbol(name)
ctx = _get_ctx(ctx) ctx = _get_ctx(ctx)
return FiniteDomainSortRef(Z3_mk_finite_domain_sort(ctx.ref(), name, sz), ctx) return FiniteDomainSortRef(Z3_mk_finite_domain_sort(ctx.ref(), name, sz), ctx)
def is_finite_domain_sort(s): def is_finite_domain_sort(s):
"""Return True if `s` is a Z3 finite-domain sort. """Return True if `s` is a Z3 finite-domain sort.
>>> is_finite_domain_sort(FiniteDomainSort("S", 100)) >>> is_finite_domain_sort(FiniteDomainSort('S', 100))
True True
>>> is_finite_domain_sort(IntSort()) >>> is_finite_domain_sort(IntSort())
False False
@ -6445,7 +6447,7 @@ class FiniteDomainRef(ExprRef):
def is_finite_domain(a): def is_finite_domain(a):
"""Return `True` if `a` is a Z3 finite-domain expression. """Return `True` if `a` is a Z3 finite-domain expression.
>>> s = FiniteDomainSort("S", 100) >>> s = FiniteDomainSort('S', 100)
>>> b = Const('b', s) >>> b = Const('b', s)
>>> is_finite_domain(b) >>> is_finite_domain(b)
True True
@ -6461,7 +6463,7 @@ class FiniteDomainNumRef(FiniteDomainRef):
def as_long(self): def as_long(self):
"""Return a Z3 finite-domain numeral as a Python long (bignum) numeral. """Return a Z3 finite-domain numeral as a Python long (bignum) numeral.
>>> s = FiniteDomainSort("S", 100) >>> s = FiniteDomainSort('S', 100)
>>> v = FiniteDomainVal(3, s) >>> v = FiniteDomainVal(3, s)
>>> v >>> v
3 3
@ -6473,7 +6475,7 @@ class FiniteDomainNumRef(FiniteDomainRef):
def as_string(self): def as_string(self):
"""Return a Z3 finite-domain numeral as a Python string. """Return a Z3 finite-domain numeral as a Python string.
>>> s = FiniteDomainSort("S", 100) >>> s = FiniteDomainSort('S', 100)
>>> v = FiniteDomainVal(42, s) >>> v = FiniteDomainVal(42, s)
>>> v.as_string() >>> v.as_string()
'42' '42'
@ -6484,10 +6486,10 @@ class FiniteDomainNumRef(FiniteDomainRef):
def FiniteDomainVal(val, sort, ctx=None): def FiniteDomainVal(val, sort, ctx=None):
"""Return a Z3 finite-domain value. If `ctx=None`, then the global context is used. """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used.
>>> s = FiniteDomainSort("S", 256) >>> s = FiniteDomainSort('S', 256)
>>> FiniteDomainVal(255, s) >>> FiniteDomainVal(255, s)
255 255
>>> FiniteDomainVal("100", s) >>> FiniteDomainVal('100', s)
100 100
""" """
if __debug__: if __debug__:
@ -6498,7 +6500,7 @@ def FiniteDomainVal(val, sort, ctx=None):
def is_finite_domain_value(a): def is_finite_domain_value(a):
"""Return `True` if `a` is a Z3 finite-domain value. """Return `True` if `a` is a Z3 finite-domain value.
>>> s = FiniteDomainSort("S", 100) >>> s = FiniteDomainSort('S', 100)
>>> b = Const('b', s) >>> b = Const('b', s)
>>> is_finite_domain_value(b) >>> is_finite_domain_value(b)
False False