Public Member Functions | |
def | num_constructors |
def | constructor |
def | recognizer |
def | 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 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)