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

   1 //
   2 // Polynomial.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 using System.Diagnostics;
  32 using System.Linq;
  33 using System.Text;
  34 using System.Threading;
  35
  36 using Mono.CodeContracts.Static.DataStructures;
  37
  38 namespace Mono.CodeContracts.Static.Analysis.Numerical {
  39         struct Polynomial<TVar, TExpr>
  40                 where TVar : IEquatable<TVar> {
  41                 readonly Monomial<TVar>[] left;
  42                 readonly ExpressionOperator? relation;
  43                 readonly Monomial<TVar>[] right;
  44                 IImmutableSet<TVar> cached_variables;
  45
  46                 public Polynomial (Monomial<TVar> monome)
  47                 {
  48                         relation = null;
  49                         left = new[] {monome};
  50                         right = null;
  51
  52                         cached_variables = null;
  53                 }
  54
  55                 public Polynomial (Monomial<TVar>[] monomes)
  56                 {
  57                         relation = null;
  58                         left = monomes;
  59                         right = null;
  60
  61                         cached_variables = null;
  62                 }
  63
  64                 public Polynomial (ExpressionOperator op, Monomial<TVar>[] left, Monomial<TVar>[] right)
  65                 {
  66                         relation = op;
  67                         this.left = left;
  68                         this.right = right;
  69
  70                         cached_variables = null;
  71                 }
  72
  73                 public Polynomial (ExpressionOperator op, Monomial<TVar>[] left, Monomial<TVar> right)
  74                 {
  75                         relation = op;
  76                         this.left = left;
  77                         this.right = new[] {right};
  78
  79                         cached_variables = null;
  80                 }
  81
  82                 public Polynomial (ExpressionOperator op, Polynomial<TVar, TExpr> left, Polynomial<TVar, TExpr> right)
  83                 {
  84                         relation = op;
  85                         this.left = left.left;
  86                         this.right = right.left;
  87
  88                         cached_variables = null;
  89                 }
  90
  91                 public Polynomial (Polynomial<TVar, TExpr> that)
  92                 {
  93                         relation = that.relation;
  94                         left = DuplicateFrom (that.left);
  95                         right = that.right != null ? DuplicateFrom (that.right) : null;
  96
  97                         cached_variables = null;
  98                 }
  99
 100                 public ExpressionOperator? Relation { get { return relation; } }
 101
 102                 public IImmutableSet<TVar> Variables
 103                 {
 104                         get
 105                         {
 106                                 if (cached_variables == null) {
 107                                         cached_variables = ImmutableSet<TVar>.Empty ();
 108                                         foreach (var monome in left)
 109                                                 cached_variables = cached_variables.AddRange (monome.Variables);
 110                                         if (relation.HasValue)
 111                                                 foreach (var monome in right)
 112                                                         cached_variables = cached_variables.AddRange (monome.Variables);
 113                                 }
 114
 115                                 return cached_variables;
 116                         }
 117                 }
 118
 119                 public Monomial<TVar>[] Left { get { return left; } }
 120                 public Monomial<TVar>[] Right { get { return right; } }
 121
 122                 public Polynomial<TVar, TExpr> LeftAsPolynomial
 123                 {
 124                         get
 125                         {
 126                                 Polynomial<TVar, TExpr> polynome;
 127                                 TryToPolynomial (left, out polynome);
 128                                 return polynome;
 129                         }
 130                 }
 131
 132                 /// <summary>
 133                 /// Returns true if poly is in form: 'k*x &lt; c'
 134                 /// </summary>
 135                 public bool IsIntervalForm
 136                 {
 137                         get
 138                         {
 139                                 var op = Relation;
 140
 141                                 if (!op.HasValue)
 142                                         return false;
 143                                 if (left.Length != 1 || right.Length != 1 || left[0].Degree != 1 || !right[0].IsConstant)
 144                                         return false;
 145
 146                                 return op.Value == ExpressionOperator.LessEqualThan;
 147                         }
 148                 }
 149
 150                 public bool IsLinear
 151                 {
 152                         get
 153                         {
 154                                 if (left.Any (m => !m.IsLinear))
 155                                         return false;
 156                                 if (Relation.HasValue && right.Any (m => !m.IsLinear))
 157                                         return false;
 158                                 return true;
 159                         }
 160                 }
 161
 162                 static Monomial<TVar>[] DuplicateFrom (Monomial<TVar>[] original)
 163                 {
 164                         var res = new Monomial<TVar>[original.Length];
 165                         Array.Copy (original, res, original.Length);
 166                         return res;
 167                 }
 168
 169                 public static bool TryToPolynomial (Monomial<TVar>[] monomials, out Polynomial<TVar, TExpr> polynome)
 170                 {
 171                         if (monomials.Length > 1) {
 172                                 polynome = new Polynomial<TVar, TExpr> (monomials);
 173                                 return polynome.TryToCanonicalForm (out polynome);
 174                         }
 175
 176                         return true.With (new Polynomial<TVar, TExpr> (monomials), out polynome);
 177                 }
 178
 179                 public bool TryToCanonicalForm (out Polynomial<TVar, TExpr> polynome)
 180                 {
 181                         var poly = this;
 182                         if (poly.relation.HasValue) {
 183                                 switch (poly.relation.Value) {
 184                                 case ExpressionOperator.GreaterThan:
 185                                         poly = poly.SwapOperands (ExpressionOperator.LessThan);
 186                                         break;
 187                                 case ExpressionOperator.GreaterEqualThan:
 188                                         poly = poly.SwapOperands (ExpressionOperator.LessEqualThan);
 189                                         break;
 190                                 }
 191
 192                                 poly = poly.MoveConstantsAndMonomes ();
 193                                 Debug.Assert (poly.relation.HasValue);
 194
 195                                 Monomial<TVar>[] left;
 196                                 Monomial<TVar>[] right;
 197                                 if (TrySimplifyMonomes (poly.left, out left) && TrySimplifyMonomes (poly.right, out right))
 198                                         return true.With (new Polynomial<TVar, TExpr> (poly.relation.Value, left, right), out polynome);
 199                         }
 200                         else {
 201                                 Monomial<TVar>[] monome;
 202                                 if (TrySimplifyMonomes (left, out monome))
 203                                         return true.With (new Polynomial<TVar, TExpr> (monome), out polynome);
 204                         }
 205
 206                         return false.Without (out polynome);
 207                 }
 208
 209                 static bool TrySimplifyMonomes (Monomial<TVar>[] monomes, out Monomial<TVar>[] result)
 210                 {
 211                         if (monomes.Length <= 1)
 212                                 return true.With (monomes, out result);
 213
 214                         var dict = new Dictionary<ListEqual<TVar>, Monomial<TVar>> ();
 215                         foreach (var monomial in monomes) {
 216                                 var key = new ListEqual<TVar> (monomial.Degree, monomial.Variables);
 217                                 Monomial<TVar> monome;
 218                                 if (dict.TryGetValue (key, out monome)) {
 219                                         Rational coeff;
 220                                         if (!Rational.TryAdd (monome.Coeff, monomial.Coeff, out coeff))
 221                                                 return false.With (monomes, out result);
 222
 223                                         var sum = monome.With (coeff);
 224                                         dict[key] = sum;
 225                                 }
 226                                 else
 227                                         dict.Add (key, monomial);
 228                         }
 229
 230                         var left = new List<Monomial<TVar>> (dict.Count);
 231                         var right = new List<Monomial<TVar>> (dict.Count);
 232
 233                         Monomial<TVar>? resMonome = null;
 234                         foreach (var pair in dict) {
 235                                 var monome = pair.Value;
 236                                 if (!monome.Coeff.IsZero) {
 237                                         if (monome.IsConstant)
 238                                                 resMonome = monome;
 239                                         else if (monome.Coeff > 0L)
 240                                                 left.Add (monome);
 241                                         else
 242                                                 right.Add (monome);
 243                                 }
 244                         }
 245
 246                         var list = new List<Monomial<TVar>> (dict.Count);
 247                         list.AddRange (left);
 248                         list.AddRange (right);
 249
 250                         if (resMonome.HasValue)
 251                                 list.Add (resMonome.Value);
 252                         if (list.Count == 0)
 253                                 list.Add (Monomial<TVar>.From (Rational.Zero));
 254
 255                         return true.With (list.ToArray (), out result);
 256                 }
 257
 258                 Polynomial<TVar, TExpr> MoveConstantsAndMonomes ()
 259                 {
 260                         if (!relation.HasValue)
 261                                 return this;
 262
 263                         var left = new List<Monomial<TVar>> ();
 264                         var right = new List<Monomial<TVar>> ();
 265
 266                         foreach (var monomial in this.left)
 267                                 if (!monomial.IsConstant)
 268                                         left.Add (monomial);
 269                                 else
 270                                         right.Add (-monomial);
 271
 272                         foreach (var monomial in this.right)
 273                                 if (!monomial.IsConstant)
 274                                         left.Add (-monomial);
 275                                 else
 276                                         right.Add (monomial);
 277
 278                         if (left.Count == 0)
 279                                 left.Add (Monomial<TVar>.From (0L));
 280                         if (right.Count == 0)
 281                                 right.Add (Monomial<TVar>.From (0));
 282
 283                         return new Polynomial<TVar, TExpr> (relation.Value, left.ToArray (), right.ToArray ());
 284                 }
 285
 286                 Polynomial<TVar, TExpr> SwapOperands (ExpressionOperator newOp)
 287                 {
 288                         return new Polynomial<TVar, TExpr> (newOp, right, left);
 289                 }
 290
 291                 public override string ToString ()
 292                 {
 293                         if (!relation.HasValue)
 294                                 return ListToString (left);
 295
 296                         return string.Format ("{0} {1} {2}", ListToString (left), relation, ListToString (right));
 297                 }
 298
 299                 static string ListToString (Monomial<TVar>[] list)
 300                 {
 301                         if (list == null)
 302                                 return string.Empty;
 303                         if (list.Length == 0)
 304                                 return "()";
 305
 306                         var sb = new StringBuilder ();
 307
 308                         var stringsOrdered = list.Select (x => x.ToString ()).OrderBy (x => x);
 309                         var first = true;
 310                         sb.Append ("(");
 311                         foreach (var str in stringsOrdered) {
 312                                 if (first)
 313                                         first = false;
 314                                 else
 315                                         sb.Append (", ");
 316                                 sb.Append (str);
 317                         }
 318                         sb.Append (")");
 319
 320                         return sb.ToString ();
 321                 }
 322
 323                 public static bool TryReduceCoefficients (Monomial<TVar>[] simplifiedLeft, Monomial<TVar>[] simplifiedRight)
 324                 {
 325                         if (simplifiedRight[0].Coeff.IsMinValue)
 326                                 return false;
 327
 328                         var abs = Rational.Abs (simplifiedRight[0].Coeff);
 329                         if (abs.IsZero)
 330                                 return true;
 331
 332                         if (simplifiedLeft.Any (monome => !(monome.Coeff / abs).IsInteger))
 333                                 return true;
 334
 335                         simplifiedRight[0] = simplifiedRight[0].With ((c) => c / abs);
 336                         for (var i = 0; i < simplifiedLeft.Length; i++)
 337                                 simplifiedLeft[i] = simplifiedLeft[i].With (c => c / abs);
 338
 339                         return true;
 340                 }
 341
 342                 public static bool TryBuildFrom (TExpr expr, IExpressionDecoder<TVar, TExpr> decoder, out Polynomial<TVar, TExpr> result)
 343                 {
 344                         return new PolynomialBuilder (decoder).Build (expr, out result);
 345                 }
 346
 347                 static bool TryMinus (Polynomial<TVar, TExpr> p, out Polynomial<TVar, TExpr> result)
 348                 {
 349                         if (p.Relation.HasValue)
 350                                 return false.Without (out result);
 351
 352                         var monomes = new Monomial<TVar>[p.left.Length];
 353                         var cnt = 0;
 354                         foreach (var m in p.left) {
 355                                 var k = -m.Coeff;
 356                                 if (k.IsInfinity)
 357                                         return false.Without (out result);
 358
 359                                 var mm = m.With (k);
 360                                 monomes[cnt++] = mm;
 361                         }
 362
 363                         return true.With (new Polynomial<TVar, TExpr> (monomes), out result);
 364                 }
 365
 366                 bool IsIntConstant (out long constant)
 367                 {
 368                         if (Relation.HasValue || left.Length != 1)
 369                                 return false.Without (out constant);
 370
 371                         return left[0].IsIntConstant (out constant);
 372                 }
 373
 374                 static Polynomial<TVar, TExpr> Concatenate (Polynomial<TVar, TExpr> left, Polynomial<TVar, TExpr> right)
 375                 {
 376                         if (left.Relation.HasValue || right.Relation.HasValue)
 377                                 throw new InvalidOperationException ();
 378
 379                         var monomes = new Monomial<TVar>[left.left.Length + right.left.Length];
 380
 381                         Array.Copy (left.left, monomes, left.left.Length);
 382                         Array.Copy (right.left, 0, monomes, left.left.Length, right.left.Length);
 383
 384                         return new Polynomial<TVar, TExpr> (left.left);
 385                 }
 386
 387                 public static bool TryToPolynomial (ExpressionOperator op, Polynomial<TVar, TExpr> left, Polynomial<TVar, TExpr> right, out Polynomial<TVar, TExpr> result)
 388                 {
 389                         if (op.IsBinary () && !left.Relation.HasValue) {
 390                                 try {
 391                                         var poly = new Polynomial<TVar, TExpr> (op, left, right);
 392                                         if (poly.TryToCanonicalForm (out result))
 393                                                 return true;
 394                                 }
 395                                 catch (Exception) {
 396                                 }
 397                         }
 398
 399                         return false.Without (out result);
 400                 }
 401
 402                 #region Nested type: ConstantGatherer
 403
 404                 class ConstantGatherer : GenericTypeExpressionVisitor<TVar, TExpr, Dummy, Pair<Rational, bool>> {
 405                         static readonly Pair<Rational, bool> Failure = new Pair<Rational, bool> (Rational.PlusInfinity, false);
 406
 407                         public ConstantGatherer (IExpressionDecoder<TVar, TExpr> decoder)
 408                                 : base (decoder)
 409                         {
 410                         }
 411
 412                         protected override Pair<Rational, bool> Default (TExpr expr, Dummy input)
 413                         {
 414                                 if (Decoder.IsNull (expr))
 415                                         return Success (Rational.Zero);
 416
 417                                 return Failure;
 418                         }
 419
 420                         protected override Pair<Rational, bool> VisitBool (TExpr expr, Dummy input)
 421                         {
 422                                 return Failure;
 423                         }
 424
 425                         protected override Pair<Rational, bool> VisitInt32 (TExpr expr, Dummy input)
 426                         {
 427                                 int value;
 428                                 if (Decoder.TryValueOf (expr, ExpressionType.Int32, out value))
 429                                         return Success (Rational.For (value));
 430
 431                                 return Failure;
 432                         }
 433
 434                         static Pair<Rational, bool> Success (Rational value)
 435                         {
 436                                 return new Pair<Rational, bool> (value, true);
 437                         }
 438                 }
 439
 440                 #endregion
 441
 442                 #region Nested type: ListEqual
 443
 444                 class ListEqual<T> {
 445                         readonly Lazy<int> cached_hash_code;
 446                         readonly T[] elements;
 447
 448                         public ListEqual (int len, IEnumerable<T> seq)
 449                         {
 450                                 elements = seq.Take (len).ToArray ();
 451                                 cached_hash_code = new Lazy<int> (() => elements.Sum (elem => elem.GetHashCode ()), LazyThreadSafetyMode.None);
 452                         }
 453
 454                         public override int GetHashCode ()
 455                         {
 456                                 return cached_hash_code.Value;
 457                         }
 458
 459                         public override bool Equals (object obj)
 460                         {
 461                                 var leq = obj as ListEqual<T>;
 462                                 if (leq == null || elements.Length != leq.elements.Length)
 463                                         return false;
 464
 465                                 if (elements.Length == 1)
 466                                         return elements[0].Equals (leq.elements[0]);
 467
 468                                 return elements.Intersect (leq.elements).Count () == elements.Count ();
 469                         }
 470                 }
 471
 472                 #endregion
 473
 474                 #region Nested type: PolynomialBuilder
 475
 476                 class PolynomialBuilder : GenericExpressionVisitor<Dummy, bool, TVar, TExpr> {
 477                         Polynomial<TVar, TExpr> poly;
 478
 479                         public PolynomialBuilder (IExpressionDecoder<TVar, TExpr> decoder)
 480                                 : base (decoder)
 481                         {
 482                         }
 483
 484                         public bool Build (TExpr expr, out Polynomial<TVar, TExpr> result)
 485                         {
 486                                 if (base.Visit (expr, Dummy.Value))
 487                                         return true.With (poly, out result);
 488
 489                                 return false.Without (out result);
 490                         }
 491
 492                         protected override bool Default (Dummy data)
 493                         {
 494                                 return false;
 495                         }
 496
 497                         public override bool VisitSizeOf (TExpr expr, Dummy data)
 498                         {
 499                                 int sizeOf;
 500                                 if (!Decoder.TrySizeOf (expr, out sizeOf))
 501                                         return false;
 502
 503                                 return true.With (new Polynomial<TVar, TExpr> (Monomial<TVar>.From (Rational.For (sizeOf))), out poly);
 504                         }
 505
 506                         public override bool VisitConstant (TExpr expr, Dummy data)
 507                         {
 508                                 var pair = new ConstantGatherer (Decoder).Visit (expr, Dummy.Value);
 509                                 if (!pair.Value || pair.Key.IsInfinity)
 510                                         return false;
 511
 512                                 poly = new Polynomial<TVar, TExpr> (Monomial<TVar>.From (pair.Key));
 513                                 return true;
 514                         }
 515
 516                         public override bool VisitAddition (TExpr left, TExpr right, TExpr original, Dummy data)
 517                         {
 518                                 Polynomial<TVar, TExpr> polyLeft, polyRight;
 519                                 if (!Build (left, out polyLeft) || !Build (right, out polyRight))
 520                                         return false;
 521
 522                                 long kLeft, kRight;
 523                                 object addition;
 524                                 if (polyLeft.IsIntConstant (out kLeft) && polyRight.IsIntConstant (out kRight) &&
 525                                     EvaluateArithmeticWithOverflow.TryBinary (Decoder.TypeOf (original), ExpressionOperator.Add, kLeft, kRight, out addition)) {
 526                                         var longValue = addition.ConvertToLong ();
 527                                         if (longValue.HasValue)
 528                                                 return true.With (new Polynomial<TVar, TExpr> (Monomial<TVar>.From (Rational.For (longValue.Value))), out poly);
 529                                 }
 530                                 return true.With (Concatenate (polyLeft, polyRight), out poly);
 531                         }
 532
 533                         public override bool VisitSubtraction (TExpr left, TExpr right, TExpr original, Dummy data)
 534                         {
 535                                 Polynomial<TVar, TExpr> polyLeft, polyRight;
 536                                 if (!Build (left, out polyLeft) || !Build (right, out polyRight))
 537                                         return false;
 538
 539                                 long kLeft, kRight;
 540                                 object subtraction;
 541                                 if (polyLeft.IsIntConstant (out kLeft) && polyRight.IsIntConstant (out kRight) &&
 542                                     EvaluateArithmeticWithOverflow.TryBinary (Decoder.TypeOf (original), ExpressionOperator.Sub, kLeft, kRight, out subtraction)) {
 543                                         var longValue = subtraction.ConvertToLong ();
 544                                         if (longValue.HasValue)
 545                                                 return true.With (new Polynomial<TVar, TExpr> (Monomial<TVar>.From (Rational.For (longValue.Value))), out poly);
 546                                 }
 547                                 return TryToPolynomialHelperForSubtraction (polyLeft, polyRight, out poly);
 548                         }
 549
 550                         public override bool VisitMultiply (TExpr left, TExpr right, TExpr original, Dummy data)
 551                         {
 552                                 Polynomial<TVar, TExpr> l, r;
 553                                 var lBuilt = Build (left, out l);
 554                                 var rBuilt = Build (right, out r);
 555
 556                                 if (lBuilt && rBuilt) {
 557                                         long kLeft, kRight;
 558                                         object mult;
 559                                         if (l.IsIntConstant (out kLeft) && r.IsIntConstant (out kRight) &&
 560                                             EvaluateArithmeticWithOverflow.TryBinary (
 561                                                     Decoder.TypeOf (original), ExpressionOperator.Mult, kLeft, kRight, out mult)) {
 562                                                 var longValue = mult.ConvertToLong ();
 563                                                 if (longValue.HasValue) {
 564                                                         var monomial = Monomial<TVar>.From (Rational.For (longValue.Value));
 565                                                         return true.With (new Polynomial<TVar, TExpr> (monomial), out poly);
 566                                                 }
 567                                         }
 568                                         return TryToPolynomialHelperForMultiplication (l, r, out poly);
 569                                 }
 570                                 return false;
 571                         }
 572
 573                         static bool TryToPolynomialHelperForMultiplication (Polynomial<TVar, TExpr> left, Polynomial<TVar, TExpr> right, out Polynomial<TVar, TExpr> result)
 574                         {
 575                                 var list = new List<Monomial<TVar>> (left.left.Length + right.left.Length);
 576                                 foreach (var m in left.left)
 577                                         foreach (var n in right.left) {
 578                                                 Rational mul;
 579                                                 if (!Rational.TryMultiply (m.Coeff, n.Coeff, out mul))
 580                                                         return false.Without (out result);
 581
 582                                                 list.Add (Monomial<TVar>.From (mul, m.Variables.Concat (n.Variables)));
 583                                         }
 584
 585                                 return true.With (new Polynomial<TVar, TExpr> (list.ToArray ()), out result);
 586                         }
 587
 588                         static bool TryToPolynomialHelperForSubtraction (Polynomial<TVar, TExpr> left, Polynomial<TVar, TExpr> right, out Polynomial<TVar, TExpr> result)
 589                         {
 590                                 Polynomial<TVar, TExpr> minusRight;
 591                                 if (TryMinus (right, out minusRight))
 592                                         return true.With (Concatenate (left, right), out result);
 593
 594                                 return false.Without (out result);
 595                         }
 596
 597                         public override bool VisitVariable (TVar var, TExpr expr, Dummy data)
 598                         {
 599                                 var monome = Monomial<TVar>.From (Rational.One, Sequence<TVar>.Singleton (Decoder.UnderlyingVariable (expr)));
 600
 601                                 return true.With (new Polynomial<TVar, TExpr> (monome), out poly);
 602                         }
 603
 604                         public override bool VisitNotEqual (TExpr left, TExpr right, TExpr original, Dummy data)
 605                         {
 606                                 return DefaultRelation (left, right, original);
 607                         }
 608
 609                         public override bool VisitLessThan (TExpr left, TExpr right, TExpr original, Dummy data)
 610                         {
 611                                 return DefaultRelation (left, right, original);
 612                         }
 613
 614                         public override bool VisitLessEqualThan (TExpr left, TExpr right, TExpr original, Dummy data)
 615                         {
 616                                 return DefaultRelation (left, right, original);
 617                         }
 618
 619                         public override bool VisitGreaterThan (TExpr left, TExpr right, TExpr original, Dummy data)
 620                         {
 621                                 return DefaultRelation (left, right, original);
 622                         }
 623
 624                         public override bool VisitGreaterEqualThan (TExpr left, TExpr right, TExpr original, Dummy data)
 625                         {
 626                                 return DefaultRelation (left, right, original);
 627                         }
 628
 629                         public override bool VisitDivision (TExpr left, TExpr right, TExpr original, Dummy data)
 630                         {
 631                                 Polynomial<TVar, TExpr> l, r;
 632                                 if (!Build (left, out l) || !Build (right, out r))
 633                                         return false;
 634
 635                                 return HelperForDivision (l, r, out poly);
 636                         }
 637
 638                         bool HelperForDivision (Polynomial<TVar, TExpr> left, Polynomial<TVar, TExpr> right, out Polynomial<TVar, TExpr> result)
 639                         {
 640                                 if (right.left.Length == 1) {
 641                                         var div = right.left[0];
 642
 643                                         if (div.IsConstant && !div.Coeff.IsZero) {
 644                                                 var monomes = new Monomial<TVar>[left.left.Length];
 645                                                 var cnt = 0;
 646                                                 foreach (var m in left.left) {
 647                                                         Rational k;
 648                                                         try {
 649                                                                 k = m.Coeff / div.Coeff;
 650                                                         }
 651                                                         catch (ArithmeticException) {
 652                                                                 return false.Without (out result);
 653                                                         }
 654
 655                                                         monomes[cnt++] = m.With (k);
 656                                                 }
 657
 658                                                 return true.With (new Polynomial<TVar, TExpr> (monomes), out result);
 659                                         }
 660                                 }
 661
 662                                 return false.Without (out result);
 663                         }
 664
 665                         bool DefaultRelation (TExpr left, TExpr right, TExpr original)
 666                         {
 667                                 Polynomial<TVar, TExpr> l, r;
 668                                 if (!Build (left, out l) || !Build (right, out r) || l.Relation.HasValue || r.Relation.HasValue)
 669                                         return false;
 670
 671                                 return true.With (new Polynomial<TVar, TExpr> (Decoder.OperatorFor (original), l.left, r.left), out poly);
 672                         }
 673                 }
 674
 675                 #endregion
 676                 }
 677 }