mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

add overloading for arithmetical expressions in C# to handle common cases

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-04-22 13:58:02 -07:00
parent 8ee49d16df
commit e4b7ac37f3
1 changed files with 162 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

162
src/api/dotnet/ArithExpr.cs
View file

@ -38,5 +38,167 @@ namespace Microsoft.Z3
Contract.Requires(ctx != null); Contract.Requires(ctx != null);
} }
#endregion #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;
}
} }
} }