Z3
src
api
java
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.fpaGetEbits
static int fpaGetEbits(long a0, long a1)
Definition:
Native.java:6087
com.microsoft.z3.FPSort.FPSort
FPSort(Context ctx, long obj)
Definition:
FPSort.java:25
com.microsoft.z3.Native.mkFpaSort
static long mkFpaSort(long a0, int a1, int a2)
Definition:
Native.java:5637
com.microsoft.z3.Context
Definition:
Context.java:27
com.microsoft.z3.Native
Definition:
Native.java:4
com.microsoft.z3.FPSort
Definition:
FPSort.java:22
com.microsoft.z3.Native.fpaGetSbits
static int fpaGetSbits(long a0, long a1)
Definition:
Native.java:6096
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.FPSort.FPSort
FPSort(Context ctx, int ebits, int sbits)
Definition:
FPSort.java:30
com.microsoft.z3.Sort
Definition:
Sort.java:26
Generated on Tue Jul 19 2016 21:26:48 for Z3 by
1.8.11