summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar Valentin Wüstholz <wuestholz@gmail.com>2016-03-07 18:25:13 -0600
committerGravatar Valentin Wüstholz <wuestholz@gmail.com>2016-03-07 18:25:13 -0600
commit63c4b7642cd4566a39906b2d73c47b4ebe9f7c1c (patch)
tree4310bdb93e86a0a181be5411af116b8dfa72d6c7 /Source
parent502942a53a6db2b3a900d7570807216372d49ad0 (diff)
Add support for weights on soft assumes.
Diffstat (limited to 'Source')
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs2
-rw-r--r--Source/Provers/SMTLib/TypeDeclCollector.cs4
-rw-r--r--Source/VCExpr/VCExprAST.cs11
-rw-r--r--Source/VCGeneration/Wlp.cs5
4 files changed, 16 insertions, 6 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 6df44c2f..06554fcb 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -281,7 +281,7 @@ namespace Microsoft.Boogie.SMTLib
Linearise(node[1], options);
return true;
}
- if (node.Op.Equals(VCExpressionGenerator.SoftOp))
+ if (node.Op is VCExprSoftOp)
{
Linearise(node[1], options);
return true;
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 72540c9c..d911ce58 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -210,10 +210,10 @@ void ObjectInvariant()
if (node.Op is VCExprStoreOp) RegisterStore(node);
else if (node.Op is VCExprSelectOp) RegisterSelect(node);
- else if (node.Op.Equals(VCExpressionGenerator.SoftOp)) {
+ else if (node.Op is VCExprSoftOp) {
var exprVar = node[0] as VCExprVar;
AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name));
- AddDeclaration(string.Format("(assert-soft {0} :weight 1)", exprVar.Name));
+ AddDeclaration(string.Format("(assert-soft {0} :weight {1})", exprVar.Name, ((VCExprSoftOp)node.Op).Weight));
} else if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp)) {
var exprVar = node[0] as VCExprVar;
AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name));
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;
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index 07db709d..d18c544a 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -199,10 +199,11 @@ namespace VC {
expr = gen.Function(VCExpressionGenerator.NamedAssumeOp, v, gen.ImpliesSimp(v, expr));
}
var soft = QKeyValue.FindBoolAttribute(ac.Attributes, "soft");
- if (soft && aid != null)
+ var softWeight = QKeyValue.FindIntAttribute(ac.Attributes, "soft", 0);
+ if ((soft || 0 < softWeight) && aid != null)
{
var v = gen.Variable("soft$$" + aid, Microsoft.Boogie.Type.Bool);
- expr = gen.Function(VCExpressionGenerator.SoftOp, v, gen.ImpliesSimp(v, expr));
+ expr = gen.Function(new VCExprSoftOp(Math.Max(softWeight, 1)), v, gen.ImpliesSimp(v, expr));
}
return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes, gen.ImpliesSimp(expr, N));
} else {