disabled quantifier merging, except when no triggers are provided (as discussed with Rustan)

3 files changed, 13 insertions, 14 deletions

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 63474c69..10a13511 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -579,15 +579,17 @@ namespace Microsoft.Boogie {
       }

     }

 

-    // if the user says ( forall x :: forall y :: { f(x,y) } ... ) we transform it to

-    // (forall x, y :: { f(x,y) } ... ) otherwise the prover ignores the trigger

+    // if the user says ( forall x :: forall y ::  ... ) and specifies *no* triggers, we transform it to

+    // (forall x, y ::  ... ) which may help the prover to pick trigger terms

+    //

+    // (Note: there used to be a different criterion here, which allowed merging when triggers were specified, which could cause prover errors due to resulting unbound variables in the triggers)

     private void MergeAdjecentQuantifier() {

       QuantifierExpr qbody = Body as QuantifierExpr;

       if (!(qbody != null && (qbody is ForallExpr) == (this is ForallExpr) && Triggers == null)) {

         return;

       }

       qbody.MergeAdjecentQuantifier();

-      if (qbody.Triggers == null) {

+      if (this.Triggers != null || qbody.Triggers != null) {

         return;

       }

       Body = qbody.Body;

diff --git a/Test/test0/Answer b/Test/test0/Answer
index f92dd1dc..f4e2b981 100644
--- a/Test/test0/Answer
+++ b/Test/test0/Answer
@@ -21,13 +21,10 @@ Triggers1.bpl(82,7): Error: trigger must mention all quantified variables, but d
 Triggers1.bpl(94,16): Error: a matching pattern must be more than just a variable by itself: x

 Triggers1.bpl(95,16): Error: a matching pattern must be more than just a variable by itself: g

 Triggers1.bpl(105,40): Error: trigger must mention all quantified variables, but does not mention: y

-Triggers1.bpl(106,40): Error: trigger must mention all quantified variables, but does not mention: x

 Triggers1.bpl(109,57): Error: trigger must mention all quantified variables, but does not mention: z

-Triggers1.bpl(110,57): Error: trigger must mention all quantified variables, but does not mention: y

-Triggers1.bpl(111,57): Error: trigger must mention all quantified variables, but does not mention: x

 Triggers1.bpl(119,33): Error: cannot refer to a global variable in this context: h1

 Triggers1.bpl(120,33): Error: cannot refer to a global variable in this context: h0

-23 name resolution errors detected in Triggers1.bpl

+20 name resolution errors detected in Triggers1.bpl

 const x: int;

 

 const y: int;

diff --git a/Test/test0/Triggers1.bpl b/Test/test0/Triggers1.bpl
index 02c63406..d079ea03 100644
--- a/Test/test0/Triggers1.bpl
+++ b/Test/test0/Triggers1.bpl
@@ -99,17 +99,17 @@ axiom (forall x: int, y: int ::
        {:nopats f(g,g) }              // but it is okay not to mention the bound variables (in a pattern exclusion)

        x < y);

 

-// --- merging of nested quantifiers

+// --- merging of nested quantifiers (disabled unless both have no triggers)

 

-axiom (forall x:int :: (forall y:int :: { f(x,y) } f(x,y) > 0)); // OK

+axiom (forall x:int :: (forall y:int :: { f(x,y) } f(x,y) > 0)); // OK, but no merging - outer quantifier has no trigger

 axiom (forall x:int :: (forall y:int :: { f(x,x) } f(x,x) > 0)); // error

-axiom (forall x:int :: (forall y:int :: { f(y,y) } f(y,y) > 0)); // error

+axiom (forall x:int :: (forall y:int :: { f(y,y) } f(y,y) > 0)); // OK - no merging

 

 // three levels

-axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y) } f(y,y) > 0))); // error

-axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,z) } f(y,y) > 0))); // error

-axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(y,z) } f(y,y) > 0))); // error

-axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y), f(y,z) } f(y,y) > 0))); // OK

+axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y) } f(y,y) > 0))); // error - z not mentioned

+axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,z) } f(y,y) > 0))); // OK - only outer two quantifiers are merged

+//axiom (forall x:int :: (forall y:int :: (forall z:int :: f(y,y) > 0))); // OK - all three are merged

+axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y), f(y,z) } f(y,y) > 0))); // OK - but not a trigger for outer x,y (which get merged)

 

 // --- no free variables