Integer values.
Definition at line 7263 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 7266 of file z3py.py.
7267 """Return a Z3 finite-domain numeral as a Python long (bignum) numeral. 7269 >>> s = FiniteDomainSort('S', 100) 7270 >>> v = FiniteDomainVal(3, s) 7276 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 7278 of file z3py.py.
7278 def as_string(self):
7279 """Return a Z3 finite-domain numeral as a Python string. 7281 >>> s = FiniteDomainSort('S', 100) 7282 >>> v = FiniteDomainVal(42, s) Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a string of a numeric constant term.