diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2014-08-15 18:09:57 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-08-15 18:09:57 +0100 |
| commit | c0341ed4745b916293be00f1a6c62514b418e69c (patch) | |
| tree | b37d6f7181e1423b1c43a5c87371e2ef2c029385 /Source/Core/AbsyExpr.cs | |
| parent | 1caf1538249bb7694be25521a06afb06107a7104 (diff) | |
Added missing Expr.Neg() static method.
Diffstat (limited to 'Source/Core/AbsyExpr.cs')
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 95a11a65..f648cec1 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -209,6 +209,13 @@ namespace Microsoft.Boogie { return Unary(Token.NoToken, UnaryOperator.Opcode.Not, e1);
}
+
+ public static Expr Neg(Expr e1) {
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ return Unary(Token.NoToken, UnaryOperator.Opcode.Neg, e1);
+ }
+
public static NAryExpr Imp(Expr e1, Expr e2) {
Contract.Requires(e2 != null);
Contract.Requires(e1 != null);
|