Public Member Functions | |
def | __init__ (self, name, ctx=None) |
def | declare_core (self, name, rec_name, args) |
def | declare (self, name, args) |
def | __repr__ (self) |
def | create (self) |
Data Fields | |
ctx | |
name | |
constructors | |
Helper class for declaring Z3 datatypes. >>> List = Datatype('List') >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) >>> List.declare('nil') >>> List = List.create() >>> # List is now a Z3 declaration >>> List.nil nil >>> List.cons(10, List.nil) cons(10, nil) >>> List.cons(10, List.nil).sort() List >>> cons = List.cons >>> nil = List.nil >>> car = List.car >>> cdr = List.cdr >>> n = cons(1, cons(0, nil)) >>> n cons(1, cons(0, nil)) >>> simplify(cdr(n)) cons(0, nil) >>> simplify(car(n)) 1
def create | ( | self | ) |
Create a Z3 datatype based on the constructors declared using the mehtod `declare()`. The function `CreateDatatypes()` must be used to define mutually recursive datatypes. >>> List = Datatype('List') >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) >>> List.declare('nil') >>> List = List.create() >>> List.nil nil >>> List.cons(10, List.nil) cons(10, nil)
Definition at line 4237 of file z3py.py.
Referenced by Datatype.declare().
def declare | ( | self, | |
name, | |||
args | |||
) |
Declare constructor named `name` with the given accessors `args`. Each accessor is a pair `(name, sort)`, where `name` is a string and `sort` a Z3 sort or a reference to the datatypes being declared. In the followin example `List.declare('cons', ('car', IntSort()), ('cdr', List))` declares the constructor named `cons` that builds a new List using an integer and a List. It also declares the accessors `car` and `cdr`. The accessor `car` extracts the integer of a `cons` cell, and `cdr` the list of a `cons` cell. After all constructors were declared, we use the method create() to create the actual datatype in Z3. >>> List = Datatype('List') >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) >>> List.declare('nil') >>> List = List.create()
Definition at line 4214 of file z3py.py.
Referenced by Datatype.create().
def declare_core | ( | self, | |
name, | |||
rec_name, | |||
args | |||
) |
Definition at line 4207 of file z3py.py.
Referenced by Datatype.declare().
constructors |
Definition at line 4205 of file z3py.py.
Referenced by Datatype.__repr__().
ctx |
Definition at line 4203 of file z3py.py.
Referenced by Probe.__eq__(), Probe.__ge__(), AstVector.__getitem__(), AstMap.__getitem__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), ApplyResult.convert_model(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), AstMap.keys(), Optimize.model(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.query(), Fixedpoint.set(), Optimize.set(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), and Fixedpoint.update_rule().
name |
Definition at line 4204 of file z3py.py.
Referenced by Datatype.__repr__().