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 }
com.microsoft.z3.Native.mkFpaSort
static long mkFpaSort(long a0, int a1, int a2)
Definition: Native.java:6031
com.microsoft.z3.Native.fpaGetEbits
static int fpaGetEbits(long a0, long a1)
Definition: Native.java:6481
com.microsoft.z3.Sort
Definition: Sort.java:26
com.microsoft.z3.FPSort.FPSort
FPSort(Context ctx, long obj)
Definition: FPSort.java:25
com.microsoft.z3.FPSort
Definition: FPSort.java:22
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:3966
com.microsoft.z3.Native
Definition: Native.java:4
com.microsoft.z3.FPSort.getEBits
int getEBits()
Definition: FPSort.java:38
com.microsoft.z3.FPSort.getSBits
int getSBits()
Definition: FPSort.java:45
com.microsoft.z3.Native.fpaGetSbits
static int fpaGetSbits(long a0, long a1)
Definition: Native.java:6490
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.FPSort.FPSort
FPSort(Context ctx, int ebits, int sbits)
Definition: FPSort.java:30