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;
20 using System.Collections.Generic;
21 using System.Linq;
22 using System.Text;
23 
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 }
override string ToString()
Returns a string representation of the numeral.
Definition: FPRMNum.cs:86
Floating-point rounding mode numerals
Definition: FPRMNum.cs:31
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
FloatingPoint RoundingMode Expressions
Definition: FPRMExpr.cs:31
Function declarations.
Definition: FuncDecl.cs:29
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955