DatatypeRef Class Reference

Inheritance diagram for DatatypeRef:

Public Member Functions
def	sort (self)
def	update_field (self, field_accessor, new_value)
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	kind (self)
def	num_args (self)
def	arg (self, idx)
def	children (self)
def	update (self, args)
def	from_string (self, s)
def	serialize (self)
Public Member Functions inherited from AstRef
def	__init__
def	__del__ (self)
def	__deepcopy__
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)
def	py_value (self)
Public Member Functions inherited from Z3PPObject
def	use_pp (self)

Additional Inherited Members
Data Fields inherited from AstRef
	ast
	ctx

Detailed Description

Datatype expressions.

Definition at line 5534 of file z3py.py.

Member Function Documentation

def sort

(

self

)

Return the datatype sort of the datatype expression `self`.

Definition at line 5537 of file z3py.py.

    def sort(self):
        """Return the datatype sort of the datatype expression `self`."""
        return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)

def update_field	(		self,
			field_accessor,
			new_value
	)

Return a new datatype expression with the specified field updated.

Args:
    field_accessor: The accessor function declaration for the field to update
    new_value: The new value for the field
    
Returns:
    A new datatype expression with the field updated, other fields unchanged
    
Example:
    >>> Person = Datatype('Person')
    >>> Person.declare('person', ('name', StringSort()), ('age', IntSort()))
    >>> Person = Person.create()
    >>> person_age = Person.accessor(0, 1)  # age accessor
    >>> p = Const('p', Person)
    >>> p2 = p.update_field(person_age, IntVal(30))

Definition at line 5541 of file z3py.py.

    def update_field(self, field_accessor, new_value):
        """Return a new datatype expression with the specified field updated.
        
        Args:
            field_accessor: The accessor function declaration for the field to update
            new_value: The new value for the field
            
        Returns:
            A new datatype expression with the field updated, other fields unchanged
            
        Example:
            >>> Person = Datatype('Person')
            >>> Person.declare('person', ('name', StringSort()), ('age', IntSort()))
            >>> Person = Person.create()
            >>> person_age = Person.accessor(0, 1)  # age accessor
            >>> p = Const('p', Person)
            >>> p2 = p.update_field(person_age, IntVal(30))
        """
        if z3_debug():
            _z3_assert(is_func_decl(field_accessor), "Z3 function declaration expected")
            _z3_assert(is_expr(new_value), "Z3 expression expected")
        return _to_expr_ref(
            Z3_datatype_update_field(self.ctx_ref(), field_accessor.ast, self.as_ast(), new_value.as_ast()),
            self.ctx
        )