Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions
IntNumRef Class Reference
+ Inheritance diagram for IntNumRef:

Public Member Functions

def as_long
def as_string

Detailed Description

Integer values.

Definition at line 2472 of file z3py.py.


Member Function Documentation

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 2475 of file z3py.py.

02475 
02476     def as_long(self):
02477         """Return a Z3 integer numeral as a Python long (bignum) numeral. 
02478         
02479         >>> v = IntVal(1)
02480         >>> v + 1
02481         1 + 1
02482         >>> v.as_long() + 1
02483         2
02484         """
02485         if __debug__:
02486             _z3_assert(self.is_int(), "Integer value expected")
02487         return int(self.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 2488 of file z3py.py.

Referenced by IntNumRef.as_long().

02488 
02489     def as_string(self):
02490         """Return a Z3 integer numeral as a Python string.
02491         >>> v = IntVal(100)
02492         >>> v.as_string()
02493         '100'
02494         """
02495         return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines