From 643a87cb5b309b30ff1037d2f4cb6e186a38f903 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 23 Apr 2016 22:03:27 -0700
Subject: [PATCH] overloading support for C# expressions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/dotnet/ArithExpr.cs | 203 +++++++++---------------------------
 src/api/dotnet/BoolExpr.cs  |  20 ++--
 2 files changed, 60 insertions(+), 163 deletions(-)

diff --git a/src/api/dotnet/ArithExpr.cs b/src/api/dotnet/ArithExpr.cs
index ac1e9200e..58d160900 100644
--- a/src/api/dotnet/ArithExpr.cs
+++ b/src/api/dotnet/ArithExpr.cs
@@ -41,231 +41,130 @@ namespace Microsoft.Z3
 
         #region Operators
 
-        private static ArithExpr MkNum(ArithExpr e, int i)
-        {
-            return (ArithExpr)e.Context.MkNumeral(i, e.Context.MkIntSort());
-        }
+        private static ArithExpr MkNum(ArithExpr e, int i) => (ArithExpr)e.Context.MkNumeral(i, e.Context.MkIntSort());        
 
-        private static ArithExpr MkNum(ArithExpr e, double d)
-        {
-            return (ArithExpr)e.Context.MkNumeral(d.ToString(), e.Context.MkRealSort());
-        }
+        private static ArithExpr MkNum(ArithExpr e, double d) => (ArithExpr)e.Context.MkNumeral(d.ToString(), e.Context.MkRealSort());        
 
         /// <summary> Operator overloading for arithmetical divsion operator (over reals) </summary>
