Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
Public Member Functions
DatatypeSortRef Class Reference
+ Inheritance diagram for DatatypeSortRef:

Public Member Functions

def num_constructors
 
def constructor
 
def recognizer
 
def accessor
 
- Public Member Functions inherited from SortRef
def as_ast
 
def get_id
 
def kind
 
def subsort
 
def cast
 
def name
 
def __eq__
 
def __ne__
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__
 
def __str__
 
def __repr__
 
def sexpr
 
def as_ast
 
def get_id
 
def ctx_ref
 
def eq
 
def translate
 
def hash
 
- Public Member Functions inherited from Z3PPObject
def use_pp
 

Additional Inherited Members

- Data Fields inherited from AstRef
 ast
 
 ctx
 

Detailed Description

Datatype sorts.

Definition at line 4301 of file z3py.py.

Member Function Documentation

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

4364  def accessor(self, i, j):
4365  """In Z3, each constructor has 0 or more accessor. The number of accessors is equal to the arity of the constructor.
4366 
4367  >>> List = Datatype('List')
4368  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4369  >>> List.declare('nil')
4370  >>> List = List.create()
4371  >>> List.num_constructors()
4372  2
4373  >>> List.constructor(0)
4374  cons
4375  >>> num_accs = List.constructor(0).arity()
4376  >>> num_accs
4377  2
4378  >>> List.accessor(0, 0)
4379  car
4380  >>> List.accessor(0, 1)
4381  cdr
4382  >>> List.constructor(1)
4383  nil
4384  >>> num_accs = List.constructor(1).arity()
4385  >>> num_accs
4386  0
4387  """
4388  if __debug__:
4389  _z3_assert(i < self.num_constructors(), "Invalid constructor index")
4390  _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index")
4391  return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx)
Function Declarations.
Definition: z3py.py:587
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(__in Z3_context c, __in Z3_sort t, unsigned idx_c, unsigned idx_a)
Return idx_a'th accessor for the idx_c'th constructor.
def ctx_ref
Definition: z3py.py:305
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 4316 of file z3py.py.

Referenced by DatatypeSortRef.accessor().

4317  def constructor(self, idx):
4318  """Return a constructor of the datatype `self`.
4319 
4320  >>> List = Datatype('List')
4321  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4322  >>> List.declare('nil')
4323  >>> List = List.create()
4324  >>> # List is now a Z3 declaration
4325  >>> List.num_constructors()
4326  2
4327  >>> List.constructor(0)
4328  cons
4329  >>> List.constructor(1)
4330  nil
4331  """
4332  if __debug__:
4333  _z3_assert(idx < self.num_constructors(), "Invalid constructor index")
4334  return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx)
Function Declarations.
Definition: z3py.py:587
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(__in Z3_context c, __in Z3_sort t, unsigned idx)
Return idx'th constructor.
def ctx_ref
Definition: z3py.py:305
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 4303 of file z3py.py.

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

4304  def num_constructors(self):
4305  """Return the number of constructors in the given Z3 datatype.
4306 
4307  >>> List = Datatype('List')
4308  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4309  >>> List.declare('nil')
4310  >>> List = List.create()
4311  >>> # List is now a Z3 declaration
4312  >>> List.num_constructors()
4313  2
4314  """
4315  return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast))
def ctx_ref
Definition: z3py.py:305
unsigned Z3_API Z3_get_datatype_sort_num_constructors(__in Z3_context c, __in Z3_sort t)
Return number of constructors for datatype.
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 4335 of file z3py.py.

4336  def recognizer(self, idx):
4337  """In Z3, each constructor has an associated recognizer predicate.
4338 
4339  If the constructor is named `name`, then the recognizer `is_name`.
4340 
4341  >>> List = Datatype('List')
4342  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4343  >>> List.declare('nil')
4344  >>> List = List.create()
4345  >>> # List is now a Z3 declaration
4346  >>> List.num_constructors()
4347  2
4348  >>> List.recognizer(0)
4349  is_cons
4350  >>> List.recognizer(1)
4351  is_nil
4352  >>> simplify(List.is_nil(List.cons(10, List.nil)))
4353  False
4354  >>> simplify(List.is_cons(List.cons(10, List.nil)))
4355  True
4356  >>> l = Const('l', List)
4357  >>> simplify(List.is_cons(l))
4358  is_cons(l)
4359  """
4360  if __debug__:
4361  _z3_assert(idx < self.num_constructors(), "Invalid recognizer index")
4362  return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx)
Function Declarations.
Definition: z3py.py:587
Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(__in Z3_context c, __in Z3_sort t, unsigned idx)
Return idx'th recognizer.
def ctx_ref
Definition: z3py.py:305