summaryrefslogtreecommitdiff
path: root/Source/VCExpr/VCExprAST.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCExpr/VCExprAST.cs')
-rw-r--r--Source/VCExpr/VCExprAST.cs11
1 files changed, 10 insertions, 1 deletions
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index a58cfb7f..2c77a252 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -344,7 +344,6 @@ namespace Microsoft.Boogie {
public static readonly VCExprOp MinimizeOp = new VCExprCustomOp("minimize##dummy", 2, Type.Bool);
public static readonly VCExprOp MaximizeOp = new VCExprCustomOp("maximize##dummy", 2, Type.Bool);
public static readonly VCExprOp NamedAssumeOp = new VCExprCustomOp("named_assume##dummy", 2, Type.Bool);
- public static readonly VCExprOp SoftOp = new VCExprCustomOp("soft##dummy", 2, Type.Bool);
public VCExprOp BoogieFunctionOp(Function func) {
Contract.Requires(func != null);
@@ -1570,6 +1569,16 @@ namespace Microsoft.Boogie.VCExprAST {
}
}
+ public class VCExprSoftOp : VCExprCustomOp
+ {
+ public readonly int Weight;
+
+ public VCExprSoftOp(int weight) : base("soft##dummy", 2, Microsoft.Boogie.Type.Bool)
+ {
+ Weight = weight;
+ }
+ }
+
public class VCExprCustomOp : VCExprOp {
public readonly string/*!*/ Name;
int arity;