Z3
src
api
java
AlgebraicNum.java
Go to the documentation of this file.
1
18
package
com.microsoft.z3;
19
23
public
class
AlgebraicNum
extends
ArithExpr
24
{
35
public
RatNum
toUpper
(
int
precision)
36
{
37
38
return
new
RatNum
(getContext(),
Native
.
getAlgebraicNumberUpper
(getContext()
39
.nCtx(), getNativeObject(), precision));
40
}
41
52
public
RatNum
toLower
(
int
precision)
53
{
54
55
return
new
RatNum
(getContext(),
Native
.
getAlgebraicNumberLower
(getContext()
56
.nCtx(), getNativeObject(), precision));
57
}
58
66
public
String
toDecimal
(
int
precision)
67
{
68
69
return
Native
.
getNumeralDecimalString
(getContext().nCtx(), getNativeObject(),
70
precision);
71
}
72
73
AlgebraicNum
(
Context
ctx,
long
obj)
74
{
75
super(ctx, obj);
76
77
}
78
}
com.microsoft.z3.Native.getAlgebraicNumberUpper
static long getAlgebraicNumberUpper(long a0, long a1, int a2)
Definition:
Native.java:3289
com.microsoft.z3.Native.getNumeralDecimalString
static String getNumeralDecimalString(long a0, long a1, int a2)
Definition:
Native.java:3190
com.microsoft.z3.AlgebraicNum.toUpper
RatNum toUpper(int precision)
Definition:
AlgebraicNum.java:35
com.microsoft.z3.Native.getAlgebraicNumberLower
static long getAlgebraicNumberLower(long a0, long a1, int a2)
Definition:
Native.java:3280
com.microsoft.z3.Native
Definition:
Native.java:4
com.microsoft.z3.AlgebraicNum
Definition:
AlgebraicNum.java:24
com.microsoft.z3.ArithExpr
Definition:
ArithExpr.java:24
com.microsoft.z3.Context
Definition:
Context.java:35
com.microsoft.z3.AlgebraicNum.toLower
RatNum toLower(int precision)
Definition:
AlgebraicNum.java:52
com.microsoft.z3.AlgebraicNum.toDecimal
String toDecimal(int precision)
Definition:
AlgebraicNum.java:66
com.microsoft.z3.RatNum
Definition:
RatNum.java:26
z3py.String
def String(name, ctx=None)
Definition:
z3py.py:10111
Generated on Sat Jul 11 2020 00:00:00 for Z3 by
1.8.18