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.AlgebraicNum
Definition: AlgebraicNum.java:24
com.microsoft.z3.AlgebraicNum.toUpper
RatNum toUpper(int precision)
Definition: AlgebraicNum.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.ArithExpr
Definition: ArithExpr.java:24
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.RatNum
Definition: RatNum.java:26
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10693