Arithmetic. More...
Public Member Functions | |
def | is_real |
def | is_int |
def | subsort |
def | cast |
Data Fields | |
ctx |
def cast | ( | self, | |
val | |||
) |
Try to cast `val` as an Integer or Real. >>> IntSort().cast(10) 10 >>> is_int(IntSort().cast(10)) True >>> is_int(10) False >>> RealSort().cast(10) 10 >>> is_real(RealSort().cast(10)) True
Reimplemented from SortRef.
Definition at line 1870 of file z3py.py.
01870 01871 def cast(self, val): 01872 """Try to cast `val` as an Integer or Real. 01873 01874 >>> IntSort().cast(10) 01875 10 01876 >>> is_int(IntSort().cast(10)) 01877 True 01878 >>> is_int(10) 01879 False 01880 >>> RealSort().cast(10) 01881 10 01882 >>> is_real(RealSort().cast(10)) 01883 True 01884 """ 01885 if is_expr(val): 01886 if __debug__: 01887 _z3_assert(self.ctx == val.ctx, "Context mismatch") 01888 val_s = val.sort() 01889 if self.eq(val_s): 01890 return val 01891 if val_s.is_int() and self.is_real(): 01892 return ToReal(val) 01893 if __debug__: 01894 _z3_assert(False, "Z3 Integer/Real expression expected" ) 01895 else: 01896 if self.is_int(): 01897 return IntVal(val, self.ctx) 01898 if self.is_real(): 01899 return RealVal(val, self.ctx) 01900 if __debug__: 01901 _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected")
def is_int | ( | self | ) |
Return `True` if `self` is of the sort Integer. >>> x = Int('x') >>> x.is_int() True >>> (x + 1).is_int() True >>> x = Real('x') >>> x.is_int() False
Definition at line 1852 of file z3py.py.
Referenced by ArithSortRef.cast().
def is_real | ( | self | ) |
Return `True` if `self` is of the sort Real. >>> x = Real('x') >>> x.is_real() True >>> (x + 1).is_real() True >>> x = Int('x') >>> x.is_real() False
Definition at line 1838 of file z3py.py.
Referenced by ArithSortRef.cast().
def subsort | ( | self, | |
other | |||
) |
Reimplemented from AstRef.
Definition at line 1882 of file z3py.py.
Referenced by FuncDeclRef::__call__(), ExprRef::__eq__(), Probe::__eq__(), Probe::__ge__(), ApplyResult::__getitem__(), Probe::__gt__(), Probe::__le__(), Probe::__lt__(), ExprRef::__ne__(), Probe::__ne__(), Fixedpoint::add_rule(), Tactic::apply(), ExprRef::arg(), ApplyResult::as_expr(), Fixedpoint::assert_exprs(), QuantifierRef::body(), BoolSortRef::cast(), ApplyResult::convert_model(), ExprRef::decl(), FuncDeclRef::domain(), Fixedpoint::get_answer(), Fixedpoint::get_assertions(), Fixedpoint::get_cover_delta(), Fixedpoint::get_rules(), SortRef::kind(), SortRef::name(), FuncDeclRef::name(), QuantifierRef::no_pattern(), 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(), Fixedpoint::statistics(), Solver::to_smt2(), Fixedpoint::update_rule(), QuantifierRef::var_name(), and QuantifierRef::var_sort().