diff options
| author |  wuestholz <unknown> | 2015-01-16 12:21:49 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2015-01-16 12:21:49 +0100 |
| commit | a3325de0835308c293e999b574a804366f37d936 (patch) | |
| tree | b334ed029df4f81f6c9dc773d77753d084642abe /Source/VCGeneration/Wlp.cs | |
| parent | ae2b9e637a608626b66bae0824a2bcf616bdb4ed (diff) | |
Worked on the verification result caching (use native support for partially verified assertions).
Diffstat (limited to 'Source/VCGeneration/Wlp.cs')
| -rw-r--r-- | Source/VCGeneration/Wlp.cs | 51 |
1 files changed, 16 insertions, 35 deletions
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 6f6326d1..cd735501 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -106,17 +106,12 @@ namespace VC { AssertCmd ac = (AssertCmd)cmd;
ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext;
VCExpr C = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);
- ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext;
-
- VCExprLetBinding LB = null;
VCExpr VU = null;
if (ac.VerifiedUnder != null)
{
- var V = gen.Variable(ctxt.FreshLetBindingName(), Microsoft.Boogie.Type.Bool);
- LB = gen.LetBinding(V, C);
- C = V;
VU = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.VerifiedUnder);
}
+ ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext;
VCExpr R = null;
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
@@ -127,28 +122,24 @@ namespace VC { ctxt.Label2absy[id] = ac;
}
- switch (Subsumption(ac)) {
- case CommandLineOptions.SubsumptionOption.Never:
- break;
- case CommandLineOptions.SubsumptionOption.Always:
- N = gen.Implies(C, N);
- break;
- case CommandLineOptions.SubsumptionOption.NotForQuantifiers:
- if (!(C is VCExprQuantifier)) {
- N = gen.Implies(C, N);
- }
- break;
- default:
- Contract.Assert(false); throw new cce.UnreachableException(); // unexpected case
+ var subsumption = Subsumption(ac);
+ if (subsumption == CommandLineOptions.SubsumptionOption.Always
+ || (subsumption == CommandLineOptions.SubsumptionOption.NotForQuantifiers && !(C is VCExprQuantifier)))
+ {
+ N = gen.ImpliesSimp(C, N);
}
- ctxt.AssertionCount++;
+ if (VU != null)
+ {
+ var litExpr = ac.VerifiedUnder as LiteralExpr;
+ if (litExpr != null && litExpr.IsTrue)
+ {
+ return N;
+ }
+ C = gen.OrSimp(VU, C);
+ }
- // TODO(wuestholz): Try to weaken the assertion instead of assuming the property that has already been verified:
- // if (VU != null)
- // {
- // C = gen.OrSimp(VU, C);
- // }
+ ctxt.AssertionCount++;
if (ctxt.ControlFlowVariableExpr == null) {
Contract.Assert(ctxt.Label2absy != null);
@@ -164,16 +155,6 @@ namespace VC { }
}
}
-
- if (VU != null)
- {
- R = gen.ImpliesSimp(gen.ImpliesSimp(VU, C), R);
- }
-
- if (LB != null)
- {
- R = gen.Let(R, LB);
- }
return R;
} else if (cmd is AssumeCmd) {
AssumeCmd ac = (AssumeCmd)cmd;
|