struct Float64

Defined in:

z3/core_ext.cr

Instance Method Summary

Instance Method Detail

def !=(other : Z3::RealExpr) #

[View source]
def !=(other : Z3::FloatExpr) #

[View source]
def *(other : Z3::RealExpr) #

[View source]
def +(other : Z3::RealExpr) #

[View source]
def -(other : Z3::RealExpr) #

[View source]
def /(other : Z3::RealExpr) #

[View source]
def <(other : Z3::RealExpr) #

[View source]
def <(other : Z3::FloatExpr) #

[View source]
def <=(other : Z3::RealExpr) #

[View source]
def <=(other : Z3::FloatExpr) #

[View source]
def ==(other : Z3::RealExpr) #

[View source]
def ==(other : Z3::FloatExpr) #

A Float literal takes its sort from the expression it's paired with. There's no arithmetic here because Float arithmetic needs a rounding mode, so it's spelled expr.add(1.5, mode) and never 1.5 + expr.


[View source]
def >(other : Z3::RealExpr) #

[View source]
def >(other : Z3::FloatExpr) #

[View source]
def >=(other : Z3::RealExpr) #

[View source]
def >=(other : Z3::FloatExpr) #

[View source]