mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

overloading support for C# expressions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-04-23 22:03:27 -07:00
parent 662e43d264
commit 643a87cb5b
2 changed files with 60 additions and 163 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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
}
}

20
src/api/dotnet/BoolExpr.cs
View file

@ -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
}