| | | 1 | | using Microsoft.Z3; |
| | | 2 | | using System; |
| | | 3 | | using System.Collections.Generic; |
| | | 4 | | |
| | | 5 | | namespace NanoCLang.Entities { |
| | | 6 | | /// <summary> |
| | | 7 | | /// Provides a class for sequence indices. |
| | | 8 | | /// </summary> |
| | | 9 | | public class SequenceIndex : Index, IEquatable<SequenceIndex?> { |
| | | 10 | | /// <summary> |
| | | 11 | | /// Creates a new instance of a sequence index that refers to a sequence of offsets starting from <paramref name |
| | | 12 | | /// </summary> |
| | | 13 | | /// <param name="offset">Start offset of the sequence.</param> |
| | | 14 | | /// <param name="step">Increments between the sequence offsets.</param> |
| | 1116 | 15 | | public SequenceIndex(int offset, int step) { |
| | 558 | 16 | | Offset = offset; |
| | 558 | 17 | | Step = step <= 0 ? throw new ArgumentException("Step must be non-negative!") : step; |
| | 558 | 18 | | } |
| | | 19 | | /// <summary> |
| | | 20 | | /// Start offset of the sequence. |
| | | 21 | | /// </summary> |
| | 1057 | 22 | | public int Offset { get; } |
| | | 23 | | /// <summary> |
| | | 24 | | /// Increments between the sequence offsets. |
| | | 25 | | /// </summary> |
| | 964 | 26 | | public int Step { get; } |
| | | 27 | | /// <inheritdoc/> |
| | 24 | 28 | | public override bool CollidesWith(int size, Index index, int otherSize) => index switch { |
| | 24 | 29 | | // Handling Seq cap Sin, also redirected from Sin cap Seq |
| | 12 | 30 | | SingletonIndex i => i.Offset + otherSize > Offset && base.CollidesWith(size, index, otherSize), // No overla |
| | 12 | 31 | | _ => base.CollidesWith(size, index, otherSize) |
| | 24 | 32 | | }; |
| | | 33 | | /// <inheritdoc/> |
| | 34 | 34 | | public override (BoolExpr guard, IntExpr value) SMTPossibleValues(NanoCSMT smt, int size, string prefix) { |
| | 34 | 35 | | var x = smt.Context.MkIntConst($"{prefix}x"); |
| | 34 | 36 | | var i = smt.Context.MkIntConst($"{prefix}i"); |
| | 34 | 37 | | return (smt.Context.MkAnd(i >= 0, i < smt.Context.MkInt(size), x >= 0), (IntExpr)(smt.Context.MkInt(Offset) |
| | 34 | 38 | | } |
| | | 39 | | /// <inheritdoc/> |
| | 220 | 40 | | public override IEnumerable<StringFormatterToken> Tokens(NanoCSourceFormat args) { |
| | 220 | 41 | | yield return Offset.ToString(); |
| | 220 | 42 | | if (args.SpaceBetweenIndexOffsetAndPlus) yield return " "; |
| | 220 | 43 | | yield return "+"; |
| | 220 | 44 | | if (args.SpaceBetweenIndexPlusAndStep) yield return " "; |
| | 220 | 45 | | yield return Step.ToString(); |
| | 220 | 46 | | } |
| | | 47 | | /// <inheritdoc/> |
| | 23 | 48 | | public override bool SubIndex(Index other) => other switch { |
| | 9 | 49 | | ArbitraryIndex _ => true, |
| | 0 | 50 | | SingletonIndex _ => false, |
| | 14 | 51 | | SequenceIndex i => i.IncludesOffset(Offset) && (Step % i.Step == 0), |
| | 0 | 52 | | _ => throw new IllFormedException(this, $"Cannot check for subindex with index of type {other.GetType().Name |
| | 23 | 53 | | }; |
| | | 54 | | /// <inheritdoc/> |
| | 47 | 55 | | public override bool IncludesOffset(int offset) => (offset >= Offset) && ((offset - Offset) % Step == 0); |
| | | 56 | | /// <inheritdoc/> |
| | 11 | 57 | | protected override Index Add(Index right) => right switch { |
| | 7 | 58 | | SingletonIndex i => new SequenceIndex(Offset + i.Offset, Step), |
| | 4 | 59 | | SequenceIndex i => new SequenceIndex(Offset + i.Offset, GCD(Step, i.Step)), |
| | 0 | 60 | | _ => new ArbitraryIndex() |
| | 11 | 61 | | }; |
| | | 62 | | /// <inheritdoc/> |
| | 0 | 63 | | protected override Index Sub(Index right) => right switch { |
| | 0 | 64 | | SingletonIndex i => new SequenceIndex(Offset - i.Offset, Step), |
| | 0 | 65 | | _ => new ArbitraryIndex() |
| | 0 | 66 | | }; |
| | | 67 | | /// <summary> |
| | | 68 | | /// Greatest Common Denominator using Euclidian Algorithm. |
| | | 69 | | /// </summary> |
| | 4 | 70 | | private static int GCD(int a, int b) { |
| | 12 | 71 | | while (b != 0) b = a % (a = b); |
| | 4 | 72 | | return a; |
| | 4 | 73 | | } |
| | | 74 | | /// <inheritdoc/> |
| | 237 | 75 | | public override object Clone() => new SequenceIndex(Offset, Step); |
| | | 76 | | #region Equality checks |
| | | 77 | | /// <inheritdoc/> |
| | 245 | 78 | | public override bool Equals(object? obj) => Equals(obj as SequenceIndex); |
| | | 79 | | /// <inheritdoc/> |
| | 245 | 80 | | public bool Equals(SequenceIndex? other) => !(other is null) && Offset == other.Offset && Step == other.Step; |
| | | 81 | | /// <inheritdoc/> |
| | 0 | 82 | | public override int GetHashCode() => HashCode.Combine(Offset, Step); |
| | | 83 | | /// <inheritdoc/> |
| | 0 | 84 | | public static bool operator ==(SequenceIndex? left, SequenceIndex? right) => EqualityComparer<SequenceIndex?>.De |
| | | 85 | | /// <inheritdoc/> |
| | 0 | 86 | | public static bool operator !=(SequenceIndex? left, SequenceIndex? right) => !(left == right); |
| | | 87 | | #endregion |
| | | 88 | | } |
| | | 89 | | } |