| | | 1 | | using Microsoft.Z3; |
| | | 2 | | using System; |
| | | 3 | | using System.Collections.Generic; |
| | | 4 | | |
| | | 5 | | namespace NanoCLang.Entities { |
| | | 6 | | /// <summary> |
| | | 7 | | /// Provides a class for singleton indices. |
| | | 8 | | /// </summary> |
| | | 9 | | public class SingletonIndex : Index, IEquatable<SingletonIndex?> { |
| | | 10 | | /// <summary> |
| | | 11 | | /// Creates a new instance of a singleton index that refers to one single <paramref name="offset"/>. |
| | | 12 | | /// </summary> |
| | | 13 | | /// <param name="offset">Offset that is referred to.</param> |
| | 1070 | 14 | | public SingletonIndex(int offset) { |
| | 535 | 15 | | Offset = offset; |
| | 535 | 16 | | } |
| | | 17 | | /// <summary> |
| | | 18 | | /// Offset that is referred to. |
| | | 19 | | /// </summary> |
| | 1247 | 20 | | public int Offset { get; } |
| | | 21 | | /// <inheritdoc/> |
| | 57 | 22 | | public override bool CollidesWith(int size, Index index, int otherSize) => index switch { |
| | 57 | 23 | | // Overlapping of half opened intervals [a, b) cap [c, d) |
| | 57 | 24 | | // ==> a < d && b < c |
| | 51 | 25 | | SingletonIndex i => Offset < i.Offset + otherSize && i.Offset < Offset + size, |
| | 57 | 26 | | // Sin cap Seq shall be handled by Seq cap Sin |
| | 6 | 27 | | SequenceIndex i => i.CollidesWith(otherSize, this, size), |
| | 0 | 28 | | _ => base.CollidesWith(size, index, otherSize) |
| | 57 | 29 | | }; |
| | | 30 | | /// <inheritdoc/> |
| | 10 | 31 | | public override (BoolExpr guard, IntExpr value) SMTPossibleValues(NanoCSMT smt, int size, string prefix) { |
| | 10 | 32 | | var i = smt.Context.MkIntConst($"{prefix}i"); |
| | 10 | 33 | | return (smt.Context.MkAnd(i >= 0, i < smt.Context.MkInt(size)), (IntExpr)(smt.Context.MkInt(Offset) + i)); |
| | 10 | 34 | | } |
| | | 35 | | /// <inheritdoc/> |
| | 93 | 36 | | public override IEnumerable<StringFormatterToken> Tokens(NanoCSourceFormat args) { |
| | 93 | 37 | | yield return Offset.ToString(); |
| | 93 | 38 | | } |
| | | 39 | | /// <inheritdoc/> |
| | 11 | 40 | | public override bool IncludesOffset(int offset) => offset == Offset; |
| | | 41 | | /// <inheritdoc/> |
| | 70 | 42 | | public override bool SubIndex(Index other) => other.IncludesOffset(Offset); |
| | | 43 | | /// <inheritdoc/> |
| | 32 | 44 | | protected override Index Add(Index right) => right switch { |
| | 32 | 45 | | SingletonIndex i => new SingletonIndex(Offset + i.Offset), |
| | 0 | 46 | | SequenceIndex i => new SequenceIndex(Offset + i.Offset, i.Step), |
| | 0 | 47 | | _ => new ArbitraryIndex() |
| | 32 | 48 | | }; |
| | | 49 | | /// <inheritdoc/> |
| | 17 | 50 | | protected override Index Sub(Index right) => right switch { |
| | 15 | 51 | | SingletonIndex i => new SingletonIndex(Offset - i.Offset), |
| | 2 | 52 | | _ => new ArbitraryIndex() |
| | 17 | 53 | | }; |
| | | 54 | | /// <inheritdoc/> |
| | 139 | 55 | | public override object Clone() => new SingletonIndex(Offset); |
| | | 56 | | #region Equality checks |
| | | 57 | | /// <inheritdoc/> |
| | 371 | 58 | | public override bool Equals(object? obj) => Equals(obj as SingletonIndex); |
| | | 59 | | /// <inheritdoc/> |
| | 371 | 60 | | public bool Equals(SingletonIndex? other) => !(other is null) && Offset == other.Offset; |
| | | 61 | | /// <inheritdoc/> |
| | 0 | 62 | | public override int GetHashCode() => HashCode.Combine(Offset); |
| | | 63 | | /// <inheritdoc/> |
| | 0 | 64 | | public static bool operator ==(SingletonIndex? left, SingletonIndex? right) => EqualityComparer<SingletonIndex?> |
| | | 65 | | /// <inheritdoc/> |
| | 0 | 66 | | public static bool operator !=(SingletonIndex? left, SingletonIndex? right) => !(left == right); |
| | | 67 | | #endregion |
| | | 68 | | } |
| | | 69 | | } |