mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Numerical/IntervalInference.cs

   1 //
   2 // IntervalInference.cs
   3 //
   4 // Authors:
   5 //      Alexander Chebaturkin (chebaturkin@gmail.com)
   6 //
   7 // Copyright (C) 2012 Alexander Chebaturkin
   8 //
   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:
  16 //
  17 // The above copyright notice and this permission notice shall be
  18 // included in all copies or substantial portions of the Software.
  19 //
  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.
  27 //
  28
  29 using System;
  30 using System.Collections.Generic;
  31
  32 using Mono.CodeContracts.Static.DataStructures;
  33 using Mono.CodeContracts.Static.Lattices;
  34
  35 namespace Mono.CodeContracts.Static.Analysis.Numerical {
  36         static class IntervalInference {
  37                 public static class ConstraintsFor {
  38                         public static IDictionary<TVar, Sequence<TInterval>> GreaterEqualThanZero<TEnv, TVar, TExpr, TInterval>
  39                                 (TExpr expr, IExpressionDecoder<TVar, TExpr> decoder, TEnv env)
  40                                 where TEnv : IIntervalEnvironment<TVar, TExpr, TInterval, Rational>
  41                                 where TVar : IEquatable<TVar>
  42                                 where TInterval : IntervalBase<TInterval, Rational>
  43                         {
  44                                 var result = new Dictionary<TVar, Sequence<TInterval>> ();
  45                                 var variable = decoder.UnderlyingVariable (expr);
  46
  47                                 AddToResult (result, variable, env.Eval (expr).Meet (env.Context.Positive));
  48
  49                                 if (!decoder.IsVariable (expr)) {
  50                                         Polynomial<TVar, TExpr> zeroPoly; // poly(0)
  51                                         if (!Polynomial<TVar, TExpr>.TryToPolynomial (new[] {Monomial<TVar>.From (Rational.Zero)}, out zeroPoly))
  52                                                 throw new AbstractInterpretationException (
  53                                                         "It can never be the case that the conversion of a list of monomials into a polynomial fails.");
  54
  55                                         Polynomial<TVar, TExpr> exprPoly; // poly(expr)
  56                                         Polynomial<TVar, TExpr> fullPoly; // '0 <= poly(expr)' polynome
  57                                         if (Polynomial<TVar, TExpr>.TryBuildFrom (expr, decoder, out exprPoly) &&
  58                                             Polynomial<TVar, TExpr>.TryToPolynomial (ExpressionOperator.LessEqualThan, zeroPoly, exprPoly, out fullPoly) &&
  59                                             fullPoly.IsIntervalForm) {
  60                                                 var k = fullPoly.Left[0].Coeff; // k != 0
  61                                                 TVar x;
  62                                                 fullPoly.Left[0].IsSingleVariable (out x);
  63
  64                                                 Rational constraint;
  65                                                 if (Rational.TryDivide (fullPoly.Right[0].Coeff, k, out constraint)) {
  66                                                         TInterval interval;
  67                                                         if (k > 0L) // +x <= constraint
  68                                                                 interval = env.Eval (x).Meet (env.Context.For (Rational.MinusInfinity, constraint));
  69                                                         else // -x <= -constraint ==> x >= constraint
  70                                                                 interval = env.Eval (x).Meet (env.Context.For (constraint, Rational.PlusInfinity));
  71
  72                                                         AddToResult (result, x, interval);
  73                                                 }
  74                                         }
  75                                 }
  76                                 return result;
  77                         }
  78
  79                         public static IDictionary<TVar, Sequence<TInterval>> LessEqualThan<TEnv, TVar, TExpr, TInterval>
  80                                 (TExpr left, TExpr right, IExpressionDecoder<TVar, TExpr> decoder, TEnv env, out bool isBottom)
  81                                 where TEnv : IIntervalEnvironment<TVar, TExpr, TInterval, Rational>
  82                                 where TVar : IEquatable<TVar>
  83                                 where TInterval : IntervalBase<TInterval, Rational>
  84                         {
  85                                 isBottom = false;
  86                                 var result = new Dictionary<TVar, Sequence<TInterval>> ();
  87
  88                                 if (IsFloat (left, decoder) || IsFloat (right, decoder))
  89                                         return result;
  90
  91                                 var leftIntv = env.Eval (left);
  92                                 var rightIntv = env.Eval (right);
  93
  94                                 var leftVar = decoder.UnderlyingVariable (left);
  95                                 var rightVar = decoder.UnderlyingVariable (right);
  96
  97                                 TInterval refinedIntv;
  98                                 if (TryRefineLessEqualThan<TEnv, TVar, TExpr, TInterval> (leftIntv, rightVar, env, out refinedIntv))
  99                                         AddToResult (result, rightVar, refinedIntv);
 100
 101                                 if (TryRefineLeftLessEqualThanK<TEnv, TVar, TExpr, TInterval> (leftVar, rightIntv, env, out refinedIntv))
 102                                         AddToResult (result, leftVar, refinedIntv);
 103
 104                                 Polynomial<TVar, TExpr> poly;
 105                                 Polynomial<TVar, TExpr> leftPoly;
 106                                 Polynomial<TVar, TExpr> rightPoly;
 107
 108                                 if (Polynomial<TVar, TExpr>.TryBuildFrom (left, decoder, out leftPoly) &&
 109                                     Polynomial<TVar, TExpr>.TryBuildFrom (right, decoder, out rightPoly) &&
 110                                     Polynomial<TVar, TExpr>.TryToPolynomial (ExpressionOperator.LessEqualThan, leftPoly, rightPoly, out poly) &&
 111                                     poly.IsLinear) {
 112                                         if (poly.Left.Length == 1)
 113                                                 return TestTrueLessEqualThan_AxLeqK (poly, env, result, out isBottom);
 114                                         if (poly.Left.Length == 2)
 115                                                 return TestTrueLessEqualThan_AxByLeqK (poly, env, result, out isBottom);
 116                                 }
 117
 118                                 return result;
 119                         }
 120
 121                         public static IDictionary<TVar, Sequence<TInterval>> LessThan<TEnv, TVar, TExpr, TInterval>
 122                                 (TExpr left, TExpr right, IExpressionDecoder<TVar, TExpr> decoder, TEnv env, out bool isBottom)
 123                                 where TEnv : IIntervalEnvironment<TVar, TExpr, TInterval, Rational>
 124                                 where TVar : IEquatable<TVar>
 125                                 where TInterval : IntervalBase<TInterval, Rational>
 126                         {
 127                                 isBottom = false;
 128                                 var result = new Dictionary<TVar, Sequence<TInterval>> ();
 129
 130                                 var leftIntv = env.Eval (left);
 131                                 var rightIntv = env.Eval (right);
 132
 133                                 var rightVar = decoder.UnderlyingVariable (right);
 134                                 var successor = IsFloat (left, decoder) || IsFloat (right, decoder) ? Rational.Zero : Rational.One;
 135
 136                                 TInterval refinedIntv;
 137                                 if (TryRefineKLessThanRight<TEnv, TVar, TExpr, TInterval> (leftIntv, rightVar, successor, env, out refinedIntv) && !refinedIntv.IsSinglePoint)
 138                                         AddToResult (result, rightVar, refinedIntv);
 139
 140                                 if (successor.IsZero)
 141                                         return result;
 142
 143                                 var leftVar = decoder.UnderlyingVariable (left);
 144                                 if (TryRefineLessThan<TEnv, TVar, TExpr, TInterval> (leftVar, rightIntv, env, out refinedIntv) && !refinedIntv.IsSinglePoint)
 145                                         AddToResult (result, leftVar, refinedIntv);
 146
 147                                 Polynomial<TVar, TExpr> poly;
 148                                 Polynomial<TVar, TExpr> leftPoly;
 149                                 Polynomial<TVar, TExpr> rightPoly;
 150
 151                                 if (Polynomial<TVar, TExpr>.TryBuildFrom (left, decoder, out leftPoly) &&
 152                                     Polynomial<TVar, TExpr>.TryBuildFrom (right, decoder, out rightPoly) &&
 153                                     Polynomial<TVar, TExpr>.TryToPolynomial (ExpressionOperator.LessThan, leftPoly, rightPoly, out poly) &&
 154                                     poly.IsLinear) {
 155                                         if (poly.Left.Length == 1)
 156                                                 return TestTrueLessEqualThan_AxLtK (poly, env, result, out isBottom);
 157                                         if (poly.Left.Length == 2)
 158                                                 return TestTrueLessEqualThan_AxByLtK (poly, env, result, out isBottom);
 159                                 }
 160
 161                                 return result;
 162                         }
 163
 164                         /// <summary>
 165                         /// Get interval for 'left' in inequation 'left &lt;= k'.
 166                         /// </summary>
 167                         public static bool TryRefineLeftLessEqualThanK<TEnv, TVar, TExpr, TInterval> (TVar left, TInterval k, TEnv env, out TInterval refined)
 168                                 where TEnv : IIntervalEnvironment<TVar, TExpr, TInterval, Rational>
 169                                 where TInterval : IntervalBase<TInterval, Rational>
 170                         {
 171                                 if (!k.IsNormal ())
 172                                         return false.Without (out refined);
 173
 174                                 var interval = env.Context.For (Rational.MinusInfinity, k.UpperBound);
 175
 176                                 TInterval leftIntv;
 177                                 if (env.TryGetValue (left, out leftIntv))
 178                                         interval = interval.Meet (leftIntv);
 179
 180                                 return true.With (interval, out refined);
 181                         }
 182
 183                         /// <summary>
 184                         /// Get interval for 'left' in inequation 'left &lt; k'.
 185                         /// </summary>
 186                         public static bool TryRefineLessThan<TEnv, TVar, TExpr, TInterval> (TVar left, TInterval k, TEnv env, out TInterval refined)
 187                                 where TEnv : IIntervalEnvironment<TVar, TExpr, TInterval, Rational>
 188                                 where TInterval : IntervalBase<TInterval, Rational>
 189                         {
 190                                 if (!k.IsNormal ())
 191                                         return false.Without (out refined);
 192
 193                                 var interval = env.Context.For (Rational.MinusInfinity, k.UpperBound.IsInteger ? k.UpperBound - 1L : k.UpperBound);
 194
 195                                 TInterval leftIntv;
 196                                 if (env.TryGetValue (left, out leftIntv))
 197                                         interval = interval.Meet (leftIntv);
 198
 199                                 return true.With (interval, out refined);
 200                         }
 201
 202                         /// <summary>
 203                         /// Get interval for 'right' in inequation 'k &lt;= right'.
 204                         /// </summary>
 205                         public static bool TryRefineLessEqualThan<TEnv, TVar, TExpr, TInterval> (TInterval k, TVar right, TEnv env, out TInterval refined)
 206                                 where TEnv : IIntervalEnvironment<TVar, TExpr, TInterval, Rational>
 207                                 where TInterval : IntervalBase<TInterval, Rational>
 208                         {
 209                                 if (!k.IsNormal ())
 210                                         return false.Without (out refined);
 211
 212                                 var interval = env.Context.RightOpen (k.LowerBound);
 213
 214                                 TInterval rightIntv;
 215                                 if (env.TryGetValue (right, out rightIntv))
 216                                         interval = interval.Meet (rightIntv);
 217
 218                                 return true.With (interval, out refined);
 219                         }
 220
 221                         /// <summary>
 222                         /// Get interval for 'right' in inequation 'k &lt; right'.
 223                         /// </summary>
 224                         public static bool TryRefineKLessThanRight<TEnv, TVar, TExpr, TInterval> (TInterval k, TVar right, Rational successor, TEnv env, out TInterval refined)
 225                                 where TEnv : IIntervalEnvironment<TVar, TExpr, TInterval, Rational>
 226                                 where TInterval : IntervalBase<TInterval, Rational>
 227                         {
 228                                 if (!k.IsNormal ())
 229                                         return false.Without (out refined);
 230
 231                                 // [k, +oo] or (k, +oo]
 232                                 var interval = env.Context.For (k.LowerBound.IsInteger ? k.LowerBound + successor : k.LowerBound, Rational.PlusInfinity);
 233
 234                                 TInterval rightIntv;
 235                                 if (env.TryGetValue (right, out rightIntv))
 236                                         interval = interval.Meet (rightIntv);
 237
 238                                 return true.With (interval, out refined);
 239                         }
 240
 241                         public static void NotEqual<TEnv, TVar, TExpr, TInterval>
 242                                 (TExpr left, TExpr right, IExpressionDecoder<TVar, TExpr> decoder, TEnv env, out InferenceResult<TVar, TInterval> resultLeft,
 243                                  out InferenceResult<TVar, TInterval> resultRight) where TInterval : IntervalBase<TInterval, Rational>
 244                                 where TEnv : IIntervalEnvironment<TVar, TExpr, TInterval, Rational>
 245                                 where TVar : IEquatable<TVar>
 246                         {
 247                                 resultLeft = InferenceResult<TVar, TInterval>.Empty;
 248                                 resultRight = InferenceResult<TVar, TInterval>.Empty;
 249
 250                                 var leftIntv = env.Eval (left);
 251                                 var rightIntv = env.Eval (right);
 252
 253                                 var leftVar = decoder.UnderlyingVariable (left);
 254                                 var rightVar = decoder.UnderlyingVariable (right);
 255
 256                                 var successor = IsFloat (left, decoder) || IsFloat (right, decoder) ? Rational.Zero : Rational.One;
 257
 258                                 // l != r <==> l < r && r < l
 259                                 LessThanRefinement<TEnv, TVar, TExpr, TInterval> (successor, env, leftIntv, rightIntv, leftVar, rightVar, ref resultLeft);
 260                                 LessThanRefinement<TEnv, TVar, TExpr, TInterval> (successor, env, rightIntv, leftIntv, rightVar, leftVar, ref resultRight);
 261                         }
 262
 263                         static void LessThanRefinement<TEnv, TVar, TExpr, TInterval>
 264                                 (Rational successor, TEnv env,
 265                                  TInterval leftIntv, TInterval rightIntv,
 266                                  TVar leftVar, TVar rightVar,
 267                                  ref InferenceResult<TVar, TInterval> result)
 268                                 where TEnv : IIntervalEnvironment<TVar, TExpr, TInterval, Rational>
 269                                 where TInterval : IntervalBase<TInterval, Rational>
 270                                 where TVar : IEquatable<TVar>
 271                         {
 272                                 TInterval refined;
 273                                 if (TryRefineKLessThanRight<TEnv, TVar, TExpr, TInterval> (leftIntv, rightVar, successor, env, out refined))
 274                                         result = result.AddConstraintFor (rightVar, refined);
 275                                 if (TryRefineLessThan<TEnv, TVar, TExpr, TInterval> (leftVar, rightIntv, env, out refined))
 276                                         result = result.AddConstraintFor (leftVar, refined);
 277                         }
 278
 279                         static IDictionary<TVar, Sequence<TInterval>> TestTrueLessEqualThan_AxByLeqK<TEnv, TVar, TExpr, TInterval>
 280                                 (Polynomial<TVar, TExpr> poly, TEnv env, IDictionary<TVar, Sequence<TInterval>> result, out bool isBottom)
 281                                 where TEnv : IIntervalEnvironment<TVar, TExpr, TInterval, Rational>
 282                                 where TVar : IEquatable<TVar>
 283                                 where TInterval : IntervalBase<TInterval, Rational>
 284                         {
 285                                 // ax + by <= k
 286                                 var ax = poly.Left[0];
 287                                 var by = poly.Left[1];
 288
 289                                 TVar x, y;
 290                                 ax.IsSingleVariable (out x);
 291                                 by.IsSingleVariable (out y);
 292
 293                                 var k = poly.Right[0].Coeff;
 294                                 var a = ax.Coeff;
 295                                 var b = by.Coeff;
 296
 297                                 var aInterval = env.Context.For (a);
 298                                 var bInterval = env.Context.For (b);
 299                                 var kInterval = env.Context.For (k);
 300
 301                                 var xInterval = env.Eval (x);
 302                                 var yInterval = env.Eval (y);
 303
 304                                 IntervalContextBase<TInterval, Rational> ctx = env.Context;
 305
 306                                 // x <= (k - (b * y)) / a;
 307                                 var boundingInterval = ctx.Div (ctx.Sub (kInterval, ctx.Mul (bInterval, yInterval)), aInterval);
 308                                 Func<Rational, TInterval> upperBounded = (i) => ctx.For (Rational.MinusInfinity, i);
 309                                 Func<Rational, TInterval> lowerBounded = (i) => ctx.For (i, Rational.PlusInfinity);
 310
 311                                 if (BoundVariable (ctx, a, xInterval, boundingInterval, x, result, out isBottom, upperBounded, lowerBounded))
 312                                         return result;
 313
 314                                 // y <= (k - (a * x)) / b;
 315                                 boundingInterval = ctx.Div (ctx.Sub (kInterval, ctx.Mul (aInterval, xInterval)), bInterval);
 316                                 if (BoundVariable (ctx, b, yInterval, boundingInterval, y, result, out isBottom, upperBounded, lowerBounded))
 317                                         return result;
 318
 319                                 return result;
 320                         }
 321
 322                         static IDictionary<TVar, Sequence<TInterval>> TestTrueLessEqualThan_AxByLtK<TEnv, TVar, TExpr, TInterval>
 323                                 (Polynomial<TVar, TExpr> poly, TEnv env, IDictionary<TVar, Sequence<TInterval>> result, out bool isBottom)
 324                                 where TEnv : IIntervalEnvironment<TVar, TExpr, TInterval, Rational>
 325                                 where TVar : IEquatable<TVar>
 326                                 where TInterval : IntervalBase<TInterval, Rational>
 327                         {
 328                                 // ax + by <= k
 329                                 var ax = poly.Left[0];
 330                                 var by = poly.Left[1];
 331
 332                                 TVar x, y;
 333                                 ax.IsSingleVariable (out x);
 334                                 by.IsSingleVariable (out y);
 335
 336                                 var k = poly.Right[0].Coeff;
 337                                 var a = ax.Coeff;
 338                                 var b = by.Coeff;
 339
 340                                 var aInterval = env.Context.For (a);
 341                                 var bInterval = env.Context.For (b);
 342                                 var kInterval = env.Context.For (k);
 343
 344                                 var xInterval = env.Eval (x);
 345                                 var yInterval = env.Eval (y);
 346
 347                                 IntervalContextBase<TInterval, Rational> ctx = env.Context;
 348                                 Func<Rational, TInterval> upperBounded =
 349                                         (i) => ctx.For (Rational.MinusInfinity, !i.IsInteger ? i.PreviousInt32 : i - 1L);
 350                                 Func<Rational, TInterval> lowerBounded =
 351                                         (i) => ctx.For (!i.IsInteger ? i.NextInt32 : i + 1L, Rational.PlusInfinity);
 352
 353                                 // x <= (k - (b * y)) / a;
 354                                 var boundingInterval = ctx.Div (ctx.Sub (kInterval, ctx.Mul (bInterval, yInterval)), aInterval);
 355                                 if (BoundVariable (ctx, a, xInterval, boundingInterval, x, result, out isBottom, upperBounded, lowerBounded))
 356                                         return result;
 357
 358                                 // y <= (k - (a * x)) / b;
 359                                 boundingInterval = ctx.Div (ctx.Sub (kInterval, ctx.Mul (aInterval, xInterval)), bInterval);
 360                                 if (BoundVariable (ctx, b, yInterval, boundingInterval, y, result, out isBottom, upperBounded, lowerBounded))
 361                                         return result;
 362
 363                                 return result;
 364                         }
 365
 366                         /// <summary>
 367                         /// Get constraints for variables from polynome in form 'a*x &lt;= k'
 368                         /// </summary>
 369                         /// <param name="poly">Polynome in canonical form. Two monomes involved. </param>
 370                         static IDictionary<TVar, Sequence<TInterval>> TestTrueLessEqualThan_AxLeqK<TEnv, TVar, TExpr, TInterval>
 371                                 (Polynomial<TVar, TExpr> poly, TEnv env, IDictionary<TVar, Sequence<TInterval>> result, out bool isBottom)
 372                                 where TEnv : IIntervalEnvironment<TVar, TExpr, TInterval, Rational>
 373                                 where TVar : IEquatable<TVar>
 374                                 where TInterval : IntervalBase<TInterval, Rational>
 375                         {
 376                                 isBottom = false;
 377
 378                                 var ax = poly.Left[0];
 379                                 var k = poly.Right[1];
 380                                 if (ax.IsConstant) {
 381                                         if (ax.Coeff > k.Coeff) {
 382                                                 isBottom = true;
 383                                                 return result;
 384                                         }
 385                                 }
 386                                 else {
 387                                         TVar x;
 388                                         ax.IsSingleVariable (out x);
 389                                         Rational div;
 390                                         if (Rational.TryDivide (k.Coeff, ax.Coeff, out div)) {
 391                                                 var intv = env.Eval (x);
 392
 393                                                 var refined = ax.Coeff.Sign < 1
 394                                                                       ? intv.Meet (env.Context.For (div, Rational.PlusInfinity))
 395                                                                       : intv.Meet (env.Context.For (Rational.MinusInfinity, div));
 396
 397                                                 AddToResult (result, x, refined);
 398                                         }
 399                                 }
 400
 401                                 return result;
 402                         }
 403
 404                         /// <summary>
 405                         /// Get constraints for variables from polynome in form 'a*x &lt;= k'
 406                         /// </summary>
 407                         /// <param name="poly">Polynome in canonical form. Two monomes involved. </param>
 408                         static IDictionary<TVar, Sequence<TInterval>> TestTrueLessEqualThan_AxLtK<TEnv, TVar, TExpr, TInterval>
 409                                 (Polynomial<TVar, TExpr> poly, TEnv env, IDictionary<TVar, Sequence<TInterval>> result, out bool isBottom)
 410                                 where TEnv : IIntervalEnvironment<TVar, TExpr, TInterval, Rational>
 411                                 where TVar : IEquatable<TVar>
 412                                 where TInterval : IntervalBase<TInterval, Rational>
 413                         {
 414                                 isBottom = false;
 415
 416                                 var ax = poly.Left[0];
 417                                 var k = poly.Right[1];
 418                                 if (ax.IsConstant) {
 419                                         if (ax.Coeff >= k.Coeff) {
 420                                                 isBottom = true;
 421                                                 return result;
 422                                         }
 423                                 }
 424                                 else {
 425                                         TVar x;
 426                                         ax.IsSingleVariable (out x);
 427                                         Rational div;
 428                                         if (Rational.TryDivide (k.Coeff, ax.Coeff, out div)) {
 429                                                 var intv = env.Eval (x);
 430
 431                                                 var boundByDivPlus = !div.IsInteger
 432                                                                              ? env.Context.For (div.NextInt32, Rational.PlusInfinity)
 433                                                                              : env.Context.For (div + 1L, Rational.PlusInfinity);
 434                                                 var boundByDivMinus = !div.IsInteger
 435                                                                               ? env.Context.For (Rational.MinusInfinity, div.NextInt32 - 1L)
 436                                                                               : env.Context.For (Rational.MinusInfinity, div - 1L);
 437                                                 var refined = intv.Meet (ax.Coeff.Sign < 1 ? boundByDivPlus : boundByDivMinus);
 438
 439                                                 if (refined.IsBottom) {
 440                                                         isBottom = true;
 441                                                         return result;
 442                                                 }
 443
 444                                                 AddToResult (result, x, refined);
 445                                         }
 446                                 }
 447                                 return result;
 448                         }
 449
 450                         static bool BoundVariable<TVar, TInterval>
 451                                 (IntervalContextBase<TInterval, Rational> ctx, Rational a, TInterval xIntervalOld, TInterval boundingInterval, TVar x,
 452                                  IDictionary<TVar, Sequence<TInterval>> result, out bool isBottom,
 453                                  Func<Rational, TInterval> upperBounded, Func<Rational, TInterval> lowerBounded)
 454                                 where TVar : IEquatable<TVar>
 455                                 where TInterval : IntervalBase<TInterval, Rational>
 456                         {
 457                                 isBottom = false;
 458                                 if (a.IsZero) {
 459                                         TInterval boundingForVariable;
 460                                         if (a.Sign > 0L)
 461                                                 boundingForVariable = upperBounded (boundingInterval.UpperBound);
 462                                         else
 463                                                 boundingForVariable = lowerBounded (boundingInterval.LowerBound);
 464
 465                                         var refined = xIntervalOld.Meet (boundingForVariable);
 466                                         if (refined.IsBottom) {
 467                                                 isBottom = true;
 468                                                 return true;
 469                                         }
 470
 471                                         AddToResult (result, x, refined);
 472                                 }
 473                                 return false;
 474                         }
 475
 476                         static bool IsFloat<TVar, TExpr> (TExpr expr, IExpressionDecoder<TVar, TExpr> decoder)
 477                         {
 478                                 if (decoder == null)
 479                                         return false;
 480
 481                                 var type = decoder.TypeOf (expr);
 482                                 return type == ExpressionType.Float32 || type == ExpressionType.Float64;
 483                         }
 484
 485                         static void AddToResult<TVar, TInterval> (IDictionary<TVar, Sequence<TInterval>> result, TVar variable, TInterval intv)
 486                                 where TVar : IEquatable<TVar>
 487                                 where TInterval : IntervalBase<TInterval, Rational>
 488                         {
 489                                 Sequence<TInterval> value;
 490                                 result.TryGetValue (variable, out value);
 491
 492                                 result[variable] = value.Cons (intv);
 493                         }
 494                 }
 495
 496                 public struct InferenceResult<TVar, TInterval>
 497                         where TInterval : IAbstractDomain<TInterval>
 498                         where TVar : IEquatable<TVar> {
 499                         public static readonly InferenceResult<TVar, TInterval> Empty =
 500                                 new InferenceResult<TVar, TInterval> (false, ImmutableMap<TVar, Sequence<TInterval>>.Empty);
 501
 502                         public readonly bool IsBottom;
 503
 504                         public readonly IImmutableMap<TVar, Sequence<TInterval>> Constraints;
 505
 506                         InferenceResult (bool isbottom, IImmutableMap<TVar, Sequence<TInterval>> map)
 507                         {
 508                                 Constraints = map;
 509                                 IsBottom = isbottom;
 510                         }
 511
 512                         public InferenceResult<TVar, TInterval> AddConstraintFor (TVar rightVar, TInterval refined)
 513                         {
 514                                 Sequence<TInterval> seq;
 515                                 Constraints.TryGetValue (rightVar, out seq);
 516
 517                                 return new InferenceResult<TVar, TInterval> (IsBottom, Constraints.Add (rightVar, seq.Cons (refined)));
 518                         }
 519
 520                         public InferenceResult<TVar, TInterval> Join (InferenceResult<TVar, TInterval> that)
 521                         {
 522                                 if (IsBottom)
 523                                         return that;
 524                                 if (that.IsBottom)
 525                                         return this;
 526
 527                                 var result = Empty;
 528                                 foreach (var var in Constraints.Keys) {
 529                                         var leftContraints = Constraints[var];
 530                                         if (leftContraints == null)
 531                                                 continue;
 532
 533                                         // tops are not included
 534                                         Sequence<TInterval> rightConstraints;
 535                                         if (that.Constraints.TryGetValue (var, out rightConstraints) && rightConstraints != null) {
 536                                                 var intv = leftContraints.Head.Join (rightConstraints.Head);
 537                                                 if (!intv.IsTop)
 538                                                         result.AddConstraintFor (var, intv);
 539                                         }
 540                                 }
 541
 542                                 return result;
 543                         }
 544                  }
 545         }
 546 }