Z3
src
api
dotnet
FPRMNum.cs
Go to the documentation of this file.
1
/*++
2
Copyright (c) 2013 Microsoft Corporation
3
4
Module Name:
5
6
FPRMExpr.cs
7
8
Abstract:
9
10
Z3 Managed API: Floating Point Rounding Mode Numerals
11
12
Author:
13
14
Christoph Wintersteiger (cwinter) 2013-06-10
15
16
Notes:
17
18
--*/
19
using
System
;
20
using
System
.Collections.Generic;
21
using
System
.Linq;
22
using
System
.Text;
23
24
using
System
.
Diagnostics
.
Contracts
;
25
26
namespace
Microsoft
.Z3
27
{
31
public
class
FPRMNum
:
FPRMExpr
32
{
36
public
bool
isRoundNearestTiesToEven {
get
{
return
IsApp &&
FuncDecl
.
DeclKind
==
Z3_decl_kind
.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
37
41
public
bool
isRNE {
get
{
return
IsApp &&
FuncDecl
.
DeclKind
==
Z3_decl_kind
.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
42
46
public
bool
isRoundNearestTiesToAway {
get
{
return
IsApp &&
FuncDecl
.
DeclKind
==
Z3_decl_kind
.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
47
51
public
bool
isRNA {
get
{
return
IsApp &&
FuncDecl
.
DeclKind
==
Z3_decl_kind
.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
52
56
public
bool
isRoundTowardPositive {
get
{
return
IsApp &&
FuncDecl
.
DeclKind
==
Z3_decl_kind
.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }
57
61
public
bool
isRTP {
get
{
return
IsApp &&
FuncDecl
.
DeclKind
==
Z3_decl_kind
.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }
62
66
public
bool
isRoundTowardNegative {
get
{
return
IsApp &&
FuncDecl
.
DeclKind
==
Z3_decl_kind
.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }
67
71
public
bool
isRTN {
get
{
return
IsApp &&
FuncDecl
.
DeclKind
==
Z3_decl_kind
.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }
72
76
public
bool
isRoundTowardZero {
get
{
return
IsApp &&
FuncDecl
.
DeclKind
==
Z3_decl_kind
.Z3_OP_FPA_RM_TOWARD_ZERO; } }
77
81
public
bool
isRTZ {
get
{
return
IsApp &&
FuncDecl
.
DeclKind
==
Z3_decl_kind
.Z3_OP_FPA_RM_TOWARD_ZERO; } }
82
86
public
override
string
ToString
()
87
{
88
return
Native.Z3_get_numeral_string(
Context
.nCtx, NativeObject);
89
}
90
91
#region Internal
92
internal
FPRMNum
(
Context
ctx, IntPtr obj)
94
: base(ctx, obj)
95
{
96
Contract.Requires(ctx != null);
97
}
98
#endregion
99
}
100
}
Microsoft.Z3.FPRMNum.ToString
override string ToString()
Returns a string representation of the numeral.
Definition:
FPRMNum.cs:86
System
Microsoft.Z3.FPRMNum
Floating-point rounding mode numerals
Definition:
FPRMNum.cs:31
System.Diagnostics
Microsoft
Microsoft.Z3.FuncDecl.DeclKind
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition:
FuncDecl.cs:138
System.Diagnostics.Contracts
Definition:
DummyContracts.cs:21
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition:
Context.cs:32
Microsoft.Z3.FPRMExpr
FloatingPoint RoundingMode Expressions
Definition:
FPRMExpr.cs:31
Microsoft.Z3.FuncDecl
Function declarations.
Definition:
FuncDecl.cs:29
Z3_decl_kind
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition:
z3_api.h:955
Generated on Sat Nov 12 2016 22:01:04 for Z3 by
1.8.12