|
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 4593 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 4655 of file z3py.py.
4655 def accessor(self, i, j):
4656 """In Z3, each constructor has 0 or more accessor. The number of accessors is equal to the arity of the constructor. 4658 >>> List = Datatype('List') 4659 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4660 >>> List.declare('nil') 4661 >>> List = List.create() 4662 >>> List.num_constructors() 4664 >>> List.constructor(0) 4666 >>> num_accs = List.constructor(0).arity() 4669 >>> List.accessor(0, 0) 4671 >>> List.accessor(0, 1) 4673 >>> List.constructor(1) 4675 >>> num_accs = List.constructor(1).arity() 4680 _z3_assert(i < self.num_constructors(),
"Invalid constructor index")
4681 _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 4608 of file z3py.py.
4608 def constructor(self, idx):
4609 """Return a constructor of the datatype `self`. 4611 >>> List = Datatype('List') 4612 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4613 >>> List.declare('nil') 4614 >>> List = List.create() 4615 >>> # List is now a Z3 declaration 4616 >>> List.num_constructors() 4618 >>> List.constructor(0) 4620 >>> List.constructor(1) 4624 _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 4595 of file z3py.py.
4595 def num_constructors(self):
4596 """Return the number of constructors in the given Z3 datatype. 4598 >>> List = Datatype('List') 4599 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4600 >>> List.declare('nil') 4601 >>> List = List.create() 4602 >>> # List is now a Z3 declaration 4603 >>> 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 4627 of file z3py.py.
4627 def recognizer(self, idx):
4628 """In Z3, each constructor has an associated recognizer predicate. 4630 If the constructor is named `name`, then the recognizer `is_name`. 4632 >>> List = Datatype('List') 4633 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4634 >>> List.declare('nil') 4635 >>> List = List.create() 4636 >>> # List is now a Z3 declaration 4637 >>> List.num_constructors() 4639 >>> List.recognizer(0) 4641 >>> List.recognizer(1) 4643 >>> simplify(List.is_nil(List.cons(10, List.nil))) 4645 >>> simplify(List.is_cons(List.cons(10, List.nil))) 4647 >>> l = Const('l', List) 4648 >>> simplify(List.is_cons(l)) 4652 _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.