Inheritance diagram for DatatypeSortRef:

Public Member Functions
def	num_constructors (self)

def	constructor (self, idx)

def	recognizer (self, idx)

def	accessor (self, i, j)

Public Member Functions inherited from SortRef
def	as_ast (self)

def	get_id (self)

def	kind (self)

def	subsort (self, other)

def	cast (self, val)

def	name (self)

def	__eq__ (self, other)

def	__ne__ (self, other)

def	__hash__ (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	__nonzero__ (self)

def	__bool__ (self)

def	sexpr (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

Datatype sorts.

Definition at line 4915 of file z3py.py.

Member Function Documentation

◆ accessor()

def accessor	(	self,
		i,
		j
	)

In Z3, each constructor has 0 or more accessor. The number of accessors is equal to the arity of the constructor.

>>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> List.num_constructors()
2
>>> List.constructor(0)
cons
>>> num_accs = List.constructor(0).arity()
>>> num_accs
2
>>> List.accessor(0, 0)
car
>>> List.accessor(0, 1)
cdr
>>> List.constructor(1)
nil
>>> num_accs = List.constructor(1).arity()
>>> num_accs
0

Definition at line 4977 of file z3py.py.

     def accessor(self, i, j):
         """In Z3, each constructor has 0 or more accessor. The number of accessors is equal to the arity of the constructor.
  
         >>> List = Datatype('List')
         >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
         >>> List.declare('nil')
         >>> List = List.create()
         >>> List.num_constructors()
         2
         >>> List.constructor(0)
         cons
         >>> num_accs = List.constructor(0).arity()
         >>> num_accs
         2
         >>> List.accessor(0, 0)
         car
         >>> List.accessor(0, 1)
         cdr
         >>> List.constructor(1)
         nil
         >>> num_accs = List.constructor(1).arity()
         >>> num_accs
         0
         """
         if z3_debug():
             _z3_assert(i < self.num_constructors(), "Invalid constructor index")
             _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index")
         return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx)
  

◆ constructor()

def constructor	(	self,
		idx
	)

Return a constructor of the datatype `self`.

>>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> # List is now a Z3 declaration
>>> List.num_constructors()
2
>>> List.constructor(0)
cons
>>> List.constructor(1)
nil

Definition at line 4930 of file z3py.py.

     def constructor(self, idx):
         """Return a constructor of the datatype `self`.
  
         >>> List = Datatype('List')
         >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
         >>> List.declare('nil')
         >>> List = List.create()
         >>> # List is now a Z3 declaration
         >>> List.num_constructors()
         2
         >>> List.constructor(0)
         cons
         >>> List.constructor(1)
         nil
         """
         if z3_debug():
             _z3_assert(idx < self.num_constructors(), "Invalid constructor index")
         return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx)
  

Referenced by DatatypeSortRef.accessor().

◆ num_constructors()

def num_constructors ( self )

Return the number of constructors in the given Z3 datatype.

>>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> # List is now a Z3 declaration
>>> List.num_constructors()
2

Definition at line 4917 of file z3py.py.

     def num_constructors(self):
         """Return the number of constructors in the given Z3 datatype.
  
         >>> List = Datatype('List')
         >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
         >>> List.declare('nil')
         >>> List = List.create()
         >>> # List is now a Z3 declaration
         >>> List.num_constructors()
         2
         """
         return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast))
  

Referenced by DatatypeSortRef.accessor(), DatatypeSortRef.constructor(), and DatatypeSortRef.recognizer().

◆ recognizer()

def recognizer	(	self,
		idx
	)

In Z3, each constructor has an associated recognizer predicate.

If the constructor is named `name`, then the recognizer `is_name`.

>>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> # List is now a Z3 declaration
>>> List.num_constructors()
2
>>> List.recognizer(0)
is(cons)
>>> List.recognizer(1)
is(nil)
>>> simplify(List.is_nil(List.cons(10, List.nil)))
False
>>> simplify(List.is_cons(List.cons(10, List.nil)))
True
>>> l = Const('l', List)
>>> simplify(List.is_cons(l))
is(cons, l)

Definition at line 4949 of file z3py.py.

     def recognizer(self, idx):
         """In Z3, each constructor has an associated recognizer predicate.
  
         If the constructor is named `name`, then the recognizer `is_name`.
  
         >>> List = Datatype('List')
         >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
         >>> List.declare('nil')
         >>> List = List.create()
         >>> # List is now a Z3 declaration
         >>> List.num_constructors()
         2
         >>> List.recognizer(0)
         is(cons)
         >>> List.recognizer(1)
         is(nil)
         >>> simplify(List.is_nil(List.cons(10, List.nil)))
         False
         >>> simplify(List.is_cons(List.cons(10, List.nil)))
         True
         >>> l = Const('l', List)
         >>> simplify(List.is_cons(l))
         is(cons, l)
         """
         if z3_debug():
             _z3_assert(idx < self.num_constructors(), "Invalid recognizer index")
         return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx)
  