Z3
AlgebraicNum.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
23 public class AlgebraicNum extends ArithExpr
24 {
33  public RatNum toUpper(int precision) throws Z3Exception
34  {
35 
36  return new RatNum(getContext(), Native.getAlgebraicNumberUpper(getContext()
37  .nCtx(), getNativeObject(), precision));
38  }
39 
47  public RatNum toLower(int precision) throws Z3Exception
48  {
49 
50  return new RatNum(getContext(), Native.getAlgebraicNumberLower(getContext()
51  .nCtx(), getNativeObject(), precision));
52  }
53 
58  public String toDecimal(int precision) throws Z3Exception
59  {
60 
61  return Native.getNumeralDecimalString(getContext().nCtx(), getNativeObject(),
62  precision);
63  }
64 
65  AlgebraicNum(Context ctx, long obj) throws Z3Exception
66  {
67  super(ctx, obj);
68 
69  }
70 }
RatNum toLower(int precision)
String toDecimal(int precision)
static String getNumeralDecimalString(long a0, long a1, int a2)
Definition: Native.java:2435
static long getAlgebraicNumberLower(long a0, long a1, int a2)
Definition: Native.java:2516
static long getAlgebraicNumberUpper(long a0, long a1, int a2)
Definition: Native.java:2525
RatNum toUpper(int precision)