From e4b7ac37f38f1a75da362bb7a2afa87c98da54f1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 22 Apr 2016 13:58:02 -0700
Subject: [PATCH] add overloading for arithmetical expressions in C# to handle
 common cases

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/dotnet/ArithExpr.cs | 162 ++++++++++++++++++++++++++++++++++++
 1 file changed, 162 insertions(+)

diff --git a/src/api/dotnet/ArithExpr.cs b/src/api/dotnet/ArithExpr.cs
index 7858ff3e1..56aa48f26 100644
--- a/src/api/dotnet/ArithExpr.cs
+++ b/src/api/dotnet/ArithExpr.cs
@@ -38,5 +38,167 @@ namespace Microsoft.Z3
             Contract.Requires(ctx != null);
         }
         #endregion
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator -(ArithExpr a, ArithExpr b)
+        {
+            return a.Context.MkSub(a, b);
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator +(ArithExpr a, ArithExpr b)
+        {
+            return a.Context.MkAdd(a, b);
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator *(ArithExpr a, ArithExpr b)
+        {
+            return a.Context.MkMul(a, b);
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator *(ArithExpr a, int b)
+        {
+            return a.Context.MkMul(a, (ArithExpr)a.Context.MkNumeral(b, a.Context.MkIntSort()));
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator *(ArithExpr a, double b)
+        {
+            return a.Context.MkMul(a, (ArithExpr)a.Context.MkNumeral(b.ToString(), a.Context.MkRealSort()));
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator *(int a, ArithExpr b)
+        {
+            return b.Context.MkMul((ArithExpr)b.Context.MkNumeral(a, b.Context.MkIntSort()), b);
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator *(double a, ArithExpr b)
+        {
+            return b.Context.MkMul((ArithExpr)b.Context.MkNumeral(a.ToString(), b.Context.MkRealSort()), b);
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator <=(ArithExpr a, ArithExpr b)
+        {
+            return a.Context.MkLe(a, b); 
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator <=(ArithExpr a, int b)
+        {
+            return a <= (ArithExpr)a.Context.MkNumeral(b, a.Context.MkIntSort());
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator <=(ArithExpr a, double b)
+        {
+            return a <= (ArithExpr)a.Context.MkNumeral(b.ToString(), a.Context.MkRealSort());
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator <=(int a, ArithExpr b)
+        {
+            return (ArithExpr)b.Context.MkNumeral(a, b.Context.MkIntSort()) <= b;
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator <=(double a, ArithExpr b)
+        {
+            return (ArithExpr)b.Context.MkNumeral(a.ToString(), b.Context.MkRealSort()) <= b;
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator <(ArithExpr a, ArithExpr b)
+        {
+            return a.Context.MkLt(a, b);
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator <(ArithExpr a, int b)
+        {
+            return a < (ArithExpr)a.Context.MkNumeral(b, a.Context.MkIntSort());
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator <(ArithExpr a, double b)
+        {
+            return a < (ArithExpr)a.Context.MkNumeral(b.ToString(), a.Context.MkRealSort());
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator <(int a, ArithExpr b)
+        {
+            return (ArithExpr)b.Context.MkNumeral(a, b.Context.MkIntSort()) < b;
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator <(double a, ArithExpr b)
+        {
+            return (ArithExpr)b.Context.MkNumeral(a.ToString(), b.Context.MkRealSort()) < b;
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >=(ArithExpr a, ArithExpr b)
+        {
+            return a.Context.MkGe(a, b);
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >=(ArithExpr a, int b)
+        {
+            return a >= (ArithExpr)a.Context.MkNumeral(b, a.Context.MkIntSort());
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >=(ArithExpr a, double b)
+        {
+            return a >= (ArithExpr)a.Context.MkNumeral(b.ToString(), a.Context.MkRealSort());
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >=(int a, ArithExpr b)
+        {
+            return (ArithExpr)b.Context.MkNumeral(a, b.Context.MkIntSort()) >= b;
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >=(double a, ArithExpr b)
+        {
+            return (ArithExpr)b.Context.MkNumeral(a.ToString(), b.Context.MkRealSort()) >= b;
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >(ArithExpr a, ArithExpr b)
+        {
+            return a.Context.MkGt(a, b);
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >(ArithExpr a, int b)
+        {
+            return a > (ArithExpr)a.Context.MkNumeral(b, a.Context.MkIntSort());
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >(ArithExpr a, double b)
+        {
+            return a > (ArithExpr)a.Context.MkNumeral(b.ToString(), a.Context.MkRealSort());
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >(int a, ArithExpr b)
+        {
+            return (ArithExpr)b.Context.MkNumeral(a, b.Context.MkIntSort()) > b;
+        }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >(double a, ArithExpr b)
+        {
+            return (ArithExpr)b.Context.MkNumeral(a.ToString(), b.Context.MkRealSort()) > b;
+        }
     }
 }