Bit-Vectors. More...
Public Member Functions | |
def | size |
def | subsort |
def | cast |
Data Fields | |
ctx |
def cast | ( | self, | |
val | |||
) |
Try to cast `val` as a Bit-Vector. >>> b = BitVecSort(32) >>> b.cast(10) 10 >>> b.cast(10).sexpr() '#x0000000a'
Reimplemented from SortRef.
Definition at line 2912 of file z3py.py.
02912 02913 def cast(self, val): 02914 """Try to cast `val` as a Bit-Vector. 02915 02916 >>> b = BitVecSort(32) 02917 >>> b.cast(10) 02918 10 02919 >>> b.cast(10).sexpr() 02920 '#x0000000a' 02921 """ 02922 if is_expr(val): 02923 if __debug__: 02924 _z3_assert(self.ctx == val.ctx, "Context mismatch") 02925 # Idea: use sign_extend if sort of val is a bitvector of smaller size 02926 return val 02927 else: 02928 return BitVecVal(val, self)
def size | ( | self | ) |
Return the size (number of bits) of the bit-vector sort `self`. >>> b = BitVecSort(32) >>> b.size() 32
Definition at line 2900 of file z3py.py.
02900 02901 def size(self): 02902 """Return the size (number of bits) of the bit-vector sort `self`. 02903 02904 >>> b = BitVecSort(32) 02905 >>> b.size() 02906 32 02907 """ 02908 return int(Z3_get_bv_sort_size(self.ctx_ref(), self.ast))
def subsort | ( | self, | |
other | |||
) |
Reimplemented from AstRef.
Definition at line 2919 of file z3py.py.
Referenced by ArithRef::__add__(), FuncDeclRef::__call__(), ArithRef::__div__(), ExprRef::__eq__(), Probe::__eq__(), ArithRef::__ge__(), Probe::__ge__(), ApplyResult::__getitem__(), ArithRef::__gt__(), Probe::__gt__(), ArithRef::__le__(), Probe::__le__(), ArithRef::__lt__(), Probe::__lt__(), ArithRef::__mod__(), ArithRef::__mul__(), ExprRef::__ne__(), Probe::__ne__(), ArithRef::__neg__(), ArithRef::__pow__(), ArithRef::__radd__(), ArithRef::__rdiv__(), ArithRef::__rmod__(), ArithRef::__rmul__(), ArithRef::__rpow__(), ArithRef::__rsub__(), ArithRef::__sub__(), 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(), 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(), Fixedpoint::set(), Tactic::solver(), ExprRef::sort(), BoolRef::sort(), QuantifierRef::sort(), ArithRef::sort(), Fixedpoint::statistics(), Solver::to_smt2(), Fixedpoint::update_rule(), QuantifierRef::var_name(), and QuantifierRef::var_sort().