Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Data Fields
BitVecSortRef Class Reference

Bit-Vectors. More...

+ Inheritance diagram for BitVecSortRef:

Public Member Functions

def size
def subsort
def cast

Data Fields

 ctx

Detailed Description

Bit-Vectors.

Bit-vector sort.

Definition at line 2897 of file z3py.py.


Member Function Documentation

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 
)
Return `True` if `self` is a subsort of `other`. 

>>> IntSort().subsort(RealSort())
True

Reimplemented from SortRef.

Definition at line 2909 of file z3py.py.

02909 
02910     def subsort(self, other):
02911         return is_bv_sort(other) and self.size() < other.size()


Field Documentation

ctx

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().

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines