Z3
Public Member Functions
DatatypeSortRef Class Reference
+ 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 __str__ (self)
 
def __repr__ (self)
 
def __eq__ (self, other)
 
def __hash__ (self)
 
def __nonzero__ (self)
 
def __bool__ (self)
 
def sexpr (self)
 
def as_ast (self)
 
def get_id (self)
 
def ctx_ref (self)
 
def eq (self, other)
 
def translate (self, target)
 
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 4477 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 4539 of file z3py.py.

4539  def accessor(self, i, j):
4540  """In Z3, each constructor has 0 or more accessor. The number of accessors is equal to the arity of the constructor.
4541 
4542  >>> List = Datatype('List')
4543  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4544  >>> List.declare('nil')
4545  >>> List = List.create()
4546  >>> List.num_constructors()
4547  2
4548  >>> List.constructor(0)
4549  cons
4550  >>> num_accs = List.constructor(0).arity()
4551  >>> num_accs
4552  2
4553  >>> List.accessor(0, 0)
4554  car
4555  >>> List.accessor(0, 1)
4556  cdr
4557  >>> List.constructor(1)
4558  nil
4559  >>> num_accs = List.constructor(1).arity()
4560  >>> num_accs
4561  0
4562  """
4563  if __debug__:
4564  _z3_assert(i < self.num_constructors(), "Invalid constructor index")
4565  _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index")
4566  return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx)
4567 

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

4492  def constructor(self, idx):
4493  """Return a constructor of the datatype `self`.
4494 
4495  >>> List = Datatype('List')
4496  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4497  >>> List.declare('nil')
4498  >>> List = List.create()
4499  >>> # List is now a Z3 declaration
4500  >>> List.num_constructors()
4501  2
4502  >>> List.constructor(0)
4503  cons
4504  >>> List.constructor(1)
4505  nil
4506  """
4507  if __debug__:
4508  _z3_assert(idx < self.num_constructors(), "Invalid constructor index")
4509  return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx)
4510 

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

4479  def num_constructors(self):
4480  """Return the number of constructors in the given Z3 datatype.
4481 
4482  >>> List = Datatype('List')
4483  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4484  >>> List.declare('nil')
4485  >>> List = List.create()
4486  >>> # List is now a Z3 declaration
4487  >>> List.num_constructors()
4488  2
4489  """
4490  return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast))
4491 

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

4511  def recognizer(self, idx):
4512  """In Z3, each constructor has an associated recognizer predicate.
4513 
4514  If the constructor is named `name`, then the recognizer `is_name`.
4515 
4516  >>> List = Datatype('List')
4517  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
4518  >>> List.declare('nil')
4519  >>> List = List.create()
4520  >>> # List is now a Z3 declaration
4521  >>> List.num_constructors()
4522  2
4523  >>> List.recognizer(0)
4524  is_cons
4525  >>> List.recognizer(1)
4526  is_nil
4527  >>> simplify(List.is_nil(List.cons(10, List.nil)))
4528  False
4529  >>> simplify(List.is_cons(List.cons(10, List.nil)))
4530  True
4531  >>> l = Const('l', List)
4532  >>> simplify(List.is_cons(l))
4533  is_cons(l)
4534  """
4535  if __debug__:
4536  _z3_assert(idx < self.num_constructors(), "Invalid recognizer index")
4537  return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx)
4538