Integer values.
Definition at line 6605 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 6608 of file z3py.py.
6609 """Return a Z3 finite-domain numeral as a Python long (bignum) numeral. 6611 >>> s = FiniteDomainSort('S', 100) 6612 >>> v = FiniteDomainVal(3, s) 6618 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'
Definition at line 6620 of file z3py.py.
6620 def as_string(self):
6621 """Return a Z3 finite-domain numeral as a Python string. 6623 >>> s = FiniteDomainSort('S', 100) 6624 >>> 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.