Z3 |

Public Member Functions
IntNumRef Class Reference
Inheritance diagram for IntNumRef:

## Public Member Functions
def | as_long (self)
def | as_string (self)
def | as_binary_string (self)
Public Member Functions inherited from ArithRef
def | sort (self)
def | is_int (self)
def | is_real (self)
def | __add__ (self, other)
def | __radd__ (self, other)
def | __mul__ (self, other)
def | __rmul__ (self, other)
def | __sub__ (self, other)
def | __rsub__ (self, other)
def | __pow__ (self, other)
def | __rpow__ (self, other)
def | __div__ (self, other)
def | __truediv__ (self, other)
def | __rdiv__ (self, other)
def | __rtruediv__ (self, other)
def | __mod__ (self, other)
def | __rmod__ (self, other)
def | __neg__ (self)
def | __pos__ (self)
def | __le__ (self, other)
def | __lt__ (self, other)
def | __gt__ (self, other)
def | __ge__ (self, other)
Public Member Functions inherited from ExprRef
def | as_ast (self)
def | get_id (self)
def | sort (self)
def | sort_kind (self)
def | __eq__ (self, other)
def | __hash__ (self)
def | __ne__ (self, other)
def | params (self)
def | decl (self)
def | num_args (self)
def | arg (self, idx)
def | children (self)
Public Member Functions inherited from AstRef
def | __init__ (self, ast, ctx=None)
def | __del__ (self)
def | __deepcopy__ (self, memo={})
def | __str__ (self)
def | __repr__ (self)
def | __eq__ (self, other)
def | __hash__ (self)
def | __nonzero__ (self)
def | __bool__ (self)
def | sexpr (self)
def | as_ast (self)
def | get_id (self)
def | ctx_ref (self)
def | eq (self, other)
def | translate (self, target)
def | __copy__ (self)
def | hash (self)
Public Member Functions inherited from Z3PPObject
def | use_pp (self)

## Additional Inherited Members
Data Fields inherited from AstRef
| ast
| ctx

## Detailed Description

    Integer values.

Definition at line 2921 of file z3py.py.

## Member Function Documentation

## ◆ as_binary_string()

def as_binary_string | ( |  | self | ) |

    Return a Z3 integer numeral as a Python binary string.
    >>> v = IntVal(10)
    >>> v.as_binary_string()
    '1010'

Definition at line 2945 of file z3py.py.

2945 def as_binary_string(self):
2946 """Return a Z3 integer numeral as a Python binary string.
2947 >>> v = IntVal(10)
2948 >>> v.as_binary_string()
2949 '1010'
2950 """
2951 return Z3_get_numeral_binary_string(self.ctx_ref(), self.as_ast())
2952
2953
z3py.IntVal
def IntVal(val, ctx=None)
Definition: z3py.py:3150
Z3_get_numeral_binary_string
Z3_string Z3_API Z3_get_numeral_binary_string(Z3_context c, Z3_ast a)
Return numeral value, as a binary string of a numeric constant term.

## ◆ as_long()

def as_long | ( |  | self | ) |

    Return a Z3 integer numeral as a Python long (bignum) numeral.

    >>> v = IntVal(1)
    >>> v + 1
    1 + 1
    >>> v.as_long() + 1
    2

Definition at line 2924 of file z3py.py.

2924 def as_long(self):
2925 """Return a Z3 integer numeral as a Python long (bignum) numeral.
2926
2927 >>> v = IntVal(1)
2928 >>> v + 1
2929 1 + 1
2930 >>> v.as_long() + 1
2931 2
2932 """
2933 if z3_debug():
2934 _z3_assert(self.is_int(), "Integer value expected")
2935 return int(self.as_string())
2936
z3py.z3_debug
def z3_debug()
Definition: z3py.py:64

Referenced by BitVecNumRef.as_signed_long().

## ◆ as_string()

def as_string | ( |  | self | ) |

    Return a Z3 integer numeral as a Python string.
    >>> v = IntVal(100)
    >>> v.as_string()
    '100'

Definition at line 2937 of file z3py.py.

2937 def as_string(self):
2938 """Return a Z3 integer numeral as a Python string.
2939 >>> v = IntVal(100)
2940 >>> v.as_string()
2941 '100'
2942 """
2943 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
2944
Z3_get_numeral_string
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.

Referenced by IntNumRef.as_long(), BitVecNumRef.as_long(), and FiniteDomainNumRef.as_long().