Z3
AlgebraicNum.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
23public 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}
RatNum toUpper(int precision)
RatNum toLower(int precision)
String toDecimal(int precision)
static long getAlgebraicNumberUpper(long a0, long a1, int a2)
Definition: Native.java:3287
static String getNumeralDecimalString(long a0, long a1, int a2)
Definition: Native.java:3188
static long getAlgebraicNumberLower(long a0, long a1, int a2)
Definition: Native.java:3278
def String(name, ctx=None)
Definition: z3py.py:10085