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

5398 def accessor(self, i, j):
5399 """In Z3, each constructor has 0 or more accessor.
5400 The number of accessors is equal to the arity of the constructor.
5401
5402 >>> List = Datatype('List')
5403 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5404 >>> List.declare('nil')
5405 >>> List = List.create()
5406 >>> List.num_constructors()
5407 2
5408 >>> List.constructor(0)
5409 cons
5410 >>> num_accs = List.constructor(0).arity()
5411 >>> num_accs
5412 2
5413 >>> List.accessor(0, 0)
5414 car
5415 >>> List.accessor(0, 1)
5416 cdr
5417 >>> List.constructor(1)
5418 nil
5419 >>> num_accs = List.constructor(1).arity()
5420 >>> num_accs
5421 0
5422 """
5423 if z3_debug():
5424 _z3_assert(i < self.num_constructors(), "Invalid constructor index")
5425 _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index")
5426 return FuncDeclRef(
5427 Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j),
5428 ctx=self.ctx,
5429 )
5430
5431
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 5351 of file z3py.py.

5351 def constructor(self, idx):
5352 """Return a constructor of the datatype `self`.
5353
5354 >>> List = Datatype('List')
5355 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5356 >>> List.declare('nil')
5357 >>> List = List.create()
5358 >>> # List is now a Z3 declaration
5359 >>> List.num_constructors()
5360 2
5361 >>> List.constructor(0)
5362 cons
5363 >>> List.constructor(1)
5364 nil
5365 """
5366 if z3_debug():
5367 _z3_assert(idx < self.num_constructors(), "Invalid constructor index")
5368 return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx)
5369
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 5338 of file z3py.py.

5338 def num_constructors(self):
5339 """Return the number of constructors in the given Z3 datatype.
5340
5341 >>> List = Datatype('List')
5342 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5343 >>> List.declare('nil')
5344 >>> List = List.create()
5345 >>> # List is now a Z3 declaration
5346 >>> List.num_constructors()
5347 2
5348 """
5349 return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast))
5350
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 5370 of file z3py.py.

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