| | | 1 | | using Microsoft.Z3; |
| | | 2 | | using NanoCLang.Environemnts; |
| | | 3 | | using System; |
| | | 4 | | using System.Collections.Generic; |
| | | 5 | | |
| | | 6 | | namespace NanoCLang.Entities { |
| | | 7 | | /// <summary> |
| | | 8 | | /// Provides a class for variable literal expression. |
| | | 9 | | /// </summary> |
| | | 10 | | public class VariableExpression : PureExpression, IEquatable<VariableExpression?>, ICloneable { |
| | | 11 | | /// <summary> |
| | | 12 | | /// Creates a new instance of a variable literal with the given <paramref name="name"/>. |
| | | 13 | | /// </summary> |
| | | 14 | | /// <param name="name">Name that the literal refers to.</param> |
| | 5014 | 15 | | public VariableExpression(string name) { |
| | 2507 | 16 | | Name = name; |
| | 2507 | 17 | | } |
| | | 18 | | /// <summary> |
| | | 19 | | /// Name that the literal refers to. |
| | | 20 | | /// </summary> |
| | 6394 | 21 | | public string Name { get; } |
| | | 22 | | /// <summary> |
| | | 23 | | /// Converts a string to its literal variable expression. |
| | | 24 | | /// </summary> |
| | | 25 | | /// <param name="name">Name of the variable.</param> |
| | 0 | 26 | | public static implicit operator VariableExpression(string name) => new VariableExpression(name); |
| | | 27 | | /// <inheritdoc/> |
| | 256 | 28 | | public override void WellFormed(LocalEnvironment gamma) { |
| | 256 | 29 | | VerbConsole.WriteLine(VerbosityLevel.Default, $"WF-Var: {Name}"); |
| | 256 | 30 | | if (!gamma.ContainsKey(Name)) |
| | 0 | 31 | | throw new IllFormedException(this, $"Reference to undeclared variable {Name}!"); |
| | 256 | 32 | | } |
| | | 33 | | /// <inheritdoc/> |
| | | 34 | | public override PureExpression Replace(Substitutor rep) |
| | 1003 | 35 | | => rep.Variables.TryGetValue(Name, out var substitute) ? substitute : (PureExpression)Clone(); |
| | | 36 | | /// <inheritdoc/> |
| | 461 | 37 | | public virtual object Clone() => new VariableExpression(Name); |
| | | 38 | | /// <inheritdoc/> |
| | 1399 | 39 | | public override ArithExpr ToArithmetic(LocalEnvironment gamma, NanoCSMT smt) => smt.Context.MkIntConst(Name); |
| | | 40 | | /// <inheritdoc/> |
| | 14 | 41 | | public override BoolExpr ToBoolean(LocalEnvironment gamma, NanoCSMT smt) => smt.Context.MkBoolConst(Name); |
| | | 42 | | /// <inheritdoc/> |
| | 624 | 43 | | protected override Type DoInferType(LocalEnvironment gamma) { |
| | 624 | 44 | | return !gamma.TryGetValue(Name, out var type) |
| | 624 | 45 | | ? throw new IllFormedException(this, $"Variable {Name} is not bound in the local environment!") |
| | 1248 | 46 | | : new RefinedType(type, v => EqualExpression(v, this)); |
| | 624 | 47 | | } |
| | | 48 | | /// <inheritdoc/> |
| | 1715 | 49 | | public override IEnumerable<StringFormatterToken> Tokens(NanoCSourceFormat args) { |
| | 1715 | 50 | | yield return Name; |
| | 1715 | 51 | | } |
| | | 52 | | #region Equality checks |
| | | 53 | | /// <inheritdoc/> |
| | 335 | 54 | | public override bool Equals(object? obj) => Equals(obj as VariableExpression); |
| | | 55 | | /// <inheritdoc/> |
| | 335 | 56 | | public bool Equals(VariableExpression? other) => !(other is null) && Name == other.Name; |
| | | 57 | | /// <inheritdoc/> |
| | 8 | 58 | | public override int GetHashCode() => System.HashCode.Combine(Name); |
| | | 59 | | /// <inheritdoc/> |
| | 0 | 60 | | public static bool operator ==(VariableExpression? left, VariableExpression? right) => EqualityComparer<Variable |
| | | 61 | | /// <inheritdoc/> |
| | 0 | 62 | | public static bool operator !=(VariableExpression? left, VariableExpression? right) => !(left == right); |
| | | 63 | | #endregion |
| | | 64 | | } |
| | | 65 | | } |