Integer values.
Definition at line 7305 of file z3py.py.
◆ as_long()
Return a Z3 finite-domain numeral as a Python long (bignum) numeral.
>>> s = FiniteDomainSort('S', 100)
>>> v = FiniteDomainVal(3, s)
>>> v
3
>>> v.as_long() + 1
4
Definition at line 7308 of file z3py.py.
7309 """Return a Z3 finite-domain numeral as a Python long (bignum) numeral.
7311 >>> s = FiniteDomainSort('S', 100)
7312 >>> v = FiniteDomainVal(3, s)
7318 return int(self.as_string())
◆ as_string()
Return a Z3 finite-domain numeral as a Python string.
>>> s = FiniteDomainSort('S', 100)
>>> v = FiniteDomainVal(42, s)
>>> v.as_string()
'42'
Reimplemented from FiniteDomainRef.
Definition at line 7320 of file z3py.py.
7320 def as_string(self):
7321 """Return a Z3 finite-domain numeral as a Python string.
7323 >>> s = FiniteDomainSort('S', 100)
7324 >>> v = FiniteDomainVal(42, s)
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a decimal string of a numeric constant term.