Z3
 
Loading...
Searching...
No Matches
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 __deepcopy__ (self, memo={})
 
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
 
- Protected Member Functions inherited from Z3PPObject
def _repr_html_ (self)
 

Detailed Description

Datatype sorts.

Definition at line 5254 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 5317 of file z3py.py.

5317 def accessor(self, i, j):
5318 """In Z3, each constructor has 0 or more accessor.
5319 The number of accessors is equal to the arity of the constructor.
5320
5321 >>> List = Datatype('List')
5322 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5323 >>> List.declare('nil')
5324 >>> List = List.create()
5325 >>> List.num_constructors()
5326 2
5327 >>> List.constructor(0)
5328 cons
5329 >>> num_accs = List.constructor(0).arity()
5330 >>> num_accs
5331 2
5332 >>> List.accessor(0, 0)
5333 car
5334 >>> List.accessor(0, 1)
5335 cdr
5336 >>> List.constructor(1)
5337 nil
5338 >>> num_accs = List.constructor(1).arity()
5339 >>> num_accs
5340 0
5341 """
5342 if z3_debug():
5343 _z3_assert(i < self.num_constructors(), "Invalid constructor index")
5344 _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index")
5345 return FuncDeclRef(
5346 Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j),
5347 ctx=self.ctx,
5348 )
5349
5350
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()

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

5270 def constructor(self, idx):
5271 """Return a constructor of the datatype `self`.
5272
5273 >>> List = Datatype('List')
5274 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5275 >>> List.declare('nil')
5276 >>> List = List.create()
5277 >>> # List is now a Z3 declaration
5278 >>> List.num_constructors()
5279 2
5280 >>> List.constructor(0)
5281 cons
5282 >>> List.constructor(1)
5283 nil
5284 """
5285 if z3_debug():
5286 _z3_assert(idx < self.num_constructors(), "Invalid constructor index")
5287 return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx)
5288
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th constructor.

Referenced by DatatypeSortRef.accessor().

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

5257 def num_constructors(self):
5258 """Return the number of constructors in the given Z3 datatype.
5259
5260 >>> List = Datatype('List')
5261 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5262 >>> List.declare('nil')
5263 >>> List = List.create()
5264 >>> # List is now a Z3 declaration
5265 >>> List.num_constructors()
5266 2
5267 """
5268 return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast))
5269
unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t)
Return number of constructors for datatype.

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

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

5289 def recognizer(self, idx):
5290 """In Z3, each constructor has an associated recognizer predicate.
5291
5292 If the constructor is named `name`, then the recognizer `is_name`.
5293
5294 >>> List = Datatype('List')
5295 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5296 >>> List.declare('nil')
5297 >>> List = List.create()
5298 >>> # List is now a Z3 declaration
5299 >>> List.num_constructors()
5300 2
5301 >>> List.recognizer(0)
5302 is(cons)
5303 >>> List.recognizer(1)
5304 is(nil)
5305 >>> simplify(List.is_nil(List.cons(10, List.nil)))
5306 False
5307 >>> simplify(List.is_cons(List.cons(10, List.nil)))
5308 True
5309 >>> l = Const('l', List)
5310 >>> simplify(List.is_cons(l))
5311 is(cons, l)
5312 """
5313 if z3_debug():
5314 _z3_assert(idx < self.num_constructors(), "Invalid recognizer index")
5315 return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx)
5316
Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th recognizer.