| | | 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 BooleanExpression : BinaryExpression { |
| | | 10 | | private readonly BoolOperator @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> |
| | 1416 | 17 | | public BooleanExpression(PureExpression left, BoolOperator op, PureExpression right) : base(left, GetOperator(op |
| | 708 | 18 | | @operator = op; |
| | 708 | 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> |
| | 132 | 27 | | public BooleanExpression(PureExpression left, string op, PureExpression right) : base(left, op, right) { |
| | 66 | 28 | | @operator = op switch { |
| | 62 | 29 | | "&&" => BoolOperator.And, |
| | 4 | 30 | | "||" => BoolOperator.Or, |
| | 0 | 31 | | _ => throw new ArgumentOutOfRangeException("Invalid boolean operator!") |
| | 66 | 32 | | }; |
| | 66 | 33 | | } |
| | | 34 | | |
| | | 35 | | /// <summary> |
| | | 36 | | /// Enumeration of valid boolean operators. |
| | | 37 | | /// </summary> |
| | | 38 | | public enum BoolOperator { |
| | | 39 | | /// <summary> |
| | | 40 | | /// Logical and conjunction operator. |
| | | 41 | | /// </summary> |
| | | 42 | | And, |
| | | 43 | | /// <summary> |
| | | 44 | | /// Logical or disjunction operator. |
| | | 45 | | /// </summary> |
| | | 46 | | Or |
| | | 47 | | } |
| | 708 | 48 | | private static string GetOperator(BoolOperator op) => op switch { |
| | 702 | 49 | | BoolOperator.And => "&&", |
| | 6 | 50 | | BoolOperator.Or => "||", |
| | 0 | 51 | | _ => throw new ArgumentOutOfRangeException("Invalid boolean operator!") |
| | 708 | 52 | | }; |
| | | 53 | | /// <inheritdoc/> |
| | | 54 | | public override PureExpression Replace(Substitutor sub) |
| | 228 | 55 | | => new BooleanExpression(Left.Replace(sub), @operator, Right.Replace(sub)); |
| | | 56 | | /// <inheritdoc/> |
| | 3 | 57 | | protected override Type DoInferType(LocalEnvironment gamma) { |
| | 3 | 58 | | var left = Left.InferType(gamma); |
| | 3 | 59 | | var right = Right.InferType(gamma); |
| | 3 | 60 | | return left.BaseType != right.BaseType |
| | 3 | 61 | | ? throw new IllFormedException(this, $"Cannot compare {left.BaseType} and {right.BaseType}!") |
| | 3 | 62 | | : new RefinedType(IntegerType.Boolean, |
| | 6 | 63 | | v => EqualExpression(v, this)); |
| | 3 | 64 | | } |
| | | 65 | | /// <inheritdoc/> |
| | 284 | 66 | | public override BoolExpr ToBoolean(LocalEnvironment gamma, NanoCSMT smt) => @operator switch { |
| | 269 | 67 | | BoolOperator.And => smt.Context.MkAnd(Left.ToBoolean(gamma, smt), Right.ToBoolean(gamma, smt)), |
| | 15 | 68 | | BoolOperator.Or => smt.Context.MkOr(Left.ToBoolean(gamma, smt), Right.ToBoolean(gamma, smt)), |
| | 0 | 69 | | _ => throw new InvalidProgramException("Unexpected operator! Constructor forbids this!") |
| | 284 | 70 | | }; |
| | | 71 | | } |
| | | 72 | | } |