diff options
| author |  leino <unknown> | 2014-07-21 22:59:58 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-07-21 22:59:58 -0700 |
| commit | f314be9242a07c302721701072696bdadc9a7acf (patch) | |
| tree | 00a10288f9d193b6a2ffcdbd51b87f07d1a52c2a /Binaries/DafnyRuntime.cs | |
| parent | c377658acba5472b6d0c1e1452ce4c4c8f1fc28e (diff) | |
Implemented missing routine in runtime system (real-to-int conversion)
Diffstat (limited to 'Binaries/DafnyRuntime.cs')
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index 6f0cab13..d6bd895a 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -656,6 +656,13 @@ namespace Dafny num = n;
den = d;
}
+ public BigInteger ToBigInteger() {
+ if (0 <= num) {
+ return num / den;
+ } else {
+ return (num - den + 1) / den;
+ }
+ }
/// <summary>
/// Returns values such that aa/dd == a and bb/dd == b.
/// </summary>
|