Added quantifier instantiation option (#857)

Added option ```/keepQuantifier``` which allows the original quantifier to be kept along with the instances. By default, the original quantifier is dropped if any instances are found. More hints had to be added to a few Civl benchmarks. Co-authored-by: Shaz Qadeer <[email protected]>
boogie-org · Mar 8, 2024 · cf5609f · cf5609f
1 parent 11660fd
commit cf5609f
Show file tree

Hide file tree

Showing 19 changed files with 45 additions and 36 deletions.
diff --git 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
@@ -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<string> Libraries { get; set; } = new HashSet<string>();
 
     // Note that procsToCheck stores all patterns <p> supplied with /proc:<p>
@@ -568,6 +571,7 @@ void ObjectInvariant5()
     private bool emitDebugInformation = true;
     private bool normalizeNames;
     private bool normalizeDeclarationOrder = true;
+    private bool keepQuantifier = false;
 
     public List<CoreOptions.ConcurrentHoudiniOptions> 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:<f>

diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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<object>;
 
 namespace VC

diff --git 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<object>;
 
 namespace Microsoft.Boogie
 {

diff --git 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<object>;
 
 namespace VC
 {

diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -7,7 +7,7 @@ function {:inline} InOrder(x: int, y: int, z: int): bool {
 
 function {:inline} Permutation<E>(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')))
 }