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
+
+ /// Operator overloading for arithmetical operator
+ public static ArithExpr operator -(ArithExpr a, ArithExpr b)
+ {
+ return a.Context.MkSub(a, b);
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static ArithExpr operator +(ArithExpr a, ArithExpr b)
+ {
+ return a.Context.MkAdd(a, b);
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static ArithExpr operator *(ArithExpr a, ArithExpr b)
+ {
+ return a.Context.MkMul(a, b);
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static ArithExpr operator *(ArithExpr a, int b)
+ {
+ return a.Context.MkMul(a, (ArithExpr)a.Context.MkNumeral(b, a.Context.MkIntSort()));
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static ArithExpr operator *(ArithExpr a, double b)
+ {
+ return a.Context.MkMul(a, (ArithExpr)a.Context.MkNumeral(b.ToString(), a.Context.MkRealSort()));
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static ArithExpr operator *(int a, ArithExpr b)
+ {
+ return b.Context.MkMul((ArithExpr)b.Context.MkNumeral(a, b.Context.MkIntSort()), b);
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static ArithExpr operator *(double a, ArithExpr b)
+ {
+ return b.Context.MkMul((ArithExpr)b.Context.MkNumeral(a.ToString(), b.Context.MkRealSort()), b);
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static BoolExpr operator <=(ArithExpr a, ArithExpr b)
+ {
+ return a.Context.MkLe(a, b);
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static BoolExpr operator <=(ArithExpr a, int b)
+ {
+ return a <= (ArithExpr)a.Context.MkNumeral(b, a.Context.MkIntSort());
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static BoolExpr operator <=(ArithExpr a, double b)
+ {
+ return a <= (ArithExpr)a.Context.MkNumeral(b.ToString(), a.Context.MkRealSort());
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static BoolExpr operator <=(int a, ArithExpr b)
+ {
+ return (ArithExpr)b.Context.MkNumeral(a, b.Context.MkIntSort()) <= b;
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static BoolExpr operator <=(double a, ArithExpr b)
+ {
+ return (ArithExpr)b.Context.MkNumeral(a.ToString(), b.Context.MkRealSort()) <= b;
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static BoolExpr operator <(ArithExpr a, ArithExpr b)
+ {
+ return a.Context.MkLt(a, b);
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static BoolExpr operator <(ArithExpr a, int b)
+ {
+ return a < (ArithExpr)a.Context.MkNumeral(b, a.Context.MkIntSort());
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static BoolExpr operator <(ArithExpr a, double b)
+ {
+ return a < (ArithExpr)a.Context.MkNumeral(b.ToString(), a.Context.MkRealSort());
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static BoolExpr operator <(int a, ArithExpr b)
+ {
+ return (ArithExpr)b.Context.MkNumeral(a, b.Context.MkIntSort()) < b;
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static BoolExpr operator <(double a, ArithExpr b)
+ {
+ return (ArithExpr)b.Context.MkNumeral(a.ToString(), b.Context.MkRealSort()) < b;
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static BoolExpr operator >=(ArithExpr a, ArithExpr b)
+ {
+ return a.Context.MkGe(a, b);
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static BoolExpr operator >=(ArithExpr a, int b)
+ {
+ return a >= (ArithExpr)a.Context.MkNumeral(b, a.Context.MkIntSort());
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static BoolExpr operator >=(ArithExpr a, double b)
+ {
+ return a >= (ArithExpr)a.Context.MkNumeral(b.ToString(), a.Context.MkRealSort());
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static BoolExpr operator >=(int a, ArithExpr b)
+ {
+ return (ArithExpr)b.Context.MkNumeral(a, b.Context.MkIntSort()) >= b;
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static BoolExpr operator >=(double a, ArithExpr b)
+ {
+ return (ArithExpr)b.Context.MkNumeral(a.ToString(), b.Context.MkRealSort()) >= b;
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static BoolExpr operator >(ArithExpr a, ArithExpr b)
+ {
+ return a.Context.MkGt(a, b);
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static BoolExpr operator >(ArithExpr a, int b)
+ {
+ return a > (ArithExpr)a.Context.MkNumeral(b, a.Context.MkIntSort());
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static BoolExpr operator >(ArithExpr a, double b)
+ {
+ return a > (ArithExpr)a.Context.MkNumeral(b.ToString(), a.Context.MkRealSort());
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static BoolExpr operator >(int a, ArithExpr b)
+ {
+ return (ArithExpr)b.Context.MkNumeral(a, b.Context.MkIntSort()) > b;
+ }
+
+ /// Operator overloading for arithmetical operator
+ public static BoolExpr operator >(double a, ArithExpr b)
+ {
+ return (ArithExpr)b.Context.MkNumeral(a.ToString(), b.Context.MkRealSort()) > b;
+ }
}
}