Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions
DatatypeSortRef Class Reference
+ Inheritance diagram for DatatypeSortRef:

Public Member Functions

def num_constructors
def constructor
def recognizer
def accessor

Detailed Description

Datatype sorts.

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

04363 
04364     def accessor(self, i, j):
04365         """In Z3, each constructor has 0 or more accessor. The number of accessors is equal to the arity of the constructor.
04366         
04367         >>> List = Datatype('List')
04368         >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
04369         >>> List.declare('nil')
04370         >>> List = List.create()
04371         >>> List.num_constructors()
04372         2
04373         >>> List.constructor(0)
04374         cons
04375         >>> num_accs = List.constructor(0).arity()
04376         >>> num_accs
04377         2
04378         >>> List.accessor(0, 0)
04379         car
04380         >>> List.accessor(0, 1)
04381         cdr
04382         >>> List.constructor(1)
04383         nil
04384         >>> num_accs = List.constructor(1).arity()
04385         >>> num_accs
04386         0
04387         """
04388         if __debug__:
04389             _z3_assert(i < self.num_constructors(), "Invalid constructor index")
04390             _z3_assert(j < self.constructor(i).arity(), "Invalid accessor index")
04391         return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx)

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

Referenced by DatatypeSortRef.accessor().

04316 
04317     def constructor(self, idx):
04318         """Return a constructor of the datatype `self`.
04319 
04320         >>> List = Datatype('List')
04321         >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
04322         >>> List.declare('nil')
04323         >>> List = List.create()
04324         >>> # List is now a Z3 declaration
04325         >>> List.num_constructors()
04326         2
04327         >>> List.constructor(0)
04328         cons
04329         >>> List.constructor(1)
04330         nil
04331         """
04332         if __debug__:
04333             _z3_assert(idx < self.num_constructors(), "Invalid constructor index")
04334         return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx)
    
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 4303 of file z3py.py.

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

04303 
04304     def num_constructors(self):
04305         """Return the number of constructors in the given Z3 datatype. 
04306         
04307         >>> List = Datatype('List')
04308         >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
04309         >>> List.declare('nil')
04310         >>> List = List.create()
04311         >>> # List is now a Z3 declaration
04312         >>> List.num_constructors()
04313         2
04314         """
04315         return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast))

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

04335 
04336     def recognizer(self, idx):
04337         """In Z3, each constructor has an associated recognizer predicate. 
04338 
04339         If the constructor is named `name`, then the recognizer `is_name`.
04340         
04341         >>> List = Datatype('List')
04342         >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
04343         >>> List.declare('nil')
04344         >>> List = List.create()
04345         >>> # List is now a Z3 declaration
04346         >>> List.num_constructors()
04347         2
04348         >>> List.recognizer(0)
04349         is_cons
04350         >>> List.recognizer(1)
04351         is_nil
04352         >>> simplify(List.is_nil(List.cons(10, List.nil)))
04353         False
04354         >>> simplify(List.is_cons(List.cons(10, List.nil)))
04355         True
04356         >>> l = Const('l', List)
04357         >>> simplify(List.is_cons(l))
04358         is_cons(l)
04359         """
04360         if __debug__:
04361             _z3_assert(idx < self.num_constructors(), "Invalid recognizer index")
04362         return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx)

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines