| | | 1 | | using Microsoft.Z3; |
| | | 2 | | using NanoCLang.Environemnts; |
| | | 3 | | using System; |
| | | 4 | | |
| | | 5 | | namespace NanoCLang.Entities { |
| | | 6 | | /// <summary> |
| | | 7 | | /// Provides a class for relation expressions. |
| | | 8 | | /// </summary> |
| | | 9 | | public class RelationalExpression : BinaryExpression { |
| | | 10 | | private readonly RelOperator @operator; |
| | | 11 | | /// <summary> |
| | | 12 | | /// Creates a new instance of a relation expression of <paramref name="left"/> and <paramref name="right"/>. |
| | | 13 | | /// </summary> |
| | | 14 | | /// <param name="left">Left hand operand.</param> |
| | | 15 | | /// <param name="op">Operator to apply</param> |
| | | 16 | | /// <param name="right">Right hand operand.</param> |
| | 2724 | 17 | | public RelationalExpression(PureExpression left, RelOperator op, PureExpression right) : base(left, GetOperator( |
| | 1362 | 18 | | @operator = op; |
| | 1362 | 19 | | } |
| | | 20 | | |
| | | 21 | | /// <summary> |
| | | 22 | | /// Creates a new instance of a relation expression of <paramref name="left"/> and <paramref name="right"/>. |
| | | 23 | | /// </summary> |
| | | 24 | | /// <param name="left">Left hand operand.</param> |
| | | 25 | | /// <param name="op">Operator to apply</param> |
| | | 26 | | /// <param name="right">Right hand operand.</param> |
| | 242 | 27 | | public RelationalExpression(PureExpression left, string op, PureExpression right) : base(left, op, right) { |
| | 121 | 28 | | @operator = op switch { |
| | 28 | 29 | | "<" => RelOperator.Less, |
| | 38 | 30 | | ">" => RelOperator.Greater, |
| | 2 | 31 | | "<=" => RelOperator.LessEqual, |
| | 18 | 32 | | ">=" => RelOperator.GreaterEqual, |
| | 34 | 33 | | "==" => RelOperator.Equal, |
| | 1 | 34 | | "!=" => RelOperator.Unequal, |
| | 0 | 35 | | _ => throw new ArgumentOutOfRangeException("Invalid relational operator!") |
| | 121 | 36 | | }; |
| | 121 | 37 | | } |
| | | 38 | | |
| | | 39 | | /// <summary> |
| | | 40 | | /// Enumeration of valid relational operators. |
| | | 41 | | /// </summary> |
| | | 42 | | public enum RelOperator { |
| | | 43 | | /// <summary> |
| | | 44 | | /// Strictly less than operator. |
| | | 45 | | /// </summary> |
| | | 46 | | Less, |
| | | 47 | | /// <summary> |
| | | 48 | | /// Strictly greater than operator. |
| | | 49 | | /// </summary> |
| | | 50 | | Greater, |
| | | 51 | | /// <summary> |
| | | 52 | | /// Less or equal to operator. |
| | | 53 | | /// </summary> |
| | | 54 | | LessEqual, |
| | | 55 | | /// <summary> |
| | | 56 | | /// Greater or equal to operator. |
| | | 57 | | /// </summary> |
| | | 58 | | GreaterEqual, |
| | | 59 | | /// <summary> |
| | | 60 | | /// Equality operator. |
| | | 61 | | /// </summary> |
| | | 62 | | Equal, |
| | | 63 | | /// <summary> |
| | | 64 | | /// Inequality operator |
| | | 65 | | /// </summary> |
| | | 66 | | Unequal |
| | | 67 | | } |
| | 1362 | 68 | | private static string GetOperator(RelOperator op) => op switch { |
| | 53 | 69 | | RelOperator.Less => "<", |
| | 89 | 70 | | RelOperator.Greater => ">", |
| | 2 | 71 | | RelOperator.LessEqual => "<=", |
| | 53 | 72 | | RelOperator.GreaterEqual => ">=", |
| | 1144 | 73 | | RelOperator.Equal => "==", |
| | 21 | 74 | | RelOperator.Unequal => "!=", |
| | 0 | 75 | | _ => throw new ArgumentOutOfRangeException("Invalid relational operator!") |
| | 1362 | 76 | | }; |
| | | 77 | | /// <inheritdoc/> |
| | | 78 | | public override PureExpression Replace(Substitutor sub) |
| | 342 | 79 | | => new RelationalExpression(Left.Replace(sub), @operator, Right.Replace(sub)); |
| | | 80 | | /// <inheritdoc/> |
| | 142 | 81 | | protected override Type DoInferType(LocalEnvironment gamma) { |
| | 142 | 82 | | var left = Left.InferType(gamma); |
| | 142 | 83 | | var right = Right.InferType(gamma); |
| | | 84 | | |
| | 142 | 85 | | switch (left.BaseType) { |
| | 284 | 86 | | case IntegerType t when right.BaseType is IntegerType o && t.Size == o.Size: break; |
| | 0 | 87 | | case IntegerType _ when right.BaseType is ReferenceType: break; |
| | 0 | 88 | | case ReferenceType _ when right.BaseType is IntegerType: break; |
| | 0 | 89 | | case ReferenceType t when right.BaseType is ReferenceType o && t.Location == o.Location: break; |
| | 0 | 90 | | default: throw new IllFormedException(this, $"Cannot compare {left.BaseType} and {right.BaseType}!"); |
| | | 91 | | } |
| | 142 | 92 | | return new RefinedType(IntegerType.Boolean, |
| | 284 | 93 | | v => EqualExpression(v, this)); |
| | 142 | 94 | | } |
| | | 95 | | /// <inheritdoc/> |
| | 720 | 96 | | public override BoolExpr ToBoolean(LocalEnvironment gamma, NanoCSMT smt) => @operator switch { |
| | 168 | 97 | | RelOperator.Less => smt.Context.MkLt(Left.ToArithmetic(gamma, smt), Right.ToArithmetic(gamma, smt)), |
| | 105 | 98 | | RelOperator.Greater => smt.Context.MkGt(Left.ToArithmetic(gamma, smt), Right.ToArithmetic(gamma, smt)), |
| | 3 | 99 | | RelOperator.LessEqual => smt.Context.MkLe(Left.ToArithmetic(gamma, smt), Right.ToArithmetic(gamma, smt)), |
| | 71 | 100 | | RelOperator.GreaterEqual => smt.Context.MkGe(Left.ToArithmetic(gamma, smt), Right.ToArithmetic(gamma, smt)), |
| | 273 | 101 | | RelOperator.Equal => Equality(gamma, smt), |
| | 100 | 102 | | RelOperator.Unequal => !Equality(gamma, smt), |
| | 0 | 103 | | _ => throw new InvalidProgramException("Unexpected operator! Constructor forbids this!") |
| | 720 | 104 | | }; |
| | 373 | 105 | | private BoolExpr Equality(LocalEnvironment gamma, NanoCSMT smt) { |
| | 373 | 106 | | return Left.InferType(gamma).BaseType is IntegerType i && i.Size == 1 |
| | 373 | 107 | | ? smt.Context.MkEq(Left.ToBoolean(gamma, smt), Right.ToBoolean(gamma, smt)) |
| | 373 | 108 | | : smt.Context.MkEq(Left.ToArithmetic(gamma, smt), Right.ToArithmetic(gamma, smt)); |
| | 373 | 109 | | } |
| | | 110 | | } |
| | | 111 | | } |