Merge

5 files changed, 21 insertions, 15 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/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index 00e1a5c6..a1240c30 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -2093,12 +2093,12 @@ Contract.Requires(that != null);
     private static int MinBitsFor(Type t) {

       Contract.Requires(t != null);

       Contract.Requires(t.IsBv);

+      Contract.Ensures(0 <= Contract.Result<int>());

 

       if (t is TypeSynonymAnnotation) {

         return MinBitsFor(((TypeSynonymAnnotation)t).ExpandedType);

       }

 

-      Contract.Ensures(0 <= Contract.Result<int>());

       if (t is BvType) {

         return t.BvBits;

       } else {

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 9f73e4a1..57ef660d 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -3724,6 +3724,13 @@ namespace Microsoft.Boogie.Houdini {
             {

                 return (elem as Model.Boolean).Value;

             }

+            if (elem is Model.DatatypeValue && (elem as Model.DatatypeValue).Arguments.Length == 1 &&

+                (elem as Model.DatatypeValue).ConstructorName == "-" &&

+                (elem as Model.DatatypeValue).Arguments[0] is Model.Integer)

+            {

+                // negative number as "-" @ int

+                return Microsoft.Basetypes.BigNum.FromInt(-1 * ((elem as Model.DatatypeValue).Arguments[0] as Model.Integer).AsInt());

+            }

             throw new NotImplementedException("Cannot yet handle this Model.Element type");

         }

 

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