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)
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__ (self)
 
def __str__ (self)
 
def __repr__ (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 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.

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

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

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

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