Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator 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__
 
def __hash__
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__
 
def __deepcopy__
 
def __str__
 
def __repr__
 
def __eq__
 
def __hash__
 
def __nonzero__
 
def __bool__
 
def sexpr
 
def as_ast
 
def get_id
 
def ctx_ref
 
def eq
 
def translate
 
def __copy__
 
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 4854 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 4916 of file z3py.py.

4917  def accessor(self, i, j):
4918  """In Z3, each constructor has 0 or more accessor. The number of accessors is equal to the arity of the constructor.
4919 
4920  >>> List = Datatype('List')
4921  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4922  >>> List.declare('nil')
4923  >>> List = List.create()
4924  >>> List.num_constructors()
4925  2
4926  >>> List.constructor(0)
4927  cons
4928  >>> num_accs = List.constructor(0).arity()
4929  >>> num_accs
4930  2
4931  >>> List.accessor(0, 0)
4932  car
4933  >>> List.accessor(0, 1)
4934  cdr
4935  >>> List.constructor(1)
4936  nil
4937  >>> num_accs = List.constructor(1).arity()
4938  >>> num_accs
4939  0
4940  """
4941  if z3_debug():
4942  _z3_assert(i < self.num_constructors(), "Invalid constructor index")
4943  _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index")
4944  return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx)
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(Z3_context c, Z3_sort t, unsigned idx_c, unsigned idx_a)
Return idx_a'th accessor for the idx_c'th constructor.
Function Declarations.
Definition: z3py.py:651
def z3_debug
Definition: z3py.py:58
def ctx_ref
Definition: z3py.py:352
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 4869 of file z3py.py.

Referenced by DatatypeSortRef.accessor().

4870  def constructor(self, idx):
4871  """Return a constructor of the datatype `self`.
4872 
4873  >>> List = Datatype('List')
4874  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4875  >>> List.declare('nil')
4876  >>> List = List.create()
4877  >>> # List is now a Z3 declaration
4878  >>> List.num_constructors()
4879  2
4880  >>> List.constructor(0)
4881  cons
4882  >>> List.constructor(1)
4883  nil
4884  """
4885  if z3_debug():
4886  _z3_assert(idx < self.num_constructors(), "Invalid constructor index")
4887  return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx)
Function Declarations.
Definition: z3py.py:651
def z3_debug
Definition: z3py.py:58
def ctx_ref
Definition: z3py.py:352
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th constructor.
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 4856 of file z3py.py.

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

4857  def num_constructors(self):
4858  """Return the number of constructors in the given Z3 datatype.
4859 
4860  >>> List = Datatype('List')
4861  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4862  >>> List.declare('nil')
4863  >>> List = List.create()
4864  >>> # List is now a Z3 declaration
4865  >>> List.num_constructors()
4866  2
4867  """
4868  return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast))
unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t)
Return number of constructors for datatype.
def ctx_ref
Definition: z3py.py:352
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 4888 of file z3py.py.

4889  def recognizer(self, idx):
4890  """In Z3, each constructor has an associated recognizer predicate.
4891 
4892  If the constructor is named `name`, then the recognizer `is_name`.
4893 
4894  >>> List = Datatype('List')
4895  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4896  >>> List.declare('nil')
4897  >>> List = List.create()
4898  >>> # List is now a Z3 declaration
4899  >>> List.num_constructors()
4900  2
4901  >>> List.recognizer(0)
4902  is(cons)
4903  >>> List.recognizer(1)
4904  is(nil)
4905  >>> simplify(List.is_nil(List.cons(10, List.nil)))
4906  False
4907  >>> simplify(List.is_cons(List.cons(10, List.nil)))
4908  True
4909  >>> l = Const('l', List)
4910  >>> simplify(List.is_cons(l))
4911  is(cons, l)
4912  """
4913  if z3_debug():
4914  _z3_assert(idx < self.num_constructors(), "Invalid recognizer index")
4915  return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx)
Function Declarations.
Definition: z3py.py:651
Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th recognizer.
def z3_debug
Definition: z3py.py:58
def ctx_ref
Definition: z3py.py:352