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
;
31 using System
.Diagnostics
;
34 using System
.Threading
;
36 using Mono
.CodeContracts
.Static
.DataStructures
;
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
;
46 public Polynomial (Monomial
<TVar
> monome
)
49 left
= new[] {monome}
;
52 cached_variables
= null;
55 public Polynomial (Monomial
<TVar
>[] monomes
)
61 cached_variables
= null;
64 public Polynomial (ExpressionOperator op
, Monomial
<TVar
>[] left
, Monomial
<TVar
>[] right
)
70 cached_variables
= null;
73 public Polynomial (ExpressionOperator op
, Monomial
<TVar
>[] left
, Monomial
<TVar
> right
)
77 this.right
= new[] {right}
;
79 cached_variables
= null;
82 public Polynomial (ExpressionOperator op
, Polynomial
<TVar
, TExpr
> left
, Polynomial
<TVar
, TExpr
> right
)
85 this.left
= left
.left
;
86 this.right
= right
.left
;
88 cached_variables
= null;
91 public Polynomial (Polynomial
<TVar
, TExpr
> that
)
93 relation
= that
.relation
;
94 left
= DuplicateFrom (that
.left
);
95 right
= that
.right
!= null ? DuplicateFrom (that
.right
) : null;
97 cached_variables
= null;
100 public ExpressionOperator
? Relation { get { return relation; }
}
102 public IImmutableSet
<TVar
> Variables
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
);
115 return cached_variables
;
119 public Monomial
<TVar
>[] Left { get { return left; }
}
120 public Monomial
<TVar
>[] Right { get { return right; }
}
122 public Polynomial
<TVar
, TExpr
> LeftAsPolynomial
126 Polynomial
<TVar
, TExpr
> polynome
;
127 TryToPolynomial (left
, out polynome
);
133 /// Returns true if poly is in form: 'k*x < c'
135 public bool IsIntervalForm
143 if (left
.Length
!= 1 || right
.Length
!= 1 || left
[0].Degree
!= 1 || !right
[0].IsConstant
)
146 return op
.Value
== ExpressionOperator
.LessEqualThan
;
154 if (left
.Any (m
=> !m
.IsLinear
))
156 if (Relation
.HasValue
&& right
.Any (m
=> !m
.IsLinear
))
162 static Monomial
<TVar
>[] DuplicateFrom (Monomial
<TVar
>[] original
)
164 var res
= new Monomial
<TVar
>[original
.Length
];
165 Array
.Copy (original
, res
, original
.Length
);
169 public static bool TryToPolynomial (Monomial
<TVar
>[] monomials
, out Polynomial
<TVar
, TExpr
> polynome
)
171 if (monomials
.Length
> 1) {
172 polynome
= new Polynomial
<TVar
, TExpr
> (monomials
);
173 return polynome
.TryToCanonicalForm (out polynome
);
176 return true.With (new Polynomial
<TVar
, TExpr
> (monomials
), out polynome
);
179 public bool TryToCanonicalForm (out Polynomial
<TVar
, TExpr
> polynome
)
182 if (poly
.relation
.HasValue
) {
183 switch (poly
.relation
.Value
) {
184 case ExpressionOperator
.GreaterThan
:
185 poly
= poly
.SwapOperands (ExpressionOperator
.LessThan
);
187 case ExpressionOperator
.GreaterEqualThan
:
188 poly
= poly
.SwapOperands (ExpressionOperator
.LessEqualThan
);
192 poly
= poly
.MoveConstantsAndMonomes ();
193 Debug
.Assert (poly
.relation
.HasValue
);
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
);
201 Monomial
<TVar
>[] monome
;
202 if (TrySimplifyMonomes (left
, out monome
))
203 return true.With (new Polynomial
<TVar
, TExpr
> (monome
), out polynome
);
206 return false.Without (out polynome
);
209 static bool TrySimplifyMonomes (Monomial
<TVar
>[] monomes
, out Monomial
<TVar
>[] result
)
211 if (monomes
.Length
<= 1)
212 return true.With (monomes
, out result
);
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
)) {
220 if (!Rational
.TryAdd (monome
.Coeff
, monomial
.Coeff
, out coeff
))
221 return false.With (monomes
, out result
);
223 var sum
= monome
.With (coeff
);
227 dict
.Add (key
, monomial
);
230 var left
= new List
<Monomial
<TVar
>> (dict
.Count
);
231 var right
= new List
<Monomial
<TVar
>> (dict
.Count
);
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
)
239 else if (monome
.Coeff
> 0L)
246 var list
= new List
<Monomial
<TVar
>> (dict
.Count
);
247 list
.AddRange (left
);
248 list
.AddRange (right
);
250 if (resMonome
.HasValue
)
251 list
.Add (resMonome
.Value
);
253 list
.Add (Monomial
<TVar
>.From (Rational
.Zero
));
255 return true.With (list
.ToArray (), out result
);
258 Polynomial
<TVar
, TExpr
> MoveConstantsAndMonomes ()
260 if (!relation
.HasValue
)
263 var left
= new List
<Monomial
<TVar
>> ();
264 var right
= new List
<Monomial
<TVar
>> ();
266 foreach (var monomial
in this.left
)
267 if (!monomial
.IsConstant
)
270 right
.Add (-monomial
);
272 foreach (var monomial
in this.right
)
273 if (!monomial
.IsConstant
)
274 left
.Add (-monomial
);
276 right
.Add (monomial
);
279 left
.Add (Monomial
<TVar
>.From (0L));
280 if (right
.Count
== 0)
281 right
.Add (Monomial
<TVar
>.From (0));
283 return new Polynomial
<TVar
, TExpr
> (relation
.Value
, left
.ToArray (), right
.ToArray ());
286 Polynomial
<TVar
, TExpr
> SwapOperands (ExpressionOperator newOp
)
288 return new Polynomial
<TVar
, TExpr
> (newOp
, right
, left
);
291 public override string ToString ()
293 if (!relation
.HasValue
)
294 return ListToString (left
);
296 return string.Format ("{0} {1} {2}", ListToString (left
), relation
, ListToString (right
));
299 static string ListToString (Monomial
<TVar
>[] list
)
303 if (list
.Length
== 0)
306 var sb
= new StringBuilder ();
308 var stringsOrdered
= list
.Select (x
=> x
.ToString ()).OrderBy (x
=> x
);
311 foreach (var str
in stringsOrdered
) {
320 return sb
.ToString ();
323 public static bool TryReduceCoefficients (Monomial
<TVar
>[] simplifiedLeft
, Monomial
<TVar
>[] simplifiedRight
)
325 if (simplifiedRight
[0].Coeff
.IsMinValue
)
328 var abs
= Rational
.Abs (simplifiedRight
[0].Coeff
);
332 if (simplifiedLeft
.Any (monome
=> !(monome
.Coeff
/ abs
).IsInteger
))
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
);
342 public static bool TryBuildFrom (TExpr expr
, IExpressionDecoder
<TVar
, TExpr
> decoder
, out Polynomial
<TVar
, TExpr
> result
)
344 return new PolynomialBuilder (decoder
).Build (expr
, out result
);
347 static bool TryMinus (Polynomial
<TVar
, TExpr
> p
, out Polynomial
<TVar
, TExpr
> result
)
349 if (p
.Relation
.HasValue
)
350 return false.Without (out result
);
352 var monomes
= new Monomial
<TVar
>[p
.left
.Length
];
354 foreach (var m
in p
.left
) {
357 return false.Without (out result
);
363 return true.With (new Polynomial
<TVar
, TExpr
> (monomes
), out result
);
366 bool IsIntConstant (out long constant
)
368 if (Relation
.HasValue
|| left
.Length
!= 1)
369 return false.Without (out constant
);
371 return left
[0].IsIntConstant (out constant
);
374 static Polynomial
<TVar
, TExpr
> Concatenate (Polynomial
<TVar
, TExpr
> left
, Polynomial
<TVar
, TExpr
> right
)
376 if (left
.Relation
.HasValue
|| right
.Relation
.HasValue
)
377 throw new InvalidOperationException ();
379 var monomes
= new Monomial
<TVar
>[left
.left
.Length
+ right
.left
.Length
];
381 Array
.Copy (left
.left
, monomes
, left
.left
.Length
);
382 Array
.Copy (right
.left
, 0, monomes
, left
.left
.Length
, right
.left
.Length
);
384 return new Polynomial
<TVar
, TExpr
> (left
.left
);
387 public static bool TryToPolynomial (ExpressionOperator op
, Polynomial
<TVar
, TExpr
> left
, Polynomial
<TVar
, TExpr
> right
, out Polynomial
<TVar
, TExpr
> result
)
389 if (op
.IsBinary () && !left
.Relation
.HasValue
) {
391 var poly
= new Polynomial
<TVar
, TExpr
> (op
, left
, right
);
392 if (poly
.TryToCanonicalForm (out result
))
399 return false.Without (out result
);
402 #region Nested type: ConstantGatherer
404 class ConstantGatherer
: GenericTypeExpressionVisitor
<TVar
, TExpr
, Dummy
, Pair
<Rational
, bool>> {
405 static readonly Pair
<Rational
, bool> Failure
= new Pair
<Rational
, bool> (Rational
.PlusInfinity
, false);
407 public ConstantGatherer (IExpressionDecoder
<TVar
, TExpr
> decoder
)
412 protected override Pair
<Rational
, bool> Default (TExpr expr
, Dummy input
)
414 if (Decoder
.IsNull (expr
))
415 return Success (Rational
.Zero
);
420 protected override Pair
<Rational
, bool> VisitBool (TExpr expr
, Dummy input
)
425 protected override Pair
<Rational
, bool> VisitInt32 (TExpr expr
, Dummy input
)
428 if (Decoder
.TryValueOf (expr
, ExpressionType
.Int32
, out value))
429 return Success (Rational
.For (value));
434 static Pair
<Rational
, bool> Success (Rational
value)
436 return new Pair
<Rational
, bool> (value, true);
442 #region Nested type: ListEqual
445 readonly Lazy
<int> cached_hash_code
;
446 readonly T
[] elements
;
448 public ListEqual (int len
, IEnumerable
<T
> seq
)
450 elements
= seq
.Take (len
).ToArray ();
451 cached_hash_code
= new Lazy
<int> (() => elements
.Sum (elem
=> elem
.GetHashCode ()), LazyThreadSafetyMode
.None
);
454 public override int GetHashCode ()
456 return cached_hash_code
.Value
;
459 public override bool Equals (object obj
)
461 var leq
= obj
as ListEqual
<T
>;
462 if (leq
== null || elements
.Length
!= leq
.elements
.Length
)
465 if (elements
.Length
== 1)
466 return elements
[0].Equals (leq
.elements
[0]);
468 return elements
.Intersect (leq
.elements
).Count () == elements
.Count ();
474 #region Nested type: PolynomialBuilder
476 class PolynomialBuilder
: GenericExpressionVisitor
<Dummy
, bool, TVar
, TExpr
> {
477 Polynomial
<TVar
, TExpr
> poly
;
479 public PolynomialBuilder (IExpressionDecoder
<TVar
, TExpr
> decoder
)
484 public bool Build (TExpr expr
, out Polynomial
<TVar
, TExpr
> result
)
486 if (base.Visit (expr
, Dummy
.Value
))
487 return true.With (poly
, out result
);
489 return false.Without (out result
);
492 protected override bool Default (Dummy data
)
497 public override bool VisitSizeOf (TExpr expr
, Dummy data
)
500 if (!Decoder
.TrySizeOf (expr
, out sizeOf
))
503 return true.With (new Polynomial
<TVar
, TExpr
> (Monomial
<TVar
>.From (Rational
.For (sizeOf
))), out poly
);
506 public override bool VisitConstant (TExpr expr
, Dummy data
)
508 var pair
= new ConstantGatherer (Decoder
).Visit (expr
, Dummy
.Value
);
509 if (!pair
.Value
|| pair
.Key
.IsInfinity
)
512 poly
= new Polynomial
<TVar
, TExpr
> (Monomial
<TVar
>.From (pair
.Key
));
516 public override bool VisitAddition (TExpr left
, TExpr right
, TExpr original
, Dummy data
)
518 Polynomial
<TVar
, TExpr
> polyLeft
, polyRight
;
519 if (!Build (left
, out polyLeft
) || !Build (right
, out polyRight
))
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
);
530 return true.With (Concatenate (polyLeft
, polyRight
), out poly
);
533 public override bool VisitSubtraction (TExpr left
, TExpr right
, TExpr original
, Dummy data
)
535 Polynomial
<TVar
, TExpr
> polyLeft
, polyRight
;
536 if (!Build (left
, out polyLeft
) || !Build (right
, out polyRight
))
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
);
547 return TryToPolynomialHelperForSubtraction (polyLeft
, polyRight
, out poly
);
550 public override bool VisitMultiply (TExpr left
, TExpr right
, TExpr original
, Dummy data
)
552 Polynomial
<TVar
, TExpr
> l
, r
;
553 var lBuilt
= Build (left
, out l
);
554 var rBuilt
= Build (right
, out r
);
556 if (lBuilt
&& rBuilt
) {
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
);
568 return TryToPolynomialHelperForMultiplication (l
, r
, out poly
);
573 static bool TryToPolynomialHelperForMultiplication (Polynomial
<TVar
, TExpr
> left
, Polynomial
<TVar
, TExpr
> right
, out Polynomial
<TVar
, TExpr
> result
)
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
) {
579 if (!Rational
.TryMultiply (m
.Coeff
, n
.Coeff
, out mul
))
580 return false.Without (out result
);
582 list
.Add (Monomial
<TVar
>.From (mul
, m
.Variables
.Concat (n
.Variables
)));
585 return true.With (new Polynomial
<TVar
, TExpr
> (list
.ToArray ()), out result
);
588 static bool TryToPolynomialHelperForSubtraction (Polynomial
<TVar
, TExpr
> left
, Polynomial
<TVar
, TExpr
> right
, out Polynomial
<TVar
, TExpr
> result
)
590 Polynomial
<TVar
, TExpr
> minusRight
;
591 if (TryMinus (right
, out minusRight
))
592 return true.With (Concatenate (left
, right
), out result
);
594 return false.Without (out result
);
597 public override bool VisitVariable (TVar
var, TExpr expr
, Dummy data
)
599 var monome
= Monomial
<TVar
>.From (Rational
.One
, Sequence
<TVar
>.Singleton (Decoder
.UnderlyingVariable (expr
)));
601 return true.With (new Polynomial
<TVar
, TExpr
> (monome
), out poly
);
604 public override bool VisitNotEqual (TExpr left
, TExpr right
, TExpr original
, Dummy data
)
606 return DefaultRelation (left
, right
, original
);
609 public override bool VisitLessThan (TExpr left
, TExpr right
, TExpr original
, Dummy data
)
611 return DefaultRelation (left
, right
, original
);
614 public override bool VisitLessEqualThan (TExpr left
, TExpr right
, TExpr original
, Dummy data
)
616 return DefaultRelation (left
, right
, original
);
619 public override bool VisitGreaterThan (TExpr left
, TExpr right
, TExpr original
, Dummy data
)
621 return DefaultRelation (left
, right
, original
);
624 public override bool VisitGreaterEqualThan (TExpr left
, TExpr right
, TExpr original
, Dummy data
)
626 return DefaultRelation (left
, right
, original
);
629 public override bool VisitDivision (TExpr left
, TExpr right
, TExpr original
, Dummy data
)
631 Polynomial
<TVar
, TExpr
> l
, r
;
632 if (!Build (left
, out l
) || !Build (right
, out r
))
635 return HelperForDivision (l
, r
, out poly
);
638 bool HelperForDivision (Polynomial
<TVar
, TExpr
> left
, Polynomial
<TVar
, TExpr
> right
, out Polynomial
<TVar
, TExpr
> result
)
640 if (right
.left
.Length
== 1) {
641 var div
= right
.left
[0];
643 if (div
.IsConstant
&& !div
.Coeff
.IsZero
) {
644 var monomes
= new Monomial
<TVar
>[left
.left
.Length
];
646 foreach (var m
in left
.left
) {
649 k
= m
.Coeff
/ div
.Coeff
;
651 catch (ArithmeticException
) {
652 return false.Without (out result
);
655 monomes
[cnt
++] = m
.With (k
);
658 return true.With (new Polynomial
<TVar
, TExpr
> (monomes
), out result
);
662 return false.Without (out result
);
665 bool DefaultRelation (TExpr left
, TExpr right
, TExpr original
)
667 Polynomial
<TVar
, TExpr
> l
, r
;
668 if (!Build (left
, out l
) || !Build (right
, out r
) || l
.Relation
.HasValue
|| r
.Relation
.HasValue
)
671 return true.With (new Polynomial
<TVar
, TExpr
> (Decoder
.OperatorFor (original
), l
.left
, r
.left
), out poly
);