|
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 4828 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 4890 of file z3py.py.
4890 def accessor(self, i, j):
4891 """In Z3, each constructor has 0 or more accessor. The number of accessors is equal to the arity of the constructor. 4893 >>> List = Datatype('List') 4894 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4895 >>> List.declare('nil') 4896 >>> List = List.create() 4897 >>> List.num_constructors() 4899 >>> List.constructor(0) 4901 >>> num_accs = List.constructor(0).arity() 4904 >>> List.accessor(0, 0) 4906 >>> List.accessor(0, 1) 4908 >>> List.constructor(1) 4910 >>> num_accs = List.constructor(1).arity() 4915 _z3_assert(i < self.num_constructors(),
"Invalid constructor index")
4916 _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 4843 of file z3py.py.
4843 def constructor(self, idx):
4844 """Return a constructor of the datatype `self`. 4846 >>> List = Datatype('List') 4847 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4848 >>> List.declare('nil') 4849 >>> List = List.create() 4850 >>> # List is now a Z3 declaration 4851 >>> List.num_constructors() 4853 >>> List.constructor(0) 4855 >>> List.constructor(1) 4859 _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 4830 of file z3py.py.
4830 def num_constructors(self):
4831 """Return the number of constructors in the given Z3 datatype. 4833 >>> List = Datatype('List') 4834 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4835 >>> List.declare('nil') 4836 >>> List = List.create() 4837 >>> # List is now a Z3 declaration 4838 >>> 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 4862 of file z3py.py.
4862 def recognizer(self, idx):
4863 """In Z3, each constructor has an associated recognizer predicate. 4865 If the constructor is named `name`, then the recognizer `is_name`. 4867 >>> List = Datatype('List') 4868 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4869 >>> List.declare('nil') 4870 >>> List = List.create() 4871 >>> # List is now a Z3 declaration 4872 >>> List.num_constructors() 4874 >>> List.recognizer(0) 4876 >>> List.recognizer(1) 4878 >>> simplify(List.is_nil(List.cons(10, List.nil))) 4880 >>> simplify(List.is_cons(List.cons(10, List.nil))) 4882 >>> l = Const('l', List) 4883 >>> simplify(List.is_cons(l)) 4887 _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.