summaryrefslogtreecommitdiff
path: root/Source/VCGeneration
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCGeneration')
-rw-r--r--Source/VCGeneration/Check.cs7
-rw-r--r--Source/VCGeneration/VC.cs12
-rw-r--r--Source/VCGeneration/Wlp.cs17
3 files changed, 18 insertions, 18 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 8c1ae407..ae4d158a 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -346,7 +346,7 @@ namespace Microsoft.Boogie {
}
}
- public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, IList<VCExprVar> namedAssumeVars = null) {
+ public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) {
Contract.Requires(descriptiveName != null);
Contract.Requires(vc != null);
Contract.Requires(handler != null);
@@ -360,7 +360,6 @@ namespace Microsoft.Boogie {
thmProver.Reset(gen);
SetTimeout();
proverStart = DateTime.UtcNow;
- thmProver.NamedAssumeVars = namedAssumeVars;
thmProver.BeginCheck(descriptiveName, vc, handler);
// gen.ClearSharedFormulas(); PR: don't know yet what to do with this guy
@@ -388,8 +387,6 @@ namespace Microsoft.Boogie {
public abstract class ProverInterface {
- public IList<VCExprVar> NamedAssumeVars;
-
public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, int taskID = -1) {
Contract.Requires(prog != null);
@@ -546,7 +543,7 @@ namespace Microsoft.Boogie {
}
// (assert vc)
- public virtual void Assert(VCExpr vc, bool polarity)
+ public virtual void Assert(VCExpr vc, bool polarity, bool isSoft = false, int weight = 1)
{
throw new NotImplementedException();
}
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index ad067c04..6e43e917 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1386,8 +1386,7 @@ namespace VC {
var exprGen = ctx.ExprGen;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
- var namedAssumeVars = new List<VCExprVar>();
- VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context, namedAssumeVars: namedAssumeVars);
+ VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context);
Contract.Assert(vc != null);
if (!CommandLineOptions.Clo.UseLabels)
@@ -1415,7 +1414,7 @@ namespace VC {
string desc = cce.NonNull(impl.Name);
if (no >= 0)
desc += "_split" + no;
- checker.BeginCheck(desc, vc, reporter, namedAssumeVars);
+ checker.BeginCheck(desc, vc, reporter);
}
private void SoundnessCheck(HashSet<List<Block>/*!*/>/*!*/ cache, Block/*!*/ orig, List<Block/*!*/>/*!*/ copies) {
@@ -1568,8 +1567,7 @@ namespace VC {
}
break;
case CommandLineOptions.VCVariety.DagIterative:
- // TODO(wuestholz): Support named assume statements not just for this encoding.
- vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount, namedAssumeVars: namedAssumeVars);
+ vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount);
break;
case CommandLineOptions.VCVariety.Doomed:
vc = FlatBlockVC(impl, label2absy, false, false, true, proverContext, out assertionCount);
@@ -3393,7 +3391,7 @@ namespace VC {
Dictionary<int, Absy> label2absy,
ProverContext proverCtxt,
out int assertionCount,
- bool isPositiveContext = true, IList<VCExprVar> namedAssumeVars = null)
+ bool isPositiveContext = true)
{
Contract.Requires(blocks != null);
Contract.Requires(proverCtxt != null);
@@ -3453,7 +3451,7 @@ namespace VC {
}
VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariableExpr, isPositiveContext);
- VCExpr vc = Wlp.Block(block, SuccCorrect, context, namedAssumeVars);
+ VCExpr vc = Wlp.Block(block, SuccCorrect, context);
assertionCount += context.AssertionCount;
VCExprVar v = gen.Variable(block.Label + "_correct", Bpl.Type.Bool);
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index 508a1400..07db709d 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -48,7 +48,7 @@ namespace VC {
public class Wlp
{
- public static VCExpr Block(Block b, VCExpr N, VCContext ctxt, IList<VCExprVar> namedAssumeVars = null)
+ public static VCExpr Block(Block b, VCExpr N, VCContext ctxt)
//modifies ctxt.*;
{
Contract.Requires(b != null);
@@ -63,7 +63,7 @@ namespace VC {
for (int i = b.Cmds.Count; --i >= 0; )
{
- res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt, namedAssumeVars);
+ res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt);
}
int id = b.UniqueId;
@@ -87,7 +87,7 @@ namespace VC {
/// <summary>
/// Computes the wlp for an assert or assume command "cmd".
/// </summary>
- internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt, IList<VCExprVar> namedAssumeVars = null) {
+ internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) {
Contract.Requires(cmd != null);
Contract.Requires(N != null);
Contract.Requires(ctxt != null);
@@ -193,11 +193,16 @@ namespace VC {
var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);
var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id");
- if (CommandLineOptions.Clo.PrintNecessaryAssumes && aid != null && namedAssumeVars != null)
+ if (CommandLineOptions.Clo.PrintNecessaryAssumes && aid != null)
{
var v = gen.Variable("assume$$" + aid, Microsoft.Boogie.Type.Bool);
- namedAssumeVars.Add(v);
- expr = gen.ImpliesSimp(v, expr);
+ expr = gen.Function(VCExpressionGenerator.NamedAssumeOp, v, gen.ImpliesSimp(v, expr));
+ }
+ var soft = QKeyValue.FindBoolAttribute(ac.Attributes, "soft");
+ if (soft && aid != null)
+ {
+ var v = gen.Variable("soft$$" + aid, Microsoft.Boogie.Type.Bool);
+ expr = gen.Function(VCExpressionGenerator.SoftOp, v, gen.ImpliesSimp(v, expr));
}
return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes, gen.ImpliesSimp(expr, N));
} else {
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-19 10:15:53 +0000