Z3
FPSort.java
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2013 Microsoft Corporation
3 
4 Module Name:
5 
6  FPSort.java
7 
8 Abstract:
9 
10 Author:
11 
12  Christoph Wintersteiger (cwinter) 2013-06-10
13 
14 Notes:
15 
16 --*/
17 package com.microsoft.z3;
18 
22 public class FPSort extends Sort
23 {
24 
25  public FPSort(Context ctx, long obj)
26  {
27  super(ctx, obj);
28  }
29 
30  public FPSort(Context ctx, int ebits, int sbits)
31  {
32  super(ctx, Native.mkFpaSort(ctx.nCtx(), ebits, sbits));
33  }
34 
38  public int getEBits() {
39  return Native.fpaGetEbits(getContext().nCtx(), getNativeObject());
40  }
41 
45  public int getSBits() {
46  return Native.fpaGetSbits(getContext().nCtx(), getNativeObject());
47  }
48 
49 }
static int fpaGetEbits(long a0, long a1)
Definition: Native.java:6087
FPSort(Context ctx, long obj)
Definition: FPSort.java:25
static long mkFpaSort(long a0, int a1, int a2)
Definition: Native.java:5637
static int fpaGetSbits(long a0, long a1)
Definition: Native.java:6096
FPSort(Context ctx, int ebits, int sbits)
Definition: FPSort.java:30