Z3
ArithExpr.cs
Go to the documentation of this file.
1 /*++
2 Copyright (<c>) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  ArithExpr.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Arith Expressions
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-11-23
15 
16 Notes:
17 
18 --*/
19 using System;
20 using System.Collections.Generic;
21 using System.Linq;
22 using System.Text;
23 
25 
26 namespace Microsoft.Z3
27 {
31  public class ArithExpr : Expr
32  {
33  #region Internal
34  internal ArithExpr(Context ctx, IntPtr obj)
36  : base(ctx, obj)
37  {
38  Contract.Requires(ctx != null);
39  }
40  #endregion
41 
42  #region Operators
43 
44  private static ArithExpr MkNum(ArithExpr e, int i) { return (ArithExpr)e.Context.MkNumeral(i, e.Context.MkIntSort()); }
45 
46  private static ArithExpr MkNum(ArithExpr e, double d) { return (ArithExpr)e.Context.MkNumeral(d.ToString(), e.Context.MkRealSort()); }
47 
49  public static ArithExpr operator /(ArithExpr a, ArithExpr b) { return a.Context.MkDiv(a, b); }
50 
52  public static ArithExpr operator /(ArithExpr a, int b) { return a / MkNum(a, b); }
53 
55  public static ArithExpr operator /(ArithExpr a, double b) { return a / MkNum(a, b); }
56 
58  public static ArithExpr operator /(int a, ArithExpr b) { return MkNum(b, a) / b; }
59 
61  public static ArithExpr operator /(double a, ArithExpr b) { return MkNum(b, a) / b; }
62 
64  public static ArithExpr operator -(ArithExpr a) { return a.Context.MkUnaryMinus(a); }
65 
67  public static ArithExpr operator -(ArithExpr a, ArithExpr b) { return a.Context.MkSub(a, b); }
68 
70  public static ArithExpr operator -(ArithExpr a, int b) { return a - MkNum(a, b); }
71 
73  public static ArithExpr operator -(ArithExpr a, double b) { return a - MkNum(a, b); }
74 
76  public static ArithExpr operator -(int a, ArithExpr b) { return MkNum(b, a) - b; }
77 
79  public static ArithExpr operator -(double a, ArithExpr b) { return MkNum(b, a) - b; }
80 
82  public static ArithExpr operator +(ArithExpr a, ArithExpr b) { return a.Context.MkAdd(a, b); }
83 
85  public static ArithExpr operator +(ArithExpr a, int b) { return a + MkNum(a, b); }
86 
88  public static ArithExpr operator +(ArithExpr a, double b) { return a + MkNum(a, b); }
89 
91  public static ArithExpr operator +(int a, ArithExpr b) { return MkNum(b, a) + b; }
92 
94  public static ArithExpr operator +(double a, ArithExpr b) { return MkNum(b, a) + b; }
95 
97  public static ArithExpr operator *(ArithExpr a, ArithExpr b) { return a.Context.MkMul(a, b); }
98 
100  public static ArithExpr operator *(ArithExpr a, int b) { return a * MkNum(a, b); }
101 
103  public static ArithExpr operator *(ArithExpr a, double b) { return a * MkNum(a, b); }
104 
106  public static ArithExpr operator *(int a, ArithExpr b) { return MkNum(b, a) * b; }
107 
109  public static ArithExpr operator *(double a, ArithExpr b) { return MkNum(b, a) * b; }
110 
112  public static BoolExpr operator <=(ArithExpr a, ArithExpr b) { return a.Context.MkLe(a, b); }
113 
115  public static BoolExpr operator <=(ArithExpr a, int b) { return a <= MkNum(a, b); }
116 
118  public static BoolExpr operator <=(ArithExpr a, double b) { return a <= MkNum(a, b); }
119 
121  public static BoolExpr operator <=(int a, ArithExpr b) { return MkNum(b, a) <= b; }
122 
124  public static BoolExpr operator <=(double a, ArithExpr b) { return MkNum(b, a) <= b; }
125 
127  public static BoolExpr operator <(ArithExpr a, ArithExpr b) { return a.Context.MkLt(a, b); }
128 
130  public static BoolExpr operator <(ArithExpr a, int b) { return a < MkNum(a, b); }
131 
133  public static BoolExpr operator <(ArithExpr a, double b) { return a < MkNum(a, b); }
134 
136  public static BoolExpr operator <(int a, ArithExpr b) { return MkNum(b, a) < b; }
137 
139  public static BoolExpr operator <(double a, ArithExpr b) { return MkNum(b, a) < b; }
140 
142  public static BoolExpr operator >(ArithExpr a, ArithExpr b) { return a.Context.MkGt(a, b); }
143 
145  public static BoolExpr operator >(ArithExpr a, int b) { return a > MkNum(a, b); }
146 
148  public static BoolExpr operator >(ArithExpr a, double b) { return a > MkNum(a, b); }
149 
151  public static BoolExpr operator >(int a, ArithExpr b) { return MkNum(b, a) > b; }
152 
154  public static BoolExpr operator >(double a, ArithExpr b) { return MkNum(b, a) > b; }
155 
157  public static BoolExpr operator >=(ArithExpr a, ArithExpr b) { return a.Context.MkGe(a, b); }
158 
160  public static BoolExpr operator >=(ArithExpr a, int b) { return a >= MkNum(a, b); }
161 
163  public static BoolExpr operator >=(ArithExpr a, double b) { return a >= MkNum(a, b); }
164 
166  public static BoolExpr operator >=(int a, ArithExpr b) { return MkNum(b, a) >= b; }
167 
169  public static BoolExpr operator >=(double a, ArithExpr b) { return MkNum(b, a) >= b; }
170 
171  #endregion
172  }
173 }
ArithExpr MkAdd(params ArithExpr[] t)
Create an expression representing t[0] + t[1] + ....
Definition: Context.cs:1022
Boolean expressions
Definition: BoolExpr.cs:31
ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 / t2.
Definition: Context.cs:1099
BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 < t2
Definition: Context.cs:1157
expr operator*(expr const &a, expr const &b)
Definition: z3++.h:1061
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition: Context.cs:2669
BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 <= t2
Definition: Context.cs:1171
expr operator>=(expr const &a, expr const &b)
Definition: z3++.h:1082
expr operator<=(expr const &a, expr const &b)
Definition: z3++.h:1154
Expressions are terms.
Definition: Expr.cs:29
RealSort MkRealSort()
Create a real sort.
Definition: Context.cs:226
ArithExpr MkSub(params ArithExpr[] t)
Create an expression representing t[0] - t[1] - ....
Definition: Context.cs:1074
expr operator+(expr const &a, expr const &b)
Definition: z3++.h:1034
expr operator<(expr const &a, expr const &b)
Definition: z3++.h:1176
ArithExpr MkMul(params ArithExpr[] t)
Create an expression representing t[0] * t[1] * ....
Definition: Context.cs:1048
expr operator>(expr const &a, expr const &b)
Definition: z3++.h:1195
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
ArithExpr MkUnaryMinus(ArithExpr t)
Create an expression representing -t.
Definition: Context.cs:1087
Arithmetic expressions (int/real)
Definition: ArithExpr.cs:31
expr operator-(expr const &a)
Definition: z3++.h:1118
BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 >= t2
Definition: Context.cs:1199
expr operator/(expr const &a, expr const &b)
Definition: z3++.h:1099
BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 > t2
Definition: Context.cs:1185
IntSort MkIntSort()
Create a new integer sort.
Definition: Context.cs:216