-        public static ArithExpr operator /(ArithExpr a, ArithExpr b)
-        {
-            return a.Context.MkDiv(a, b);
-        }
+        public static ArithExpr operator /(ArithExpr a, ArithExpr b) => a.Context.MkDiv(a, b);
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static ArithExpr operator -(ArithExpr a, ArithExpr b)
-        {
-            return a.Context.MkSub(a, b);
-        }
+        public static ArithExpr operator /(ArithExpr a, int b) => a / MkNum(a, b);
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static ArithExpr operator -(ArithExpr a, int b)
-        {
-            return a.Context.MkSub(a, MkNum(a, b));
-        }
+        public static ArithExpr operator /(ArithExpr a, double b) => a / MkNum(a, b);
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static ArithExpr operator -(ArithExpr a, double b)
-        {
-            return a.Context.MkSub(a, MkNum(a, b));
-        }
+        public static ArithExpr operator /(int a, ArithExpr b) => MkNum(b, a) / b;
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static ArithExpr operator -(int a, ArithExpr b)
-        {
-            return b.Context.MkSub(MkNum(b, a), b);
-        }
+        public static ArithExpr operator /(double a, ArithExpr b) => MkNum(b, a) / b;
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static ArithExpr operator -(double a, ArithExpr b)
-        {
-            return b.Context.MkSub(MkNum(b, a), b);
-        }
+        public static ArithExpr operator -(ArithExpr a, ArithExpr b) => 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);
-        }
+        public static ArithExpr operator -(ArithExpr a, int b) => a - MkNum(a, b);        
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static ArithExpr operator +(ArithExpr a, int b)
-        {
-            return a.Context.MkAdd(a, MkNum(a, b));
-        }
+        public static ArithExpr operator -(ArithExpr a, double b) => a - MkNum(a, b);
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static ArithExpr operator +(ArithExpr a, double b)
-        {
-            return a.Context.MkAdd(a, MkNum(a, b));
-        }
+        public static ArithExpr operator -(int a, ArithExpr b) => MkNum(b, a) - b;
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static ArithExpr operator +(int a, ArithExpr b)
-        {
-            return b.Context.MkAdd(MkNum(b, a), b);
-        }
+        public static ArithExpr operator -(double a, ArithExpr b) => MkNum(b, a) - b;
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static ArithExpr operator +(double a, ArithExpr b)
-        {
-            return b.Context.MkAdd(MkNum(b, a), b);
-        }
+        public static ArithExpr operator +(ArithExpr a, ArithExpr b) => 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);
-        }
+        public static ArithExpr operator +(ArithExpr a, int b) => a + MkNum(a, b);
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static ArithExpr operator *(ArithExpr a, int b)
-        {
-            return a.Context.MkMul(a, MkNum(a, b));
-        }
+        public static ArithExpr operator +(ArithExpr a, double b) => a + MkNum(a, b);
+ 
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator +(int a, ArithExpr b) => MkNum(b, a) + b;
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static ArithExpr operator *(ArithExpr a, double b)
-        {
-            return a.Context.MkMul(a, MkNum(a, b));
-        }
+        public static ArithExpr operator +(double a, ArithExpr b) => MkNum(b, a) + b;
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static ArithExpr operator *(int a, ArithExpr b)
-        {
-            return b.Context.MkMul(MkNum(b, a), b);
-        }
+        public static ArithExpr operator *(ArithExpr a, ArithExpr b) => a.Context.MkMul(a, b);
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static ArithExpr operator *(double a, ArithExpr b)
-        {
-            return b.Context.MkMul(MkNum(b, a), b);
-        }
+        public static ArithExpr operator *(ArithExpr a, int b) => a * MkNum(a, b);
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static BoolExpr operator <=(ArithExpr a, ArithExpr b)
-        {
-            return a.Context.MkLe(a, b); 
-        }
+        public static ArithExpr operator *(ArithExpr a, double b) => a * MkNum(a, b);
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static BoolExpr operator <=(ArithExpr a, int b)
-        {
-            return a <= MkNum(a, b);
-        }
+        public static ArithExpr operator *(int a, ArithExpr b) => MkNum(b, a) * b;
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static BoolExpr operator <=(ArithExpr a, double b)
-        {
-            return a <= MkNum(a, b);
-        }
+        public static ArithExpr operator *(double a, ArithExpr b) => MkNum(b, a) * b;
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static BoolExpr operator <=(int a, ArithExpr b)
-        {
-            return MkNum(b, a) <= b;
-        }
+        public static BoolExpr operator <=(ArithExpr a, ArithExpr b) => a.Context.MkLe(a, b);         
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static BoolExpr operator <=(double a, ArithExpr b)
-        {
-            return MkNum(b, a) <= b;
-        }
+        public static BoolExpr operator <=(ArithExpr a, int b) => a <= MkNum(a, b);
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static BoolExpr operator <(ArithExpr a, ArithExpr b)
-        {
-            return a.Context.MkLt(a, b);
-        }
+        public static BoolExpr operator <=(ArithExpr a, double b) => a <= MkNum(a, b);
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static BoolExpr operator <(ArithExpr a, int b)
-        {
-            return a < MkNum(a, b);
-        }
+        public static BoolExpr operator <=(int a, ArithExpr b) => MkNum(b, a) <= b;
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static BoolExpr operator <(ArithExpr a, double b)
-        {
-            return a < MkNum(a, b);
-        }
+        public static BoolExpr operator <=(double a, ArithExpr b) => MkNum(b, a) <= b;
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static BoolExpr operator <(int a, ArithExpr b)
-        {
-            return MkNum(b, a) < b;
-        }
+        public static BoolExpr operator <(ArithExpr a, ArithExpr b) => a.Context.MkLt(a, b);
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static BoolExpr operator <(double a, ArithExpr b)
-        {
-            return MkNum(b, a) < b;
-        }
+        public static BoolExpr operator <(ArithExpr a, int b) => a < MkNum(a, b);
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static BoolExpr operator >=(ArithExpr a, ArithExpr b)
-        {
-            return a.Context.MkGe(a, b);
-        }
+        public static BoolExpr operator <(ArithExpr a, double b) => a < MkNum(a, b);
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static BoolExpr operator >=(ArithExpr a, int b)
-        {
-            return a >= MkNum(a, b);
-        }
+        public static BoolExpr operator <(int a, ArithExpr b) => MkNum(b, a) < b;
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static BoolExpr operator >=(ArithExpr a, double b)
-        {
-            return a >= MkNum(a, b);
-        }
+        public static BoolExpr operator <(double a, ArithExpr b) => MkNum(b, a) < b;
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static BoolExpr operator >=(int a, ArithExpr b)
-        {
-            return MkNum(b, a) >= b;
-        }
+        public static BoolExpr operator >(ArithExpr a, ArithExpr b) => a.Context.MkGt(a, b);
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static BoolExpr operator >=(double a, ArithExpr b)
-        {
-            return MkNum(b, a) >= b;
-        }
+        public static BoolExpr operator >(ArithExpr a, int b) => a > MkNum(a, b);
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static BoolExpr operator >(ArithExpr a, ArithExpr b)
-        {
-            return a.Context.MkGt(a, b);
-        }
+        public static BoolExpr operator >(ArithExpr a, double b) => a > MkNum(a, b);
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static BoolExpr operator >(ArithExpr a, int b)
-        {
-            return a > MkNum(a, b);
-        }
+        public static BoolExpr operator >(int a, ArithExpr b) => MkNum(b, a) > b;
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static BoolExpr operator >(ArithExpr a, double b)
-        {
-            return a > MkNum(a, b);
-        }
+        public static BoolExpr operator >(double a, ArithExpr b) => MkNum(b, a) > b;
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static BoolExpr operator >(int a, ArithExpr b)
-        {
-            return MkNum(b, a) > b;
-        }
+        public static BoolExpr operator >=(ArithExpr a, ArithExpr b) => a.Context.MkGe(a, b);
 
         /// <summary> Operator overloading for arithmetical operator </summary>
