Z3
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 }
RatNum toLower(int precision)
String toDecimal(int precision)
static String getNumeralDecimalString(long a0, long a1, int a2)
Definition: Native.java:2825
static long getAlgebraicNumberLower(long a0, long a1, int a2)
Definition: Native.java:2906
static long getAlgebraicNumberUpper(long a0, long a1, int a2)
Definition: Native.java:2915
RatNum toUpper(int precision)
def String(name, ctx=None)
Definition: z3py.py:9443