Public Member Functions | |
def | __init__ |
def | declare_core |
def | declare |
def | __repr__ |
def | create |
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 __init__ | ( | self, | |
name, | |||
ctx = None |
|||
) |
def __repr__ | ( | self | ) |
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 4177 of file z3py.py.
Referenced by Datatype.declare().
04177 04178 def create(self): 04179 """Create a Z3 datatype based on the constructors declared using the mehtod `declare()`. 04180 04181 The function `CreateDatatypes()` must be used to define mutually recursive datatypes. 04182 04183 >>> List = Datatype('List') 04184 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 04185 >>> List.declare('nil') 04186 >>> List = List.create() 04187 >>> List.nil 04188 nil 04189 >>> List.cons(10, List.nil) 04190 cons(10, nil) 04191 """ 04192 return CreateDatatypes([self])[0]
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 4154 of file z3py.py.
Referenced by Datatype.create().
04154 04155 def declare(self, name, *args): 04156 """Declare constructor named `name` with the given accessors `args`. 04157 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. 04158 04159 In the followin example `List.declare('cons', ('car', IntSort()), ('cdr', List))` 04160 declares the constructor named `cons` that builds a new List using an integer and a List. 04161 It also declares the accessors `car` and `cdr`. The accessor `car` extracts the integer of a `cons` cell, 04162 and `cdr` the list of a `cons` cell. After all constructors were declared, we use the method create() to create 04163 the actual datatype in Z3. 04164 04165 >>> List = Datatype('List') 04166 >>> List.declare('cons', ('car', IntSort()), ('cdr', List)) 04167 >>> List.declare('nil') 04168 >>> List = List.create() 04169 """ 04170 if __debug__: 04171 _z3_assert(isinstance(name, str), "String expected") 04172 _z3_assert(name != "", "Constructor name cannot be empty") 04173 return self.declare_core(name, "is_" + name, *args)
def declare_core | ( | self, | |
name, | |||
rec_name, | |||
args | |||
) |
Definition at line 4147 of file z3py.py.
Referenced by Datatype.declare().
04147 04148 def declare_core(self, name, rec_name, *args): 04149 if __debug__: 04150 _z3_assert(isinstance(name, str), "String expected") 04151 _z3_assert(isinstance(rec_name, str), "String expected") 04152 _z3_assert(all([_valid_accessor(a) for a in args]), "Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)") 04153 self.constructors.append((name, rec_name, args))
Definition at line 4142 of file z3py.py.
Referenced by Datatype.__repr__().
Definition at line 4142 of file z3py.py.
Referenced by ArithRef::__add__(), BitVecRef::__add__(), BitVecRef::__and__(), FuncDeclRef::__call__(), ArithRef::__div__(), BitVecRef::__div__(), ExprRef::__eq__(), Probe::__eq__(), ArithRef::__ge__(), BitVecRef::__ge__(), Probe::__ge__(), ArrayRef::__getitem__(), ApplyResult::__getitem__(), ArithRef::__gt__(), BitVecRef::__gt__(), Probe::__gt__(), BitVecRef::__invert__(), ArithRef::__le__(), BitVecRef::__le__(), Probe::__le__(), BitVecRef::__lshift__(), ArithRef::__lt__(), BitVecRef::__lt__(), Probe::__lt__(), ArithRef::__mod__(), BitVecRef::__mod__(), ArithRef::__mul__(), BitVecRef::__mul__(), ExprRef::__ne__(), Probe::__ne__(), ArithRef::__neg__(), BitVecRef::__neg__(), BitVecRef::__or__(), ArithRef::__pow__(), ArithRef::__radd__(), BitVecRef::__radd__(), BitVecRef::__rand__(), ArithRef::__rdiv__(), BitVecRef::__rdiv__(), BitVecRef::__rlshift__(), ArithRef::__rmod__(), BitVecRef::__rmod__(), ArithRef::__rmul__(), BitVecRef::__rmul__(), BitVecRef::__ror__(), ArithRef::__rpow__(), BitVecRef::__rrshift__(), BitVecRef::__rshift__(), ArithRef::__rsub__(), BitVecRef::__rsub__(), BitVecRef::__rxor__(), ArithRef::__sub__(), BitVecRef::__sub__(), BitVecRef::__xor__(), Fixedpoint::add_rule(), Tactic::apply(), AlgebraicNumRef::approx(), ExprRef::arg(), ApplyResult::as_expr(), Fixedpoint::assert_exprs(), QuantifierRef::body(), BoolSortRef::cast(), ApplyResult::convert_model(), ExprRef::decl(), RatNumRef::denominator(), FuncDeclRef::domain(), ArraySortRef::domain(), Fixedpoint::get_answer(), Fixedpoint::get_assertions(), Fixedpoint::get_cover_delta(), Fixedpoint::get_rules(), SortRef::kind(), SortRef::name(), FuncDeclRef::name(), QuantifierRef::no_pattern(), RatNumRef::numerator(), Fixedpoint::param_descrs(), Tactic::param_descrs(), Fixedpoint::parse_file(), Fixedpoint::parse_string(), QuantifierRef::pattern(), FuncDeclRef::range(), ArraySortRef::range(), Fixedpoint::set(), Tactic::solver(), ExprRef::sort(), BoolRef::sort(), QuantifierRef::sort(), ArithRef::sort(), BitVecRef::sort(), ArrayRef::sort(), Fixedpoint::statistics(), Solver::to_smt2(), Fixedpoint::update_rule(), QuantifierRef::var_name(), and QuantifierRef::var_sort().
Definition at line 4142 of file z3py.py.
Referenced by Datatype.__repr__().