|
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 | __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 | hash (self) |
|
def | use_pp (self) |
|
Datatype sorts.
Definition at line 4477 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 4539 of file z3py.py.
4539 def accessor(self, i, j):
4540 """In Z3, each constructor has 0 or more accessor. The number of accessors is equal to the arity of the constructor. 4542 >>> List = Datatype('List') 4543 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4544 >>> List.declare('nil') 4545 >>> List = List.create() 4546 >>> List.num_constructors() 4548 >>> List.constructor(0) 4550 >>> num_accs = List.constructor(0).arity() 4553 >>> List.accessor(0, 0) 4555 >>> List.accessor(0, 1) 4557 >>> List.constructor(1) 4559 >>> num_accs = List.constructor(1).arity() 4564 _z3_assert(i < self.num_constructors(),
"Invalid constructor index")
4565 _z3_assert(j < self.constructor(i).arity(),
"Invalid accessor index")
4566 return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx)
§ 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 4492 of file z3py.py.
4492 def constructor(self, idx):
4493 """Return a constructor of the datatype `self`. 4495 >>> List = Datatype('List') 4496 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4497 >>> List.declare('nil') 4498 >>> List = List.create() 4499 >>> # List is now a Z3 declaration 4500 >>> List.num_constructors() 4502 >>> List.constructor(0) 4504 >>> List.constructor(1) 4508 _z3_assert(idx < self.num_constructors(),
"Invalid constructor index")
4509 return FuncDeclRef(Z3_get_datatype_sort_constructor(self.ctx_ref(), self.ast, idx), self.ctx)
§ 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 4479 of file z3py.py.
4479 def num_constructors(self):
4480 """Return the number of constructors in the given Z3 datatype. 4482 >>> List = Datatype('List') 4483 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4484 >>> List.declare('nil') 4485 >>> List = List.create() 4486 >>> # List is now a Z3 declaration 4487 >>> List.num_constructors() 4490 return int(Z3_get_datatype_sort_num_constructors(self.ctx_ref(), self.ast))
§ 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 4511 of file z3py.py.
4511 def recognizer(self, idx):
4512 """In Z3, each constructor has an associated recognizer predicate. 4514 If the constructor is named `name`, then the recognizer `is_name`. 4516 >>> List = Datatype('List') 4517 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 4518 >>> List.declare('nil') 4519 >>> List = List.create() 4520 >>> # List is now a Z3 declaration 4521 >>> List.num_constructors() 4523 >>> List.recognizer(0) 4525 >>> List.recognizer(1) 4527 >>> simplify(List.is_nil(List.cons(10, List.nil))) 4529 >>> simplify(List.is_cons(List.cons(10, List.nil))) 4531 >>> l = Const('l', List) 4532 >>> simplify(List.is_cons(l)) 4536 _z3_assert(idx < self.num_constructors(),
"Invalid recognizer index")
4537 return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx)