|
def | num_constructors (self) |
|
def | constructor (self, idx) |
|
def | recognizer (self, idx) |
|
def | accessor (self, i, j) |
|
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) |
|
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) |
|
def | use_pp (self) |
|
Datatype sorts.
Definition at line 4834 of file z3py.py.
◆ 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 4896 of file z3py.py.
4896 def accessor(self, i, j):
4897 """In Z3, each constructor has 0 or more accessor. The number of accessors is equal to the arity of the constructor. 4899 >>> List = Datatype('List') 4900 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4901 >>> List.declare('nil') 4902 >>> List = List.create() 4903 >>> List.num_constructors() 4905 >>> List.constructor(0) 4907 >>> num_accs = List.constructor(0).arity() 4910 >>> List.accessor(0, 0) 4912 >>> List.accessor(0, 1) 4914 >>> List.constructor(1) 4916 >>> num_accs = List.constructor(1).arity() 4921 _z3_assert(i < self.num_constructors(),
"Invalid constructor index")
4922 _z3_assert(j < self.constructor(i).arity(),
"Invalid accessor index")
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 4849 of file z3py.py.
4849 def constructor(self, idx):
4850 """Return a constructor of the datatype `self`. 4852 >>> List = Datatype('List') 4853 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4854 >>> List.declare('nil') 4855 >>> List = List.create() 4856 >>> # List is now a Z3 declaration 4857 >>> List.num_constructors() 4859 >>> List.constructor(0) 4861 >>> List.constructor(1) 4865 _z3_assert(idx < self.num_constructors(),
"Invalid constructor index")
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th constructor.
◆ 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 4836 of file z3py.py.
4836 def num_constructors(self):
4837 """Return the number of constructors in the given Z3 datatype. 4839 >>> List = Datatype('List') 4840 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4841 >>> List.declare('nil') 4842 >>> List = List.create() 4843 >>> # List is now a Z3 declaration 4844 >>> List.num_constructors() unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t)
Return number of constructors for datatype.
◆ 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 4868 of file z3py.py.
4868 def recognizer(self, idx):
4869 """In Z3, each constructor has an associated recognizer predicate. 4871 If the constructor is named `name`, then the recognizer `is_name`. 4873 >>> List = Datatype('List') 4874 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4875 >>> List.declare('nil') 4876 >>> List = List.create() 4877 >>> # List is now a Z3 declaration 4878 >>> List.num_constructors() 4880 >>> List.recognizer(0) 4882 >>> List.recognizer(1) 4884 >>> simplify(List.is_nil(List.cons(10, List.nil))) 4886 >>> simplify(List.is_cons(List.cons(10, List.nil))) 4888 >>> l = Const('l', List) 4889 >>> simplify(List.is_cons(l)) 4893 _z3_assert(idx < self.num_constructors(),
"Invalid recognizer index")
Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th recognizer.