| | | 1 | | using Microsoft.Z3; |
| | | 2 | | using System; |
| | | 3 | | using System.Collections.Generic; |
| | | 4 | | |
| | | 5 | | namespace NanoCLang.Entities { |
| | | 6 | | /// <summary> |
| | | 7 | | /// Provides a class for arbitrary indices. |
| | | 8 | | /// </summary> |
| | | 9 | | public class ArbitraryIndex : Index, IEquatable<ArbitraryIndex?> { |
| | | 10 | | /// <inheritdoc/> |
| | | 11 | | // Arbitrary indices always overlap with everything |
| | 0 | 12 | | public override bool CollidesWith(int size, Index index, int otherSize) => true; |
| | | 13 | | /// <inheritdoc/> |
| | | 14 | | public override (BoolExpr guard, IntExpr value) SMTPossibleValues(NanoCSMT smt, int size, string prefix) |
| | 0 | 15 | | => (smt.Context.MkTrue(), smt.Context.MkIntConst($"{prefix}arbindex")); |
| | | 16 | | /// <inheritdoc/> |
| | 5 | 17 | | public override IEnumerable<StringFormatterToken> Tokens(NanoCSourceFormat args) { |
| | 5 | 18 | | yield return "any"; |
| | 5 | 19 | | } |
| | | 20 | | /// <inheritdoc/> |
| | 5 | 21 | | public override bool SubIndex(Index other) => other is ArbitraryIndex; |
| | | 22 | | /// <inheritdoc/> |
| | 26 | 23 | | public override bool IncludesOffset(int offset) => true; |
| | | 24 | | /// <inheritdoc/> |
| | 0 | 25 | | protected override Index Add(Index right) => new ArbitraryIndex(); |
| | | 26 | | /// <inheritdoc/> |
| | 0 | 27 | | protected override Index Sub(Index right) => new ArbitraryIndex(); |
| | | 28 | | /// <inheritdoc/> |
| | 252 | 29 | | public override object Clone() => new ArbitraryIndex(); |
| | | 30 | | #region Equality checks |
| | | 31 | | /// <inheritdoc/> |
| | 251 | 32 | | public override bool Equals(object? obj) => Equals(obj as ArbitraryIndex); |
| | | 33 | | /// <inheritdoc/> |
| | 251 | 34 | | public bool Equals(ArbitraryIndex? other) => !(other is null); |
| | | 35 | | /// <inheritdoc/> |
| | 0 | 36 | | public override int GetHashCode() => 0; |
| | | 37 | | /// <inheritdoc/> |
| | 0 | 38 | | public static bool operator ==(ArbitraryIndex? left, ArbitraryIndex? right) => EqualityComparer<ArbitraryIndex?> |
| | | 39 | | /// <inheritdoc/> |
| | 0 | 40 | | public static bool operator !=(ArbitraryIndex? left, ArbitraryIndex? right) => !(left == right); |
| | | 41 | | #endregion |
| | | 42 | | } |
| | | 43 | | } |