5 // Alexander Chebaturkin (chebaturkin@gmail.com)
7 // Copyright (C) 2012 Alexander Chebaturkin
9 // Permission is hereby granted, free of charge, to any person obtaining
10 // a copy of this software and associated documentation files (the
11 // "Software"), to deal in the Software without restriction, including
12 // without limitation the rights to use, copy, modify, merge, publish,
13 // distribute, sublicense, and/or sell copies of the Software, and to
14 // permit persons to whom the Software is furnished to do so, subject to
15 // the following conditions:
17 // The above copyright notice and this permission notice shall be
18 // included in all copies or substantial portions of the Software.
20 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
21 // EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
22 // MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
23 // NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
24 // LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
25 // OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
26 // WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
30 using System
.Collections
.Generic
;
35 using Mono
.CodeContracts
.Static
.DataStructures
;
36 using Mono
.CodeContracts
.Static
.Lattices
;
38 namespace Mono
.CodeContracts
.Static
.Analysis
.Numerical
{
39 public class DisInterval
: IntervalBase
<DisInterval
, Rational
> {
40 public static readonly DisInterval NotZero
=
41 For (Sequence
<Interval
>.From (Interval
.For (Rational
.MinusInfinity
, -1L),
42 Interval
.For (1L, Rational
.PlusInfinity
)));
44 static DisInterval cached_bottom
;
45 static DisInterval cached_top
;
47 readonly Sequence
<Interval
> intervals
;
48 readonly Interval join_interval
;
51 DisInterval (Interval interval
)
52 : base (interval
.LowerBound
, interval
.UpperBound
)
54 var list
= Sequence
<Interval
>.Empty
;
57 else if (interval
.IsBottom
)
61 list
= list
.Cons (interval
);
65 join_interval
= interval
;
68 DisInterval (Sequence
<Interval
> intervals
)
69 : base (Rational
.MinusInfinity
, Rational
.PlusInfinity
)
72 this.intervals
= Normalize (intervals
, out isBottom
);
75 join_interval
= Interval
.BottomValue
;
81 join_interval
= JoinAll (intervals
);
82 if (join_interval
.IsBottom
)
84 else if (join_interval
.IsTop
)
85 state
= intervals
.Length () <= 1 ? State
.Top
: State
.Normal
;
87 LowerBound
= join_interval
.LowerBound
;
88 UpperBound
= join_interval
.UpperBound
;
93 DisInterval (State state
)
94 : base (Rational
.MinusInfinity
, Rational
.PlusInfinity
)
97 join_interval
= state
== State
.Bottom
? Interval
.BottomValue
: Interval
.TopValue
;
98 intervals
= Sequence
<Interval
>.Empty
;
101 public static DisInterval BottomValue { get { return cached_bottom ?? (cached_bottom = new DisInterval (State.Bottom)); }
}
103 public static DisInterval TopValue { get { return cached_top ?? (cached_top = new DisInterval (State.Top)); }
}
105 public Interval AsInterval { get { return join_interval; }
}
107 public override DisInterval Top { get { return TopValue; }
}
109 public override DisInterval Bottom { get { return BottomValue; }
}
111 public override bool IsTop { get { return state == State.Top; }
}
113 public override bool IsBottom { get { return state == State.Bottom; }
}
115 public bool IsNotZero
119 if (!this.IsNormal ())
122 return intervals
.All (intv
=> !intv
.Includes (0));
126 public bool IsPositiveOrZero { get { return this.IsNormal () && LowerBound >= 0L; }
}
128 public override bool Equals (object other
)
130 if (ReferenceEquals (this, other
))
132 var that
= other
as DisInterval
;
135 var intv
= other
as Interval
;
139 return Equals (For (intv
));
142 if (state
== that
.state
&& join_interval
.Equals (that
.join_interval
))
143 return HaveSameIntervals (intervals
, that
.intervals
);
148 static bool HaveSameIntervals (Sequence
<Interval
> left
, Sequence
<Interval
> right
)
150 if (left
.Length () != right
.Length ())
154 var curRight
= right
;
156 while (!curLeft
.IsEmpty ()) {
157 if (!curLeft
.Head
.Equals (curRight
.Head
))
159 curLeft
= curLeft
.Tail
;
160 curRight
= curRight
.Tail
;
166 public override int GetHashCode ()
169 return (state
.GetHashCode () * 397) ^
170 (join_interval
!= null ? join_interval
.GetHashCode () : 0);
174 public static Sequence
<Interval
> Normalize (Sequence
<Interval
> intervals
, out bool isBottom
)
176 if (intervals
.Length () == 0) {
181 Comparison
<Interval
> comparison
=
182 (a
, b
) => a
.Equals (b
) ? 0 : a
.UpperBound
<= b
.UpperBound
? -1 : 1;
184 var intervalList
= new List
<Interval
> (intervals
.AsEnumerable ());
185 intervalList
.Sort (comparison
);
187 var list
= Sequence
<Interval
>.Empty
;
190 Interval last
= null;
192 foreach (var t
in intervalList
) {
197 else if (cur
.IsTop
) {
199 return Sequence
<Interval
>.Empty
;
201 else if (!cur
.Equals (last
)) {
203 while (list
!= null) {
205 if (Interval
.AreConsecutiveIntegers (last
, cur
)) {
207 cur
= last
.Join (cur
);
209 else if (last
.LessEqual (cur
))
211 else if (last
.OverlapsWith (cur
)) {
213 cur
= cur
.Join (last
);
221 list
= list
.Cons (cur
);
225 isBottom
= bottomCnt
== intervals
.Length ();
226 return list
.Reverse ();
229 public static Interval
JoinAll (Sequence
<Interval
> list
)
232 return Interval
.TopValue
;
237 while (cur
!= null) {
238 res
= res
.Join (cur
.Head
);
245 protected override bool IsFiniteBound (Rational n
)
247 return !n
.IsInfinity
;
250 public static DisInterval
operator + (DisInterval left
, DisInterval right
)
252 return OperatorLifting (left
, right
, (a
, b
) => a
+ b
, true);
255 public static DisInterval
operator * (DisInterval left
, DisInterval right
)
257 return OperatorLifting (left
, right
, (a
, b
) => a
* b
, true);
260 public static DisInterval
operator / (DisInterval left
, DisInterval right
)
262 return OperatorLifting (left
, right
, (a
, b
) => a
/ b
, true);
265 public static DisInterval
operator - (DisInterval left
, DisInterval right
)
267 return OperatorLifting (left
, right
, (a
, b
) => a
- b
, true);
270 public static DisInterval
operator - (DisInterval left
)
272 if (left
.IsBottom
|| left
.IsTop
)
275 return For (left
.intervals
.Select (i
=> -i
).Reverse ());
278 static DisInterval
OperatorLifting (DisInterval left
, DisInterval right
,
279 Func
<Interval
, Interval
, Interval
> binop
, bool propagateTop
)
281 if (left
.IsBottom
|| right
.IsBottom
)
284 if ((propagateTop
&& (left
.IsTop
|| right
.IsTop
)) || (left
.IsTop
&& right
.IsTop
))
287 var intervals
= Sequence
<Interval
>.Empty
;
289 var hasNoNormals
= true;
291 if (propagateTop
|| (left
.IsNormal () && right
.IsNormal ()))
292 foreach (var leftIntv
in left
.intervals
.AsEnumerable ())
293 foreach (var rightIntv
in right
.intervals
.AsEnumerable ()) {
294 var res
= binop (leftIntv
, rightIntv
);
300 hasNoNormals
= false;
301 intervals
= intervals
.Cons (res
);
304 var notTop
= left
.IsTop
? right
: left
;
305 var rightIsTop
= !left
.IsTop
;
307 foreach (var intv
in notTop
.intervals
.AsEnumerable ()) {
309 ? binop (intv
, Interval
.TopValue
)
310 : binop (Interval
.TopValue
, intv
);
317 hasNoNormals
= false;
318 intervals
= intervals
.Cons (res
);
322 return hasNoNormals
? BottomValue
: For (intervals
.Reverse ());
325 public override DisInterval
Widen (DisInterval that
)
327 if (IsTop
|| that
.IsTop
)
330 return new DisInterval (Widen (intervals
, that
.intervals
));
333 static Sequence
<Interval
> Widen (Sequence
<Interval
> left
, Sequence
<Interval
> right
)
335 if (left
.IsEmpty () || right
.IsEmpty ())
337 if (left
.Length () == 1 && right
.Length () == 1)
338 return Sequence
<Interval
>.Singleton (left
.Head
.Widen (right
.Head
));
340 if (left
.Length () == 1) {
341 if (left
.Head
.LessEqual (right
.Head
))
343 return Sequence
<Interval
>.Singleton (left
.Head
.Widen (right
.Head
.Join (right
.Last ())));
346 if (right
.Length () == 1)
347 return Sequence
<Interval
>.Singleton (left
.Head
.Join (left
.Last ()).Widen (right
.Head
));
349 var l
= left
.Head
.Widen (right
.Head
);
350 var r
= left
.Last ().Widen (right
.Last ());
352 var list
= Sequence
<Interval
>.Singleton (l
);
354 var curRight
= right
.Tail
;
355 while (curRight
!= null && curRight
.Tail
!= null) {
356 var curLeft
= left
.Tail
;
357 while (curLeft
!= null && curRight
.Tail
!= null)
358 if (curLeft
.Head
.LessEqual (curRight
.Head
)) {
359 list
= list
.Cons (curRight
.Head
);
363 list
= list
.Cons (r
);
365 return list
.Reverse ();
368 public override DisInterval
Meet (DisInterval that
)
371 if (this.TryTrivialMeet (that
, out result
))
375 var meetIntervals
= Meet (intervals
, that
.intervals
, out isBottom
);
379 if (meetIntervals
.Length () == 0)
382 return For (meetIntervals
);
385 static Sequence
<Interval
> Meet (Sequence
<Interval
> left
, Sequence
<Interval
> right
, out bool isBottom
)
388 var list
= Sequence
<Interval
>.Empty
;
389 foreach (var leftIntv
in left
.AsEnumerable ()) {
390 foreach (var rightIntv
in right
.AsEnumerable ()) {
391 var res
= leftIntv
.Meet (rightIntv
);
392 if (res
.IsNormal ()) {
394 list
= list
.Cons (res
);
399 return list
.Reverse ();
402 public override DisInterval
ImmutableVersion ()
407 public override DisInterval
Clone ()
412 public override void Dump (TextWriter tw
)
416 public override bool LessEqual (DisInterval that
)
419 if (this.TryTrivialLessEqual (that
, out result
))
422 if (!join_interval
.LessEqual (that
.join_interval
))
425 return intervals
.AsEnumerable ().All (inv
=> that
.intervals
.Any (inv
.LessEqual
));
428 public override DisInterval
Join (DisInterval that
, bool widening
, out bool weaker
)
434 public override DisInterval
Join (DisInterval that
)
437 if (this.TryTrivialJoin (that
, out result
))
440 var join = Join (intervals
, that
.intervals
);
447 static Sequence
<Interval
> Join (Sequence
<Interval
> left
, Sequence
<Interval
> right
)
449 var list
= Sequence
<Interval
>.Empty
;
452 var curRight
= right
;
454 while (!curLeft
.IsEmpty () && !curRight
.IsEmpty ()) {
455 var l
= curLeft
.Head
;
456 var r
= curRight
.Head
;
458 if (l
.IsTop
|| r
.IsTop
)
459 return Sequence
<Interval
>.Empty
;
462 curLeft
= curLeft
.Tail
;
464 curRight
= curRight
.Tail
;
465 else if (l
.LessEqual (r
)) {
466 list
= list
.Cons (r
);
467 curLeft
= curLeft
.Tail
;
468 curRight
= curRight
.Tail
;
470 else if (r
.LessEqual (l
)) {
471 list
= list
.Cons (l
);
472 curLeft
= curLeft
.Tail
;
473 curRight
= curRight
.Tail
;
475 else if (r
.OverlapsWith (l
)) {
476 list
= list
.Cons (l
.Join (r
));
477 curLeft
= curLeft
.Tail
;
478 curRight
= curRight
.Tail
;
480 else if (l
.OnTheLeftOf (r
)) {
481 list
= list
.Cons (l
);
482 curLeft
= curLeft
.Tail
;
484 else if (r
.OnTheLeftOf (l
)) {
485 list
= list
.Cons (r
);
486 curRight
= curRight
.Tail
;
490 while (!curLeft
.IsEmpty ()) {
491 list
= list
.Cons (curLeft
.Head
);
492 curLeft
= curLeft
.Tail
;
495 while (!curRight
.IsEmpty ()) {
496 list
= list
.Cons (curRight
.Head
);
497 curRight
= curRight
.Tail
;
500 return list
.Reverse ();
503 public static DisInterval
For (Interval interval
)
505 return new DisInterval (interval
);
508 public static DisInterval
For (Sequence
<Interval
> intervals
)
510 return new DisInterval (intervals
);
513 public override string ToString ()
518 return this.BottomSymbolIfAny ();
519 if (intervals
!= null && intervals
.Length () == 1)
520 return intervals
.Head
.ToString ();
522 return string.Format ("({0})", ToString (intervals
));
525 string ToString (Sequence
<Interval
> list
)
530 var sb
= new StringBuilder ();
533 foreach (var intv
in list
.AsEnumerable ()) {
542 return sb
.ToString ();
545 public DisInterval
Select (Func
<Interval
, Interval
> selector
)
550 return new DisInterval (selector (Interval
.TopValue
));
552 var list
= Sequence
<Interval
>.Empty
;
554 for (var cur
= intervals
; cur
!= null; cur
= cur
.Tail
) {
555 var intv
= selector (cur
.Head
);
561 list
= list
.Cons (intv
);
564 return new DisInterval (list
.Reverse ());
567 public static DisInterval
EverythingExcept (DisInterval interval
)
569 var left
= Interval
.For (Rational
.MinusInfinity
, interval
.LowerBound
- 1L);
570 var right
= Interval
.For (interval
.UpperBound
+ 1L, Rational
.PlusInfinity
);
572 if (left
.IsNormal () && right
.IsNormal ())
573 return new DisInterval (Sequence
<Interval
>.From (left
, right
));
575 if (left
.IsNormal ())
576 return new DisInterval (left
);
578 if (right
.IsNormal ())
579 return new DisInterval (right
);
584 #region Nested type: State