Z3 |

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.Diagnostics;
20 using System;
21 using System.Collections.Generic;
22 using System.Linq;
23 using System.Text;
24
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
93 internal FPRMNum(Context ctx, IntPtr obj)
94 : base(ctx, obj)
95 {
96 Debug.Assert(ctx != null);
97 }
98 #endregion
99 }
100}
Microsoft.Z3.AST.IsApp
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:154
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:32
Microsoft.Z3.FPRMNum
Floating-point rounding mode numerals
Definition: FPRMNum.cs:32
Microsoft.Z3.FPRMNum.isRTN
bool isRTN
Indicates whether the term is the floating-point rounding numeral roundTowardNegative
Definition: FPRMNum.cs:71
Microsoft.Z3.FPRMNum.isRNA
bool isRNA
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
Definition: FPRMNum.cs:51
Microsoft.Z3.FPRMNum.isRoundTowardPositive
bool isRoundTowardPositive
Indicates whether the term is the floating-point rounding numeral roundTowardPositive
Definition: FPRMNum.cs:56
Microsoft.Z3.FPRMNum.isRTZ
bool isRTZ
Indicates whether the term is the floating-point rounding numeral roundTowardZero
Definition: FPRMNum.cs:81
Microsoft.Z3.FPRMNum.isRTP
bool isRTP
Indicates whether the term is the floating-point rounding numeral roundTowardPositive
Definition: FPRMNum.cs:61
Microsoft.Z3.FPRMNum.isRNE
bool isRNE
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
Definition: FPRMNum.cs:41
Microsoft.Z3.FPRMNum.isRoundNearestTiesToEven
bool isRoundNearestTiesToEven
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
Definition: FPRMNum.cs:36
Microsoft.Z3.FPRMNum.ToString
override string ToString()
Returns a string representation of the numeral.
Definition: FPRMNum.cs:86
Microsoft.Z3.FPRMNum.isRoundTowardZero
bool isRoundTowardZero
Indicates whether the term is the floating-point rounding numeral roundTowardZero
Definition: FPRMNum.cs:76
Microsoft.Z3.FPRMNum.isRoundTowardNegative
bool isRoundTowardNegative
Indicates whether the term is the floating-point rounding numeral roundTowardNegative
Definition: FPRMNum.cs:66
Microsoft.Z3.FPRMNum.isRoundNearestTiesToAway
bool isRoundNearestTiesToAway
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
Definition: FPRMNum.cs:46
Microsoft.Z3.FuncDecl
Function declarations.
Definition: FuncDecl.cs:31
Microsoft.Z3.FuncDecl.DeclKind
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:137
Microsoft.Z3
Definition: AlgebraicNum.cs:27
Z3_decl_kind
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:1000