Z3 |

Public Member Functions
FiniteDomainNumRef Class Reference
Inheritance diagram for FiniteDomainNumRef:

## Public Member Functions
def | as_long (self)
def | as_string (self)
Public Member Functions inherited from FiniteDomainRef
def | sort (self)
def | as_string (self)
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 7634 of file z3py.py.

## Member Function Documentation

## ◆ as_long()

def as_long | ( |  | self | ) |

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

7637 def as_long(self):
7638 """Return a Z3 finite-domain numeral as a Python long (bignum) numeral.
7639
7640 >>> s = FiniteDomainSort('S', 100)
7641 >>> v = FiniteDomainVal(3, s)
7642 >>> v
7643 3
7644 >>> v.as_long() + 1
7645 4
7646 """
7647 return int(self.as_string())
7648
z3py.FiniteDomainVal
def FiniteDomainVal(val, sort, ctx=None)
Definition: z3py.py:7660
z3py.FiniteDomainSort
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:7590

Referenced by BitVecNumRef.as_signed_long().

## ◆ as_string()

def as_string | ( |  | self | ) |

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

7649 def as_string(self):
7650 """Return a Z3 finite-domain numeral as a Python string.
7651
7652 >>> s = FiniteDomainSort('S', 100)
7653 >>> v = FiniteDomainVal(42, s)
7654 >>> v.as_string()
7655 '42'
7656 """
7657 return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
7658
7659
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().