| | | 1 | | using Microsoft.Z3; |
| | | 2 | | using NanoCLang.Environemnts; |
| | | 3 | | using System; |
| | | 4 | | using System.Collections.Generic; |
| | | 5 | | using System.Linq; |
| | | 6 | | |
| | | 7 | | namespace NanoCLang.Entities { |
| | | 8 | | /// <summary> |
| | | 9 | | /// Provides a class for uninterpreted function calls. |
| | | 10 | | /// </summary> |
| | | 11 | | public class UninterpretedApplicationExpression : PureExpression, IEquatable<UninterpretedApplicationExpression?> { |
| | | 12 | | /// <summary> |
| | | 13 | | /// Creates a new uninterpreted function call instance that calls the function named <paramref name="name"/> wit |
| | | 14 | | /// </summary> |
| | | 15 | | /// <param name="name">Name of the uninterpreted function to call.</param> |
| | | 16 | | /// <param name="parameters">Parameters to pass to the function.</param> |
| | 1154 | 17 | | public UninterpretedApplicationExpression(string name, params PureExpression[] parameters) { |
| | 577 | 18 | | Name = name; |
| | 577 | 19 | | Parameters = parameters; |
| | 577 | 20 | | } |
| | | 21 | | /// <summary> |
| | | 22 | | /// Name of the uninterpreted function to call. |
| | | 23 | | /// </summary> |
| | 1495 | 24 | | public string Name { get; } |
| | | 25 | | /// <summary> |
| | | 26 | | /// Parameters to pass to the function. |
| | | 27 | | /// </summary> |
| | 2103 | 28 | | public PureExpression[] Parameters { get; } |
| | | 29 | | /// <inheritdoc/> |
| | 83 | 30 | | public override void WellFormed(LocalEnvironment gamma) { |
| | 83 | 31 | | VerbConsole.WriteLine(VerbosityLevel.Default, $"WF-UnintF: {this}"); |
| | 499 | 32 | | foreach (var param in Parameters) |
| | 125 | 33 | | param.WellFormed(gamma); |
| | 83 | 34 | | } |
| | | 35 | | /// <inheritdoc/> |
| | 0 | 36 | | protected override Type DoInferType(LocalEnvironment gamma) => throw new InvalidOperationException("Cannot infer |
| | | 37 | | /// <inheritdoc/> |
| | 500 | 38 | | public override IEnumerable<StringFormatterToken> Tokens(NanoCSourceFormat args) { |
| | 500 | 39 | | yield return Name; |
| | 500 | 40 | | yield return "("; |
| | 5643 | 41 | | foreach (var tk in StringFormatterToken.Separated(Parameters, args, args.ParameterListSeparator)) yield retu |
| | 500 | 42 | | if (args.SpaceInEmptyArgList && Parameters.Length == 0) yield return " "; |
| | 500 | 43 | | yield return ")"; |
| | 500 | 44 | | } |
| | | 45 | | /// <inheritdoc/> |
| | 382 | 46 | | public override BoolExpr ToBoolean(LocalEnvironment gamma, NanoCSMT smt) { |
| | 382 | 47 | | switch (Name) { |
| | | 48 | | case "PAdd": |
| | 32 | 49 | | if (Parameters.Length != 3) throw new IllFormedException(this, $"Inconsistend parameter count for uninte |
| | 32 | 50 | | return smt.PAdd((IntExpr)Parameters[0].ToArithmetic(gamma, smt), (IntExpr)Parameters[1].ToArithmetic(gam |
| | | 51 | | case "BLen": |
| | 153 | 52 | | if (Parameters.Length != 2) throw new IllFormedException(this, $"Inconsistend parameter count for uninte |
| | 153 | 53 | | return smt.BLen((IntExpr)Parameters[0].ToArithmetic(gamma, smt), Parameters[1].ToArithmetic(gamma, smt)) |
| | | 54 | | case "Safe": |
| | 159 | 55 | | if (Parameters.Length != 1) throw new IllFormedException(this, $"Inconsistend parameter count for uninte |
| | 159 | 56 | | return smt.Safe((IntExpr)Parameters[0].ToArithmetic(gamma, smt)); |
| | | 57 | | case "SafeN": |
| | 38 | 58 | | if (Parameters.Length != 2) throw new IllFormedException(this, $"Inconsistend parameter count for uninte |
| | 38 | 59 | | return smt.SafeN((IntExpr)Parameters[0].ToArithmetic(gamma, smt), (IntExpr)Parameters[1].ToArithmetic(ga |
| | 0 | 60 | | default: throw new IllFormedException(this, $"Function {Name} is not a boolean function!"); |
| | | 61 | | } |
| | 382 | 62 | | } |
| | | 63 | | /// <inheritdoc/> |
| | 0 | 64 | | public override ArithExpr ToArithmetic(LocalEnvironment gamma, NanoCSMT smt) { |
| | 0 | 65 | | switch (Name) { |
| | | 66 | | case "BS": |
| | 0 | 67 | | if (Parameters.Length != 1) throw new IllFormedException(this, $"Inconsistend parameter count for uninte |
| | 0 | 68 | | return smt.BS((IntExpr)Parameters[0].ToArithmetic(gamma, smt)); |
| | | 69 | | case "BE": |
| | 0 | 70 | | if (Parameters.Length != 1) throw new IllFormedException(this, $"Inconsistend parameter count for uninte |
| | 0 | 71 | | return smt.BS((IntExpr)Parameters[0].ToArithmetic(gamma, smt)); |
| | 0 | 72 | | default: throw new IllFormedException(this, $"Function {Name} is not an integral function!"); |
| | | 73 | | } |
| | 0 | 74 | | } |
| | | 75 | | /// <inheritdoc/> |
| | | 76 | | public override PureExpression Replace(Substitutor sub) |
| | 908 | 77 | | => new UninterpretedApplicationExpression(Name, Parameters.Select(i => i.Replace(sub)).ToArray()); |
| | | 78 | | #region Equality checks |
| | | 79 | | /// <inheritdoc/> |
| | 125 | 80 | | public override bool Equals(object? obj) => Equals(obj as UninterpretedApplicationExpression); |
| | | 81 | | /// <inheritdoc/> |
| | 125 | 82 | | public bool Equals(UninterpretedApplicationExpression? other) => !(other is null) && Name == other.Name && Param |
| | | 83 | | /// <inheritdoc/> |
| | 0 | 84 | | public override int GetHashCode() { |
| | 0 | 85 | | var hash = new HashCode(); |
| | 0 | 86 | | hash.Add(Name); |
| | 0 | 87 | | foreach (var param in Parameters) hash.Add(param); |
| | 0 | 88 | | return hash.ToHashCode(); |
| | 0 | 89 | | } |
| | | 90 | | /// <inheritdoc/> |
| | 0 | 91 | | public static bool operator ==(UninterpretedApplicationExpression? left, UninterpretedApplicationExpression? rig |
| | | 92 | | /// <inheritdoc/> |
| | 0 | 93 | | public static bool operator !=(UninterpretedApplicationExpression? left, UninterpretedApplicationExpression? rig |
| | | 94 | | #endregion |
| | | 95 | | } |
| | | 96 | | } |