Z3
ArithExpr.cs
Go to the documentation of this file.
1/*++
2Copyright (<c>) 2012 Microsoft Corporation
3
4Module Name:
5
6 ArithExpr.cs
7
8Abstract:
9
10 Z3 Managed API: Arith Expressions
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-11-23
15
16Notes:
17
18--*/
19using System.Diagnostics;
20using System;
21using System.Collections.Generic;
22using System.Linq;
23using System.Text;
24
25
26namespace Microsoft.Z3
27{
31 public class ArithExpr : Expr
32 {
33 #region Internal
35 internal ArithExpr(Context ctx, IntPtr obj)
36 : base(ctx, obj)
37 {
38 Debug.Assert(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}
Arithmetic expressions (int/real)
Definition: ArithExpr.cs:32
static BoolExpr operator>(ArithExpr a, ArithExpr b)
Operator overloading for arithmetical operator
Definition: ArithExpr.cs:142
static ArithExpr operator*(ArithExpr a, ArithExpr b)
Operator overloading for arithmetical operator
Definition: ArithExpr.cs:97
static BoolExpr operator>=(ArithExpr a, ArithExpr b)
Operator overloading for arithmetical operator
Definition: ArithExpr.cs:157
static ArithExpr operator+(ArithExpr a, ArithExpr b)
Operator overloading for arithmetical operator
Definition: ArithExpr.cs:82
static BoolExpr operator<(ArithExpr a, ArithExpr b)
Operator overloading for arithmetical operator
Definition: ArithExpr.cs:127
static ArithExpr operator-(ArithExpr a)
Operator overloading for arithmetical operator
Definition: ArithExpr.cs:64
static ArithExpr operator/(ArithExpr a, ArithExpr b)
Operator overloading for arithmetical division operator (over reals)
Definition: ArithExpr.cs:49
static BoolExpr operator<=(ArithExpr a, ArithExpr b)
Operator overloading for arithmetical operator
Definition: ArithExpr.cs:112
Boolean expressions
Definition: BoolExpr.cs:32
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 <= t2
Definition: Context.cs:1145
ArithExpr MkUnaryMinus(ArithExpr t)
Create an expression representing -t.
Definition: Context.cs:1067
ArithExpr MkSub(params ArithExpr[] t)
Create an expression representing t[0] - t[1] - ....
Definition: Context.cs:1055
BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 < t2
Definition: Context.cs:1132
BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 >= t2
Definition: Context.cs:1171
ArithExpr MkMul(params ArithExpr[] t)
Create an expression representing t[0] * t[1] * ....
Definition: Context.cs:1031
ArithExpr MkAdd(params ArithExpr[] t)
Create an expression representing t[0] + t[1] + ....
Definition: Context.cs:1007
RealSort MkRealSort()
Create a real sort.
Definition: Context.cs:211
ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 / t2.
Definition: Context.cs:1078
IntSort MkIntSort()
Create a new integer sort.
Definition: Context.cs:202
Expr MkNumeral(string v, Sort ty)
Create a Term of a given sort.
Definition: Context.cs:2745
BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
Create an expression representing t1 > t2
Definition: Context.cs:1158
Expressions are terms.
Definition: Expr.cs:31