| | | 1 | | using Microsoft.Z3; |
| | | 2 | | using NanoCLang.Environemnts; |
| | | 3 | | |
| | | 4 | | namespace NanoCLang.Entities { |
| | | 5 | | /// <summary> |
| | | 6 | | /// Provides a class for additive expressions. |
| | | 7 | | /// </summary> |
| | | 8 | | public class AdditionExpression : BinaryExpression { |
| | | 9 | | /// <summary> |
| | | 10 | | /// Operator used for this expression. |
| | | 11 | | /// </summary> |
| | | 12 | | public const string OPERATOR = "+"; |
| | | 13 | | /// <summary> |
| | | 14 | | /// Creates a new instance of an additive expression of <paramref name="left"/> + <paramref name="right"/>. |
| | | 15 | | /// </summary> |
| | | 16 | | /// <param name="left">Left hand operand.</param> |
| | | 17 | | /// <param name="right">Right hand operand.</param> |
| | 246 | 18 | | public AdditionExpression(PureExpression left, PureExpression right) : base(left, OPERATOR, right) { } |
| | | 19 | | /// <inheritdoc/> |
| | | 20 | | public override PureExpression Replace(Substitutor sub) |
| | 23 | 21 | | => new AdditionExpression(Left.Replace(sub), Right.Replace(sub)); |
| | | 22 | | /// <inheritdoc/> |
| | 43 | 23 | | protected override Type DoInferType(LocalEnvironment gamma) { |
| | 43 | 24 | | var left = Left.InferType(gamma); |
| | 43 | 25 | | var right = Right.InferType(gamma); |
| | 43 | 26 | | switch (left.BaseType) { |
| | | 27 | | case IntegerType t: |
| | 14 | 28 | | switch (right.BaseType) { |
| | 12 | 29 | | case IntegerType o when t.Size == o.Size: |
| | 12 | 30 | | return new RefinedType( |
| | 12 | 31 | | new IntegerType(t.Size, IndexOperation(t.Values, o.Values)), |
| | 24 | 32 | | v => EqualExpression(v, this)); |
| | | 33 | | case ReferenceType o: |
| | 2 | 34 | | return new RefinedType( |
| | 2 | 35 | | new ReferenceType(o.Location, IndexOperation(t.Values, o.Offsets)), |
| | 4 | 36 | | v => new UninterpretedApplicationExpression("PAdd", v, Right, Left)); |
| | 0 | 37 | | default: throw new IllFormedException(this, $"Cannot add {left.BaseType} and {right.BaseType}!"); |
| | | 38 | | } |
| | | 39 | | case ReferenceType t: |
| | 29 | 40 | | switch (right.BaseType) { |
| | | 41 | | case IntegerType o: |
| | 29 | 42 | | return new RefinedType( |
| | 29 | 43 | | new ReferenceType(t.Location, IndexOperation(t.Offsets, o.Values)), |
| | 58 | 44 | | v => new UninterpretedApplicationExpression("PAdd", v, Left, Right)); |
| | 0 | 45 | | default: throw new IllFormedException(this, $"Cannot add {left.BaseType} and {right.BaseType}!"); |
| | | 46 | | } |
| | 0 | 47 | | default: throw new IllFormedException(this, $"No binary operation {left.BaseType}!"); |
| | | 48 | | } |
| | 43 | 49 | | } |
| | | 50 | | /// <inheritdoc/> |
| | | 51 | | public override ArithExpr ToArithmetic(LocalEnvironment gamma, NanoCSMT smt) |
| | 33 | 52 | | => smt.Context.MkAdd(Left.ToArithmetic(gamma, smt), Right.ToArithmetic(gamma, smt)); |
| | | 53 | | /// <inheritdoc/> |
| | 43 | 54 | | public override Index IndexOperation(Index left, Index right) => left + right; |
| | | 55 | | } |
| | | 56 | | } |