Z3
FPRMNum.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2013 Microsoft Corporation
3
4Module Name:
5
6 FPRMExpr.cs
7
8Abstract:
9
10 Z3 Managed API: Floating Point Rounding Mode Numerals
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2013-06-10
15
16Notes:
17
18--*/
19using System.Diagnostics;
20using System;
21using System.Collections.Generic;
22using System.Linq;
23using System.Text;
24
25
26namespace 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}
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:154
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
FloatingPoint RoundingMode Expressions
Definition: FPRMExpr.cs:32
Floating-point rounding mode numerals
Definition: FPRMNum.cs:32
bool isRTN
Indicates whether the term is the floating-point rounding numeral roundTowardNegative
Definition: FPRMNum.cs:71
bool isRNA
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
Definition: FPRMNum.cs:51
bool isRoundTowardPositive
Indicates whether the term is the floating-point rounding numeral roundTowardPositive
Definition: FPRMNum.cs:56
bool isRTZ
Indicates whether the term is the floating-point rounding numeral roundTowardZero
Definition: FPRMNum.cs:81
bool isRTP
Indicates whether the term is the floating-point rounding numeral roundTowardPositive
Definition: FPRMNum.cs:61
bool isRNE
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
Definition: FPRMNum.cs:41
bool isRoundNearestTiesToEven
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
Definition: FPRMNum.cs:36
override string ToString()
Returns a string representation of the numeral.
Definition: FPRMNum.cs:86
bool isRoundTowardZero
Indicates whether the term is the floating-point rounding numeral roundTowardZero
Definition: FPRMNum.cs:76
bool isRoundTowardNegative
Indicates whether the term is the floating-point rounding numeral roundTowardNegative
Definition: FPRMNum.cs:66
bool isRoundNearestTiesToAway
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
Definition: FPRMNum.cs:46
Function declarations.
Definition: FuncDecl.cs:31
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:137
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:1000