Integer values.
Definition at line 7190 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 7193 of file z3py.py.
7194 """Return a Z3 finite-domain numeral as a Python long (bignum) numeral. 7196 >>> s = FiniteDomainSort('S', 100) 7197 >>> v = FiniteDomainVal(3, s) 7203 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 7205 of file z3py.py.
7205 def as_string(self):
7206 """Return a Z3 finite-domain numeral as a Python string. 7208 >>> s = FiniteDomainSort('S', 100) 7209 >>> 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.