diff options
| author |  wuestholz <unknown> | 2015-01-30 12:52:21 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2015-01-30 12:52:21 +0100 |
| commit | 994fdafa5e496c007e78274093f7b02fa2e8dd06 (patch) | |
| tree | 8a9247151dcf4e9d51101ffdbea81ed463eb8ab3 | |
| parent | 400c69b10f9b7e6abd0fe9518a0d8be5508bf093 (diff) | |
Minor change to the encoding of partially verified assertions as VC
| -rw-r--r-- | Source/VCExpr/VCExprAST.cs | 4 | ||||
| -rw-r--r-- | Source/VCGeneration/Wlp.cs | 55 |
2 files changed, 34 insertions, 25 deletions
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 41f1e207..4f8dc08e 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -267,7 +267,7 @@ namespace Microsoft.Boogie { return True;
return Or(e0, e1);
}
- public VCExpr ImpliesSimp(VCExpr e0, VCExpr e1) {
+ public VCExpr ImpliesSimp(VCExpr e0, VCExpr e1, bool aggressive = true) {
Contract.Requires(e1 != null);
Contract.Requires(e0 != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
@@ -278,7 +278,7 @@ namespace Microsoft.Boogie { if (e0.Equals(False) || e1.Equals(True))
return True;
// attempt to save on the depth of expressions (to reduce chances of stack overflows)
- while (e1 is VCExprBinary) {
+ while (aggressive && e1 is VCExprBinary) {
VCExprBinary n = (VCExprBinary)e1;
if (n.Op == ImpliesOp) {
if (AndSize(n[0]) <= AndSize(e0)) {
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index cd735501..45e511f0 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -26,13 +26,6 @@ namespace VC { public int AssertionCount; // counts the number of assertions for which Wlp has been computed
public bool isPositiveContext;
- int letBindingCount;
- public string FreshLetBindingName()
- {
- var c = System.Threading.Interlocked.Increment(ref letBindingCount);
- return string.Format("v##let##{0}", c);
- }
-
public VCContext(Dictionary<int, Absy> label2absy, ProverContext ctxt, bool isPositiveContext = true)
{
Contract.Requires(ctxt != null);
@@ -104,41 +97,57 @@ namespace VC { Contract.Assert(gen != null);
if (cmd is AssertCmd) {
AssertCmd ac = (AssertCmd)cmd;
- ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext;
+
+ var isFullyVerified = false;
+ if (ac.VerifiedUnder != null)
+ {
+ var litExpr = ac.VerifiedUnder as LiteralExpr;
+ isFullyVerified = litExpr != null && litExpr.IsTrue;
+ }
+
+ if (!isFullyVerified)
+ {
+ ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext;
+ }
+
VCExpr C = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);
+
VCExpr VU = null;
- if (ac.VerifiedUnder != null)
+ if (!isFullyVerified)
{
- VU = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.VerifiedUnder);
+ if (ac.VerifiedUnder != null)
+ {
+ VU = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.VerifiedUnder);
+ }
+ ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext;
}
- ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext;
VCExpr R = null;
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
R = gen.Implies(C, N);
} else {
- int id = ac.UniqueId;
- if (ctxt.Label2absy != null) {
- ctxt.Label2absy[id] = ac;
- }
-
var subsumption = Subsumption(ac);
if (subsumption == CommandLineOptions.SubsumptionOption.Always
|| (subsumption == CommandLineOptions.SubsumptionOption.NotForQuantifiers && !(C is VCExprQuantifier)))
{
- N = gen.ImpliesSimp(C, N);
+ N = gen.ImpliesSimp(C, N, false);
}
- if (VU != null)
+ if (isFullyVerified)
+ {
+ return N;
+ }
+ else if (VU != null)
{
- var litExpr = ac.VerifiedUnder as LiteralExpr;
- if (litExpr != null && litExpr.IsTrue)
- {
- return N;
- }
C = gen.OrSimp(VU, C);
}
+ int id = ac.UniqueId;
+ if (ctxt.Label2absy != null)
+ {
+ ctxt.Label2absy[id] = ac;
+ }
+
ctxt.AssertionCount++;
if (ctxt.ControlFlowVariableExpr == null) {
|