Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups 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 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 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 4217 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 4279 of file z3py.py.

4280  def accessor(self, i, j):
4281  """In Z3, each constructor has 0 or more accessor. The number of accessors is equal to the arity of the constructor.
4282 
4283  >>> List = Datatype('List')
4284  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4285  >>> List.declare('nil')
4286  >>> List = List.create()
4287  >>> List.num_constructors()
4288  2
4289  >>> List.constructor(0)
4290  cons
4291  >>> num_accs = List.constructor(0).arity()
4292  >>> num_accs
4293  2
4294  >>> List.accessor(0, 0)
4295  car
4296  >>> List.accessor(0, 1)
4297  cdr
4298  >>> List.constructor(1)
4299  nil
4300  >>> num_accs = List.constructor(1).arity()
4301  >>> num_accs
4302  0
4303  """
4304  if __debug__:
4305  _z3_assert(i < self.num_constructors(), "Invalid constructor index")
4306  _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index")
4307  return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx)
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 4232 of file z3py.py.

Referenced by DatatypeSortRef.accessor().

4233  def constructor(self, idx):
4234  """Return a constructor of the datatype `self`.
4235 
4236  >>> List = Datatype('List')
4237  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4238  >>> List.declare('nil')
4239  >>> List = List.create()
4240  >>> # List is now a Z3 declaration
4241  >>> List.num_constructors()
4242  2
4243  >>> List.constructor(0)
4244  cons
4245  >>> List.constructor(1)
4246  nil
4247  """
4248  if __debug__:
4249  _z3_assert(idx < self.num_constructors(), "Invalid constructor index")
4250  return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx)
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 4219 of file z3py.py.

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

4220  def num_constructors(self):
4221  """Return the number of constructors in the given Z3 datatype.
4222 
4223  >>> List = Datatype('List')
4224  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4225  >>> List.declare('nil')
4226  >>> List = List.create()
4227  >>> # List is now a Z3 declaration
4228  >>> List.num_constructors()
4229  2
4230  """
4231  return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast))
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 4251 of file z3py.py.

4252  def recognizer(self, idx):
4253  """In Z3, each constructor has an associated recognizer predicate.
4254 
4255  If the constructor is named `name`, then the recognizer `is_name`.
4256 
4257  >>> List = Datatype('List')
4258  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4259  >>> List.declare('nil')
4260  >>> List = List.create()
4261  >>> # List is now a Z3 declaration
4262  >>> List.num_constructors()
4263  2
4264  >>> List.recognizer(0)
4265  is_cons
4266  >>> List.recognizer(1)
4267  is_nil
4268  >>> simplify(List.is_nil(List.cons(10, List.nil)))
4269  False
4270  >>> simplify(List.is_cons(List.cons(10, List.nil)))
4271  True
4272  >>> l = Const('l', List)
4273  >>> simplify(List.is_cons(l))
4274  is_cons(l)
4275  """
4276  if __debug__:
4277  _z3_assert(idx < self.num_constructors(), "Invalid recognizer index")
4278  return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx)