From 63c4b7642cd4566a39906b2d73c47b4ebe9f7c1c Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Mon, 7 Mar 2016 18:25:13 -0600 Subject: Add support for weights on soft assumes. --- Source/Provers/SMTLib/SMTLibLineariser.cs | 2 +- Source/Provers/SMTLib/TypeDeclCollector.cs | 4 ++-- Source/VCExpr/VCExprAST.cs | 11 ++++++++++- Source/VCGeneration/Wlp.cs | 5 +++-- 4 files changed, 16 insertions(+), 6 deletions(-) (limited to 'Source') 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 { -- cgit v1.2.3