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 }
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:23
com.microsoft.z3.ArithExpr
Definition: ArithExpr.java:23
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:25
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10111