Float64
Inherits Float < Comparable < Comparable < Comparable < Number < Comparable < Steppable < Comparable < Value < Object
Instance methods
!=(other : Z3::RealExpr)
Source!=(other : Z3::FloatExpr)
Source*(other : Z3::RealExpr)
Source+(other : Z3::RealExpr)
Source-(other : Z3::RealExpr)
Source/(other : Z3::RealExpr)
Source<(other : Z3::RealExpr)
Source<(other : Z3::FloatExpr)
Source<=(other : Z3::RealExpr)
Source<=(other : Z3::FloatExpr)
Source==(other : Z3::RealExpr)
Source==(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.
>(other : Z3::RealExpr)
Source>(other : Z3::FloatExpr)
Source>=(other : Z3::RealExpr)
Source>=(other : Z3::FloatExpr)
Source