DatatypeRef Class Reference

Inheritance diagram for DatatypeRef:

Public Member Functions
	sort (self)
	update_field (self, field_accessor, new_value)
Public Member Functions inherited from ExprRef
	as_ast (self)
	get_id (self)
	sort_kind (self)
	__eq__ (self, other)
	__hash__ (self)
	__ne__ (self, other)
	params (self)
	decl (self)
	kind (self)
	num_args (self)
	arg (self, idx)
	children (self)
	update (self, *args)
	from_string (self, s)
	serialize (self)
Public Member Functions inherited from AstRef
	__init__ (self, ast, ctx=None)
	__del__ (self)
	__deepcopy__ (self, memo={})
	__str__ (self)
	__repr__ (self)
	__eq__ (self, other)
	__hash__ (self)
	__nonzero__ (self)
	__bool__ (self)
	sexpr (self)
	ctx_ref (self)
	eq (self, other)
	translate (self, target)
	__copy__ (self)
	hash (self)
	py_value (self)
Public Member Functions inherited from Z3PPObject
	use_pp (self)

Additional Inherited Members
Data Fields inherited from AstRef
	ast = ast
	ctx = _get_ctx(ctx)
Protected Member Functions inherited from Z3PPObject
	_repr_html_ (self)

Detailed Description

Datatype expressions.

Definition at line 5521 of file z3py.py.

Member Function Documentation

sort()

sort

(

self

)

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

Reimplemented from ExprRef.

Definition at line 5524 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)
 

update_field()

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 5528 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
        )