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__
 
def __del__ (self)
 
def __deepcopy__
 
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 __copy__ (self)
 
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 5246 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 5309 of file z3py.py.

5309  def accessor(self, i, j):
5310  """In Z3, each constructor has 0 or more accessor.
5311  The number of accessors is equal to the arity of the constructor.
5312 
5313  >>> List = Datatype('List')
5314  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5315  >>> List.declare('nil')
5316  >>> List = List.create()
5317  >>> List.num_constructors()
5318  2
5319  >>> List.constructor(0)
5320  cons
5321  >>> num_accs = List.constructor(0).arity()
5322  >>> num_accs
5323  2
5324  >>> List.accessor(0, 0)
5325  car
5326  >>> List.accessor(0, 1)
5327  cdr
5328  >>> List.constructor(1)
5329  nil
5330  >>> num_accs = List.constructor(1).arity()
5331  >>> num_accs
5332  0
5333  """
5334  if z3_debug():
5335  _z3_assert(i < self.num_constructors(), "Invalid constructor index")
5336  _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index")
5337  return FuncDeclRef(
5339  ctx=self.ctx,
5340  )
5341 
5342 
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:718
def accessor(self, i, j)
Definition: z3py.py:5309
def num_constructors(self)
Definition: z3py.py:5249
def z3_debug()
Definition: z3py.py:62
def constructor(self, idx)
Definition: z3py.py:5262
def ctx_ref(self)
Definition: z3py.py:400
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 5262 of file z3py.py.

Referenced by DatatypeSortRef.accessor().

5262  def constructor(self, idx):
5263  """Return a constructor of the datatype `self`.
5264 
5265  >>> List = Datatype('List')
5266  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5267  >>> List.declare('nil')
5268  >>> List = List.create()
5269  >>> # List is now a Z3 declaration
5270  >>> List.num_constructors()
5271  2
5272  >>> List.constructor(0)
5273  cons
5274  >>> List.constructor(1)
5275  nil
5276  """
5277  if z3_debug():
5278  _z3_assert(idx < self.num_constructors(), "Invalid constructor index")
5279  return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx)
5280 
Function Declarations.
Definition: z3py.py:718
def num_constructors(self)
Definition: z3py.py:5249
def z3_debug()
Definition: z3py.py:62
def constructor(self, idx)
Definition: z3py.py:5262
def ctx_ref(self)
Definition: z3py.py:400
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 5249 of file z3py.py.

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

5249  def num_constructors(self):
5250  """Return the number of constructors in the given Z3 datatype.
5251 
5252  >>> List = Datatype('List')
5253  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5254  >>> List.declare('nil')
5255  >>> List = List.create()
5256  >>> # List is now a Z3 declaration
5257  >>> List.num_constructors()
5258  2
5259  """
5260  return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast))
5261 
def num_constructors(self)
Definition: z3py.py:5249
unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t)
Return number of constructors for datatype.
def ctx_ref(self)
Definition: z3py.py:400
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 5281 of file z3py.py.

5281  def recognizer(self, idx):
5282  """In Z3, each constructor has an associated recognizer predicate.
5283 
5284  If the constructor is named `name`, then the recognizer `is_name`.
5285 
5286  >>> List = Datatype('List')
5287  >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5288  >>> List.declare('nil')
5289  >>> List = List.create()
5290  >>> # List is now a Z3 declaration
5291  >>> List.num_constructors()
5292  2
5293  >>> List.recognizer(0)
5294  is(cons)
5295  >>> List.recognizer(1)
5296  is(nil)
5297  >>> simplify(List.is_nil(List.cons(10, List.nil)))
5298  False
5299  >>> simplify(List.is_cons(List.cons(10, List.nil)))
5300  True
5301  >>> l = Const('l', List)
5302  >>> simplify(List.is_cons(l))
5303  is(cons, l)
5304  """
5305  if z3_debug():
5306  _z3_assert(idx < self.num_constructors(), "Invalid recognizer index")
5307  return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx)
5308 
Function Declarations.
Definition: z3py.py:718
Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th recognizer.
def num_constructors(self)
Definition: z3py.py:5249
def z3_debug()
Definition: z3py.py:62
def ctx_ref(self)
Definition: z3py.py:400
def recognizer(self, idx)
Definition: z3py.py:5281