diff --git a/Source/Core/CoreOptions.cs b/Source/Core/CoreOptions.cs index d60f52230..4e91977a2 100644 --- a/Source/Core/CoreOptions.cs +++ b/Source/Core/CoreOptions.cs @@ -107,6 +107,7 @@ public enum VerbosityLevel bool ConcurrentHoudini { get; } double VcsPathJoinMult { get; } bool VerifySeparately { get; } + bool KeepQuantifier { get; } public enum ProverWarnings { diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index ff4755836..06653bfe9 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/Source/ExecutionEngine/CommandLineOptions.cs @@ -1,11 +1,9 @@ using System; using System.Collections.Generic; using System.Collections.Specialized; -using System.Diagnostics; using System.Diagnostics.Contracts; using System.IO; using Microsoft.Boogie.SMTLib; -using VC; namespace Microsoft.Boogie { @@ -519,6 +517,11 @@ public bool PrintInlined { public int LiveVariableAnalysis { get; set; } = 1; + public bool KeepQuantifier { + get => keepQuantifier; + set => keepQuantifier = value; + } + public HashSet Libraries { get; set; } = new HashSet(); // Note that procsToCheck stores all patterns

supplied with /proc:

@@ -568,6 +571,7 @@ void ObjectInvariant5() private bool emitDebugInformation = true; private bool normalizeNames; private bool normalizeDeclarationOrder = true; + private bool keepQuantifier = false; public List Cho { get; set; } = new(); @@ -1322,7 +1326,8 @@ protected override bool ParseOption(string name, CommandLineParseState ps) ps.CheckBooleanFlag("trustSequentialization", x => trustSequentialization = x) || ps.CheckBooleanFlag("useBaseNameForFileName", x => UseBaseNameForFileName = x) || ps.CheckBooleanFlag("freeVarLambdaLifting", x => FreeVarLambdaLifting = x) || - ps.CheckBooleanFlag("warnNotEliminatedVars", x => WarnNotEliminatedVars = x) + ps.CheckBooleanFlag("warnNotEliminatedVars", x => WarnNotEliminatedVars = x) || + ps.CheckBooleanFlag("keepQuantifier", x => keepQuantifier = x) ) { // one of the boolean flags matched @@ -1933,6 +1938,11 @@ Track and report which program elements labeled with an report. This generalizes and replaces the previous (undocumented) `/printNecessaryAssertions` option. + /keepQuantifier + If pool-based quantifier instantiation creates instances of a quantifier + then keep the quantifier along with the instances. By default, the quantifier + is dropped if any instances are created. + ---- Verification-condition splitting -------------------------------------- /vcsMaxCost: diff --git a/Source/Provers/SMTLib/SMTLibOptions.cs b/Source/Provers/SMTLib/SMTLibOptions.cs index 354c91979..af4100123 100644 --- a/Source/Provers/SMTLib/SMTLibOptions.cs +++ b/Source/Provers/SMTLib/SMTLibOptions.cs @@ -1,5 +1,4 @@ using System; -using System.Collections.Generic; using Microsoft.Boogie.SMTLib; namespace Microsoft.Boogie diff --git a/Source/VCExpr/NormalizeNamer.cs b/Source/VCExpr/NormalizeNamer.cs index 8f0ebb0c1..b371210ba 100644 --- a/Source/VCExpr/NormalizeNamer.cs +++ b/Source/VCExpr/NormalizeNamer.cs @@ -1,7 +1,3 @@ -using System; -using System.Collections.Generic; -using System.Diagnostics.Contracts; - namespace Microsoft.Boogie.VCExprAST { public class NormalizeNamer : ScopedNamer diff --git a/Source/VCExpr/QuantifierInstantiationEngine.cs b/Source/VCExpr/QuantifierInstantiationEngine.cs index 1bae1b1cc..1f062ba91 100644 --- a/Source/VCExpr/QuantifierInstantiationEngine.cs +++ b/Source/VCExpr/QuantifierInstantiationEngine.cs @@ -374,17 +374,34 @@ private VCExpr LetConvert(VCExpr vcExpr) private VCExpr AugmentWithInstances(VCExprQuantifier quantifierExpr) { + var instances = quantifierInstantiationInfo[quantifierExpr].instances; + if (instances.Count == 0) + { + return quantifierExpr; + } if (quantifierExpr.Quan == Quantifier.ALL) { - return vcExprGen.And(quantifierExpr, - vcExprGen.NAry(VCExpressionGenerator.AndOp, - quantifierInstantiationInfo[quantifierExpr].instances.Values.ToList())); + var instantiatedConjuncts = vcExprGen.NAry(VCExpressionGenerator.AndOp, instances.Values.ToList()); + if (exprTranslator.GenerationOptions.Options.KeepQuantifier) + { + return vcExprGen.And(quantifierExpr, instantiatedConjuncts); + } + else + { + return instantiatedConjuncts; + } } else { - return vcExprGen.Or(quantifierExpr, - vcExprGen.NAry(VCExpressionGenerator.OrOp, - quantifierInstantiationInfo[quantifierExpr].instances.Values.ToList())); + var instantiatedDisjuncts = vcExprGen.NAry(VCExpressionGenerator.OrOp, instances.Values.ToList()); + if (exprTranslator.GenerationOptions.Options.KeepQuantifier) + { + return vcExprGen.Or(quantifierExpr, instantiatedDisjuncts); + } + else + { + return instantiatedDisjuncts; + } } } diff --git a/Source/VCExpr/RandomiseNamer.cs b/Source/VCExpr/RandomiseNamer.cs index 4a85f3ff4..6fe1ad021 100644 --- a/Source/VCExpr/RandomiseNamer.cs +++ b/Source/VCExpr/RandomiseNamer.cs @@ -1,5 +1,4 @@ using System; -using System.Diagnostics.Contracts; namespace Microsoft.Boogie.VCExprAST; diff --git a/Source/VCGeneration/Checker.cs b/Source/VCGeneration/Checker.cs index b0f145e5e..195361cfd 100644 --- a/Source/VCGeneration/Checker.cs +++ b/Source/VCGeneration/Checker.cs @@ -6,7 +6,6 @@ using Microsoft.Boogie.VCExprAST; using System.Diagnostics; using System.Threading.Tasks; -using Microsoft.Boogie.SMTLib; using VC; namespace Microsoft.Boogie diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index a4ac161a4..46fe6b792 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -8,9 +8,7 @@ using Microsoft.Boogie.GraphUtil; using System.Diagnostics.Contracts; using System.IO; -using System.Runtime.CompilerServices; using System.Threading.Tasks; -using VC; using Set = Microsoft.Boogie.GSet; namespace VC diff --git a/Source/VCGeneration/Counterexample.cs b/Source/VCGeneration/Counterexample.cs index 11e5ff3d9..31cafb18c 100644 --- a/Source/VCGeneration/Counterexample.cs +++ b/Source/VCGeneration/Counterexample.cs @@ -7,7 +7,6 @@ using Microsoft.Boogie.VCExprAST; using VC; using VCGeneration; -using Set = Microsoft.Boogie.GSet; namespace Microsoft.Boogie { diff --git a/Source/VCGeneration/ModelViewInfo.cs b/Source/VCGeneration/ModelViewInfo.cs index 8aedd87bd..2e9d547ed 100644 --- a/Source/VCGeneration/ModelViewInfo.cs +++ b/Source/VCGeneration/ModelViewInfo.cs @@ -1,8 +1,6 @@ using System.Collections.Generic; using Microsoft.Boogie; -using Bpl = Microsoft.Boogie; using System.Diagnostics.Contracts; -using Set = Microsoft.Boogie.GSet; namespace VC { diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index aba8e05df..7b397fa0b 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -9,7 +9,6 @@ using Microsoft.BaseTypes; using Microsoft.Boogie.VCExprAST; using Microsoft.Boogie.SMTLib; -using VCGeneration; using System.Threading.Tasks; namespace VC diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 5a296ffc4..19cfe5426 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -2,10 +2,8 @@ using System.Collections; using System.Collections.Generic; using System.Diagnostics; -using System.Linq; using System.IO; using Microsoft.Boogie; -using Microsoft.Boogie.GraphUtil; using System.Diagnostics.Contracts; using Microsoft.BaseTypes; using Microsoft.Boogie.VCExprAST; diff --git a/Source/VCGeneration/VCGenOptions.cs b/Source/VCGeneration/VCGenOptions.cs index 765e1772b..6fc1ca5f5 100644 --- a/Source/VCGeneration/VCGenOptions.cs +++ b/Source/VCGeneration/VCGenOptions.cs @@ -1,5 +1,3 @@ -using VC; - namespace Microsoft.Boogie; public interface VCGenOptions : SMTLibOptions diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 67d8b54f4..e26ed57c7 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -2,8 +2,6 @@ using Microsoft.Boogie; using Microsoft.Boogie.VCExprAST; using System.Diagnostics.Contracts; -using System.Collections.Generic; -using System.Runtime.CompilerServices; using Microsoft.BaseTypes; namespace VC diff --git a/Test/civl/inductive-sequentialization/ChangRoberts.bpl b/Test/civl/inductive-sequentialization/ChangRoberts.bpl index 61d4b8a4a..bc2174aaf 100644 --- a/Test/civl/inductive-sequentialization/ChangRoberts.bpl +++ b/Test/civl/inductive-sequentialization/ChangRoberts.bpl @@ -115,10 +115,10 @@ modifies channel; assume {:add_to_pool "INV2", Next(Max(id))} true; havoc channel; - assume (forall i:int :: 1 <= i && i <= n ==> channel[Next(i)] == EmptyChannel()[id[i] := 1 ]); + assume (forall i:int :: {:add_to_pool "CHANNEL_INV", i} 1 <= i && i <= n ==> channel[Next(i)] == EmptyChannel()[id[i] := 1 ]); assume (forall i:int :: i < 1 || i > n ==> channel[i] == EmptyChannel()); call create_asyncs((lambda pa:P :: Pid(pa->pid->val))); - assume (forall i:int, msg:int :: Pid(i) && channel[i][msg] > 0 ==> msg == id[Prev(i)]); + assume (forall i:int, msg:int :: {:add_to_pool "CHANNEL_INV", Prev(i)} Pid(i) && channel[i][msg] > 0 ==> msg == id[Prev(i)]); } action {:layer 2} diff --git a/Test/civl/inductive-sequentialization/PingPong.bpl b/Test/civl/inductive-sequentialization/PingPong.bpl index 13031a2ef..1cf3f53ba 100644 --- a/Test/civl/inductive-sequentialization/PingPong.bpl +++ b/Test/civl/inductive-sequentialization/PingPong.bpl @@ -49,7 +49,7 @@ modifies channel; assert handles == BothHandles(cid); assert channel[cid] == ChannelPair(EmptyChannel(), EmptyChannel()); - assume {:add_to_pool "INV", c, c+1} 0 < c; + assume {:add_to_pool "INV", 0, c, c+1} 0 < c; if (*) { channel[cid] := ChannelPair(EmptyChannel(), EmptyChannel()[c := 1]); call create_async(PONG(c, One(Right(cid)))); @@ -75,7 +75,7 @@ action {:layer 2} PING' (x: int, {:linear_in} p: One ChannelHandle) creates PING; modifies channel; { - assert (exists {:pool "INV"} m:int :: channel[p->val->cid]->left[m] > 0); + assert (exists {:pool "INV"} m:int :: {:add_to_pool "INV", m} channel[p->val->cid]->left[m] > 0); assert (forall m:int :: channel[p->val->cid]->right[m] == 0); call PING(x, p); } @@ -84,7 +84,7 @@ action {:layer 2} PONG' (y: int, {:linear_in} p: One ChannelHandle) creates PONG; modifies channel; { - assert (exists {:pool "INV"} m:int :: channel[p->val->cid]->right[m] > 0); + assert (exists {:pool "INV"} m:int :: {:add_to_pool "INV", m} channel[p->val->cid]->right[m] > 0); assert (forall m:int :: channel[p->val->cid]->left[m] == 0); call PONG(y, p); } diff --git a/Test/civl/inductive-sequentialization/ProducerConsumer.bpl b/Test/civl/inductive-sequentialization/ProducerConsumer.bpl index 7e16dc255..8a8832875 100644 --- a/Test/civl/inductive-sequentialization/ProducerConsumer.bpl +++ b/Test/civl/inductive-sequentialization/ProducerConsumer.bpl @@ -57,7 +57,7 @@ modifies channels; C := channel->C; head := channel->head; tail := channel->tail; - assume {:add_to_pool "INV1", c} 0 < c; + assume {:add_to_pool "INV1", c, c+1} 0 < c; if (*) { assume head == tail; call create_async(PRODUCER(c, One(Send(cid)))); diff --git a/Test/civl/paxos/PaxosActions.bpl b/Test/civl/paxos/PaxosActions.bpl index a1f3cbb78..44c72dcc3 100644 --- a/Test/civl/paxos/PaxosActions.bpl +++ b/Test/civl/paxos/PaxosActions.bpl @@ -56,7 +56,7 @@ modifies decision; assert voteInfo[r] is Some; assert voteInfo[r]->t->value == v; - assume {:add_to_pool "Round", r} true; + assume {:add_to_pool "Round", r} {:add_to_pool "NodeSet", q} true; if (*) { assume IsSubset(q, voteInfo[r]->t->ns) && IsQuorum(q); diff --git a/Test/inst/ying_sort.bpl b/Test/inst/ying_sort.bpl index 263007517..4c148955b 100644 --- a/Test/inst/ying_sort.bpl +++ b/Test/inst/ying_sort.bpl @@ -7,7 +7,7 @@ function {:inline} InOrder(x: int, y: int, z: int): bool { function {:inline} Permutation(A: Vec E, B: Vec E): bool { Vec_Len(A) == Vec_Len(B) && - (forall {:pool "A"} k: int :: {:add_to_pool "A", k} InOrder(0, k, Vec_Len(A)) ==> + (forall {:pool "A"} k: int :: {:add_to_pool "A", k} {:add_to_pool "B", k} InOrder(0, k, Vec_Len(A)) ==> (exists {:pool "B"} k': int :: {:add_to_pool "B", k'} InOrder(0, k', Vec_Len(B)) ==> Vec_Nth(A, k) == Vec_Nth(B, k'))) }