Z3
 
Loading...
Searching...
No Matches
DatatypeSortRef Class Reference
+ Inheritance diagram for DatatypeSortRef:

Public Member Functions

 num_constructors (self)
 
 constructor (self, idx)
 
 recognizer (self, idx)
 
 accessor (self, i, j)
 
- Public Member Functions inherited from SortRef
 as_ast (self)
 
 get_id (self)
 
 kind (self)
 
 subsort (self, other)
 
 cast (self, val)
 
 name (self)
 
 __eq__ (self, other)
 
 __ne__ (self, other)
 
 __hash__ (self)
 
- Public Member Functions inherited from AstRef
 __init__ (self, ast, ctx=None)
 
 __del__ (self)
 
 __deepcopy__ (self, memo={})
 
 __str__ (self)
 
 __repr__ (self)
 
 __eq__ (self, other)
 
 __hash__ (self)
 
 __nonzero__ (self)
 
 __bool__ (self)
 
 sexpr (self)
 
 ctx_ref (self)
 
 eq (self, other)
 
 translate (self, target)
 
 __copy__ (self)
 
 hash (self)
 
 py_value (self)
 
- Public Member Functions inherited from Z3PPObject
 use_pp (self)
 

Additional Inherited Members

- Data Fields inherited from AstRef
 ast = ast
 
 ctx = _get_ctx(ctx)
 
- Protected Member Functions inherited from Z3PPObject
 _repr_html_ (self)
 

Detailed Description

Datatype sorts.

Definition at line 5344 of file z3py.py.

Member Function Documentation

◆ accessor()

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

5407 def accessor(self, i, j):
5408 """In Z3, each constructor has 0 or more accessor.
5409 The number of accessors is equal to the arity of the constructor.
5410
5411 >>> List = Datatype('List')
5412 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5413 >>> List.declare('nil')
5414 >>> List = List.create()
5415 >>> List.num_constructors()
5416 2
5417 >>> List.constructor(0)
5418 cons
5419 >>> num_accs = List.constructor(0).arity()
5420 >>> num_accs
5421 2
5422 >>> List.accessor(0, 0)
5423 car
5424 >>> List.accessor(0, 1)
5425 cdr
5426 >>> List.constructor(1)
5427 nil
5428 >>> num_accs = List.constructor(1).arity()
5429 >>> num_accs
5430 0
5431 """
5432 if z3_debug():
5433 _z3_assert(i < self.num_constructors(), "Invalid constructor index")
5434 _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index")
5435 return FuncDeclRef(
5436 Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j),
5437 ctx=self.ctx,
5438 )
5439
5440
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.

◆ constructor()

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

5360 def constructor(self, idx):
5361 """Return a constructor of the datatype `self`.
5362
5363 >>> List = Datatype('List')
5364 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5365 >>> List.declare('nil')
5366 >>> List = List.create()
5367 >>> # List is now a Z3 declaration
5368 >>> List.num_constructors()
5369 2
5370 >>> List.constructor(0)
5371 cons
5372 >>> List.constructor(1)
5373 nil
5374 """
5375 if z3_debug():
5376 _z3_assert(idx < self.num_constructors(), "Invalid constructor index")
5377 return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx)
5378
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th constructor.

Referenced by accessor().

◆ num_constructors()

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

5347 def num_constructors(self):
5348 """Return the number of constructors in the given Z3 datatype.
5349
5350 >>> List = Datatype('List')
5351 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5352 >>> List.declare('nil')
5353 >>> List = List.create()
5354 >>> # List is now a Z3 declaration
5355 >>> List.num_constructors()
5356 2
5357 """
5358 return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast))
5359
unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t)
Return number of constructors for datatype.

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

◆ recognizer()

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

5379 def recognizer(self, idx):
5380 """In Z3, each constructor has an associated recognizer predicate.
5381
5382 If the constructor is named `name`, then the recognizer `is_name`.
5383
5384 >>> List = Datatype('List')
5385 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5386 >>> List.declare('nil')
5387 >>> List = List.create()
5388 >>> # List is now a Z3 declaration
5389 >>> List.num_constructors()
5390 2
5391 >>> List.recognizer(0)
5392 is(cons)
5393 >>> List.recognizer(1)
5394 is(nil)
5395 >>> simplify(List.is_nil(List.cons(10, List.nil)))
5396 False
5397 >>> simplify(List.is_cons(List.cons(10, List.nil)))
5398 True
5399 >>> l = Const('l', List)
5400 >>> simplify(List.is_cons(l))
5401 is(cons, l)
5402 """
5403 if z3_debug():
5404 _z3_assert(idx < self.num_constructors(), "Invalid recognizer index")
5405 return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx)
5406
Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th recognizer.