diff options
| author |  Unknown <Alex@Mehldau.inf.ethz.ch> | 2014-03-03 13:56:55 +0100 |
|---|---|---|
| committer | Unknown <Alex@Mehldau.inf.ethz.ch> | 2014-03-03 13:56:55 +0100 |
| commit | 2b2d7c7f4ec6226c54ad664ce390fefdaf8fecaf (patch) | |
| tree | 76e38254c3e129022d0454ad0042803b946583ef /Test/test0 | |
| parent | 7a5fa3b224d6cf8015bd9792f7bff5074f82932d (diff) | |
disabled quantifier merging, except when no triggers are provided (as discussed with Rustan)
Diffstat (limited to 'Test/test0')
| -rw-r--r-- | Test/test0/Answer | 5 | ||||
| -rw-r--r-- | Test/test0/Triggers1.bpl | 14 |
2 files changed, 8 insertions, 11 deletions
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
|