-        public static BoolExpr operator >(double a, ArithExpr b)
-        {
-            return MkNum(b, a) > b;
-        }
+        public static BoolExpr operator >=(ArithExpr a, int b) => a >= MkNum(a, b);
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >=(ArithExpr a, double b) => a >= MkNum(a, b);
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >=(int a, ArithExpr b) => MkNum(b, a) >= b;
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >=(double a, ArithExpr b) => MkNum(b, a) >= b;
+
         #endregion
     }
 }
diff --git a/src/api/dotnet/BoolExpr.cs b/src/api/dotnet/BoolExpr.cs
index 4d5a43074..5bac65243 100644
--- a/src/api/dotnet/BoolExpr.cs
+++ b/src/api/dotnet/BoolExpr.cs
@@ -36,21 +36,19 @@ namespace Microsoft.Z3
         #endregion
 
         #region Operators
-        /// <summary>
-        /// Disjunction of Boolean expressions
-        /// </summary>
-        public static BoolExpr operator|(BoolExpr a, BoolExpr b)
-        {
-            return a.Context.MkOr(a, b);
-        }
+        /// <summary> Disjunction of Boolean expressions </summary>
+        public static BoolExpr operator|(BoolExpr a, BoolExpr b) => a.Context.MkOr(a, b);
 
         /// <summary>
         /// Conjunction of Boolean expressions
         /// </summary>
-        public static BoolExpr operator &(BoolExpr a, BoolExpr b)
-        {
-            return a.Context.MkAnd(a, b);
-        }
+        public static BoolExpr operator &(BoolExpr a, BoolExpr b) => a.Context.MkAnd(a, b);
+       
+        /// <summary> Xor of Boolean expressions </summary>
+        public static BoolExpr operator ^(BoolExpr a, BoolExpr b) => a.Context.MkXor(a, b);
+       
+        /// <summary> Negation </summary>
+        public static BoolExpr operator !(BoolExpr a) => a.Context.MkNot(a);        
 
         #endregion
     }