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__ (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

## Detailed Description

    Datatype sorts.

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

5251 def accessor(self, i, j):
5252 """In Z3, each constructor has 0 or more accessor.
5253 The number of accessors is equal to the arity of the constructor.
5254
5255 >>> List = Datatype('List')
5256 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5257 >>> List.declare('nil')
5258 >>> List = List.create()
5259 >>> List.num_constructors()
5260 2
5261 >>> List.constructor(0)
5262 cons
5263 >>> num_accs = List.constructor(0).arity()
5264 >>> num_accs
5265 2
5266 >>> List.accessor(0, 0)
5267 car
5268 >>> List.accessor(0, 1)
5269 cdr
5270 >>> List.constructor(1)
5271 nil
5272 >>> num_accs = List.constructor(1).arity()
5273 >>> num_accs
5274 0
5275 """
5276 if z3_debug():
5277 _z3_assert(i < self.num_constructors(), "Invalid constructor index")
5278 _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index")
5279 return FuncDeclRef(
5280 Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j),
5281 ctx=self.ctx,
5282 )
5283
5284
z3py.z3_debug
def z3_debug()
Definition: z3py.py:64
z3py.IntSort
def IntSort(ctx=None)
Definition: z3py.py:3100
Z3_get_datatype_sort_constructor_accessor
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 5204 of file z3py.py.

5204 def constructor(self, idx):
5205 """Return a constructor of the datatype `self`.
5206
5207 >>> List = Datatype('List')
5208 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5209 >>> List.declare('nil')
5210 >>> List = List.create()
5211 >>> # List is now a Z3 declaration
5212 >>> List.num_constructors()
5213 2
5214 >>> List.constructor(0)
5215 cons
5216 >>> List.constructor(1)
5217 nil
5218 """
5219 if z3_debug():
5220 _z3_assert(idx < self.num_constructors(), "Invalid constructor index")
5221 return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx)
5222
Z3_get_datatype_sort_constructor
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 5191 of file z3py.py.

5191 def num_constructors(self):
5192 """Return the number of constructors in the given Z3 datatype.
5193
5194 >>> List = Datatype('List')
5195 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5196 >>> List.declare('nil')
5197 >>> List = List.create()
5198 >>> # List is now a Z3 declaration
5199 >>> List.num_constructors()
5200 2
5201 """
5202 return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast))
5203
Z3_get_datatype_sort_num_constructors
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 5223 of file z3py.py.

5223 def recognizer(self, idx):
5224 """In Z3, each constructor has an associated recognizer predicate.
5225
5226 If the constructor is named `name`, then the recognizer `is_name`.
5227
5228 >>> List = Datatype('List')
5229 >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
5230 >>> List.declare('nil')
5231 >>> List = List.create()
5232 >>> # List is now a Z3 declaration
5233 >>> List.num_constructors()
5234 2
5235 >>> List.recognizer(0)
5236 is(cons)
5237 >>> List.recognizer(1)
5238 is(nil)
5239 >>> simplify(List.is_nil(List.cons(10, List.nil)))
5240 False
5241 >>> simplify(List.is_cons(List.cons(10, List.nil)))
5242 True
5243 >>> l = Const('l', List)
5244 >>> simplify(List.is_cons(l))
5245 is(cons, l)
5246 """
5247 if z3_debug():
5248 _z3_assert(idx < self.num_constructors(), "Invalid recognizer index")
5249 return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx)
5250
z3py.simplify
def simplify(a, *arguments, **keywords)
Utils.
Definition: z3py.py:8645
z3py.Const
def Const(name, sort)
Definition: z3py.py:1405
Z3_get_datatype_sort_recognizer
Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th recognizer.