Preparing search index...
The search index is not available
z3-solver
z3-solver
FP
Interface FP<Name>
Floating-point expression (IEEE 754)
interface
FP
<
Name
extends
string
=
"main"
>
{
ctx
:
Context
<
Name
>
;
get
ast
()
:
Z3_ast
;
get
sort
()
:
S
;
abs
()
:
FP
<
Name
>
;
add
(
rm
:
FPRM
<
Name
>
,
other
:
CoercibleToFP
<
Name
>
)
:
FP
<
Name
>
;
arg
(
i
:
number
)
:
AnyExpr
<
Name
>
;
children
()
:
AnyExpr
<
Name
>
[]
;
decl
()
:
FuncDecl
<
Name
,
Sort
<
Name
>
[]
,
Sort
<
Name
>
>
;
div
(
rm
:
FPRM
<
Name
>
,
other
:
CoercibleToFP
<
Name
>
)
:
FP
<
Name
>
;
eq
(
other
:
CoercibleToExpr
<
Name
>
)
:
Bool
<
Name
>
;
eqIdentity
(
other
:
Ast
<
Name
,
unknown
>
)
:
boolean
;
fma
(
rm
:
FPRM
<
Name
>
,
y
:
CoercibleToFP
<
Name
>
,
z
:
CoercibleToFP
<
Name
>
,
)
:
FP
<
Name
>
;
ge
(
other
:
CoercibleToFP
<
Name
>
)
:
Bool
<
Name
>
;
gt
(
other
:
CoercibleToFP
<
Name
>
)
:
Bool
<
Name
>
;
hash
()
:
number
;
id
()
:
number
;
isInf
()
:
Bool
<
Name
>
;
isNaN
()
:
Bool
<
Name
>
;
isNegative
()
:
Bool
<
Name
>
;
isNormal
()
:
Bool
<
Name
>
;
isPositive
()
:
Bool
<
Name
>
;
isSubnormal
()
:
Bool
<
Name
>
;
isZero
()
:
Bool
<
Name
>
;
le
(
other
:
CoercibleToFP
<
Name
>
)
:
Bool
<
Name
>
;
lt
(
other
:
CoercibleToFP
<
Name
>
)
:
Bool
<
Name
>
;
mul
(
rm
:
FPRM
<
Name
>
,
other
:
CoercibleToFP
<
Name
>
)
:
FP
<
Name
>
;
name
()
:
string
|
number
;
neg
()
:
FP
<
Name
>
;
neq
(
other
:
CoercibleToExpr
<
Name
>
)
:
Bool
<
Name
>
;
neqIdentity
(
other
:
Ast
<
Name
,
unknown
>
)
:
boolean
;
numArgs
()
:
number
;
params
()
:
(
|
string
|
number
|
Sort
<
Name
>
|
Expr
<
Name
,
AnySort
<
Name
>
,
unknown
>
|
FuncDecl
<
Name
,
Sort
<
Name
>
[]
,
Sort
<
Name
>
>
)
[]
;
rem
(
other
:
CoercibleToFP
<
Name
>
)
:
FP
<
Name
>
;
sexpr
()
:
string
;
sqrt
(
rm
:
FPRM
<
Name
>
)
:
FP
<
Name
>
;
sub
(
rm
:
FPRM
<
Name
>
,
other
:
CoercibleToFP
<
Name
>
)
:
FP
<
Name
>
;
}
Type Parameters
Name
extends
string
=
"main"
Hierarchy (
View Summary
)
Expr
<
Name
,
FPSort
<
Name
>
,
Z3_ast
>
FP
FPNum
Index
Arithmetic
abs
add
div
fma
mul
neg
rem
sqrt
sub
Comparison
ge
gt
le
lt
Other
ctx
ast
sort
arg
children
decl
eq
eq
Identity
hash
id
name
neq
neq
Identity
num
Args
params
sexpr
Predicates
is
Inf
is
NaN
is
Negative
is
Normal
is
Positive
is
Subnormal
is
Zero
Arithmetic
abs
abs
()
:
FP
<
Name
>
Returns
FP
<
Name
>
add
add
(
rm
:
FPRM
<
Name
>
,
other
:
CoercibleToFP
<
Name
>
)
:
FP
<
Name
>
Parameters
rm
:
FPRM
<
Name
>
other
:
CoercibleToFP
<
Name
>
Returns
FP
<
Name
>
div
div
(
rm
:
FPRM
<
Name
>
,
other
:
CoercibleToFP
<
Name
>
)
:
FP
<
Name
>
Parameters
rm
:
FPRM
<
Name
>
other
:
CoercibleToFP
<
Name
>
Returns
FP
<
Name
>
fma
fma
(
rm
:
FPRM
<
Name
>
,
y
:
CoercibleToFP
<
Name
>
,
z
:
CoercibleToFP
<
Name
>
)
:
FP
<
Name
>
Parameters
rm
:
FPRM
<
Name
>
y
:
CoercibleToFP
<
Name
>
z
:
CoercibleToFP
<
Name
>
Returns
FP
<
Name
>
mul
mul
(
rm
:
FPRM
<
Name
>
,
other
:
CoercibleToFP
<
Name
>
)
:
FP
<
Name
>
Parameters
rm
:
FPRM
<
Name
>
other
:
CoercibleToFP
<
Name
>
Returns
FP
<
Name
>
neg
neg
()
:
FP
<
Name
>
Returns
FP
<
Name
>
rem
rem
(
other
:
CoercibleToFP
<
Name
>
)
:
FP
<
Name
>
Parameters
other
:
CoercibleToFP
<
Name
>
Returns
FP
<
Name
>
sqrt
sqrt
(
rm
:
FPRM
<
Name
>
)
:
FP
<
Name
>
Parameters
rm
:
FPRM
<
Name
>
Returns
FP
<
Name
>
sub
sub
(
rm
:
FPRM
<
Name
>
,
other
:
CoercibleToFP
<
Name
>
)
:
FP
<
Name
>
Parameters
rm
:
FPRM
<
Name
>
other
:
CoercibleToFP
<
Name
>
Returns
FP
<
Name
>
Comparison
ge
ge
(
other
:
CoercibleToFP
<
Name
>
)
:
Bool
<
Name
>
Parameters
other
:
CoercibleToFP
<
Name
>
Returns
Bool
<
Name
>
gt
gt
(
other
:
CoercibleToFP
<
Name
>
)
:
Bool
<
Name
>
Parameters
other
:
CoercibleToFP
<
Name
>
Returns
Bool
<
Name
>
le
le
(
other
:
CoercibleToFP
<
Name
>
)
:
Bool
<
Name
>
Parameters
other
:
CoercibleToFP
<
Name
>
Returns
Bool
<
Name
>
lt
lt
(
other
:
CoercibleToFP
<
Name
>
)
:
Bool
<
Name
>
Parameters
other
:
CoercibleToFP
<
Name
>
Returns
Bool
<
Name
>
Other
Readonly
ctx
ctx
:
Context
<
Name
>
ast
get
ast
()
:
Z3_ast
Returns
Z3_ast
sort
get
sort
()
:
S
Returns
S
arg
arg
(
i
:
number
)
:
AnyExpr
<
Name
>
Parameters
i
:
number
Returns
AnyExpr
<
Name
>
children
children
()
:
AnyExpr
<
Name
>
[]
Returns
AnyExpr
<
Name
>
[]
decl
decl
()
:
FuncDecl
<
Name
,
Sort
<
Name
>
[]
,
Sort
<
Name
>
>
Returns
FuncDecl
<
Name
,
Sort
<
Name
>
[]
,
Sort
<
Name
>
>
eq
eq
(
other
:
CoercibleToExpr
<
Name
>
)
:
Bool
<
Name
>
Parameters
other
:
CoercibleToExpr
<
Name
>
Returns
Bool
<
Name
>
eq
Identity
eqIdentity
(
other
:
Ast
<
Name
,
unknown
>
)
:
boolean
Parameters
other
:
Ast
<
Name
,
unknown
>
Returns
boolean
hash
hash
()
:
number
Returns
number
id
id
()
:
number
Returns
number
name
name
()
:
string
|
number
Returns
string
|
number
neq
neq
(
other
:
CoercibleToExpr
<
Name
>
)
:
Bool
<
Name
>
Parameters
other
:
CoercibleToExpr
<
Name
>
Returns
Bool
<
Name
>
neq
Identity
neqIdentity
(
other
:
Ast
<
Name
,
unknown
>
)
:
boolean
Parameters
other
:
Ast
<
Name
,
unknown
>
Returns
boolean
num
Args
numArgs
()
:
number
Returns
number
params
params
()
:
(
|
string
|
number
|
Sort
<
Name
>
|
Expr
<
Name
,
AnySort
<
Name
>
,
unknown
>
|
FuncDecl
<
Name
,
Sort
<
Name
>
[]
,
Sort
<
Name
>
>
)
[]
Returns (
|
string
|
number
|
Sort
<
Name
>
|
Expr
<
Name
,
AnySort
<
Name
>
,
unknown
>
|
FuncDecl
<
Name
,
Sort
<
Name
>
[]
,
Sort
<
Name
>
>
)
[]
sexpr
sexpr
()
:
string
Returns
string
Predicates
is
Inf
isInf
()
:
Bool
<
Name
>
Returns
Bool
<
Name
>
is
NaN
isNaN
()
:
Bool
<
Name
>
Returns
Bool
<
Name
>
is
Negative
isNegative
()
:
Bool
<
Name
>
Returns
Bool
<
Name
>
is
Normal
isNormal
()
:
Bool
<
Name
>
Returns
Bool
<
Name
>
is
Positive
isPositive
()
:
Bool
<
Name
>
Returns
Bool
<
Name
>
is
Subnormal
isSubnormal
()
:
Bool
<
Name
>
Returns
Bool
<
Name
>
is
Zero
isZero
()
:
Bool
<
Name
>
Returns
Bool
<
Name
>
Settings
Member Visibility
Protected
Inherited
External
Theme
OS
Light
Dark
On This Page
Arithmetic
abs
add
div
fma
mul
neg
rem
sqrt
sub
Comparison
ge
gt
le
lt
Other
ctx
ast
sort
arg
children
decl
eq
eq
Identity
hash
id
name
neq
neq
Identity
num
Args
params
sexpr
Predicates
is
Inf
is
NaN
is
Negative
is
Normal
is
Positive
is
Subnormal
is
Zero
z3-solver
Loading...
Floating-point expression (IEEE 754)