summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Binaries/DafnyPrelude.bpl15
-rw-r--r--Source/VCExpr/TypeErasure.cs4
-rw-r--r--Source/VCExpr/TypeErasureArguments.cs8
-rw-r--r--Source/VCExpr/TypeErasurePremisses.cs12
-rw-r--r--Source/VCExpr/VCExprAST.cs8
-rw-r--r--Test/dafny0/Answer7
-rw-r--r--Test/dafny0/SmallTests.dfy16
7 files changed, 48 insertions, 22 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 30992d46..94a8833a 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -137,11 +137,16 @@ axiom (forall<T> s0: Seq T, s1: Seq T, x: T ::
{ Seq#Contains(Seq#Append(s0, s1), x) }
Seq#Contains(Seq#Append(s0, s1), x) <==>
Seq#Contains(s0, x) || Seq#Contains(s1, x));
-axiom (forall<T> s: Seq T, i: int, v: T, len: int, x: T ::
- { Seq#Contains(Seq#Build(s, i, v, len), x) }
- Seq#Contains(Seq#Build(s, i, v, len), x) <==>
- (0 <= i && i < len && x == v) ||
- (exists j: int :: { Seq#Index(s,j) } 0 <= j && j < Seq#Length(s) && j < len && j!=i && Seq#Index(s,j) == x));
+axiom (forall<T> i: int, v: T, len: int, x: T ::
+ { Seq#Contains(Seq#Build(Seq#Empty(), i, v, len), x) }
+ 0 <= i && i < len ==>
+ (Seq#Contains(Seq#Build(Seq#Empty(), i, v, len), x) <==> x == v));
+axiom (forall<T> s: Seq T, i0: int, v0: T, len0: int, i1: int, v1: T, len1: int, x: T ::
+ { Seq#Contains(Seq#Build(Seq#Build(s, i0, v0, len0), i1, v1, len1), x) }
+ 0 <= i0 && i0 < len0 && len0 <= i1 && i1 < len1 ==>
+ (Seq#Contains(Seq#Build(Seq#Build(s, i0, v0, len0), i1, v1, len1), x) <==>
+ v1 == x ||
+ Seq#Contains(Seq#Build(s, i0, v0, len0), x)));
axiom (forall<T> s: Seq T, n: int, x: T ::
{ Seq#Contains(Seq#Take(s, n), x) }
Seq#Contains(Seq#Take(s, n), x) <==>
diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 93adec82..fb91d326 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -287,7 +287,7 @@ namespace Microsoft.Boogie.TypeErasure {
return eq;
return Gen.Forall(quantifiedVars, new List<VCTrigger/*!*/>(),
- "ctor:" + typeRepr.Name, eq);
+ "ctor:" + typeRepr.Name, -1, eq);
}
// generate an axiom (forall x0, x1, ... :: invFun(fun(x0, x1, ...) == xi)
@@ -305,7 +305,7 @@ namespace Microsoft.Boogie.TypeErasure {
List<VCTrigger/*!*/>/*!*/ triggers = HelperFuns.ToList(Gen.Trigger(true, HelperFuns.ToList(funApp)));
Contract.Assert(cce.NonNullElements(triggers));
- return Gen.Forall(quantifiedVars, triggers, "typeInv:" + invFun.Name, eq);
+ return Gen.Forall(quantifiedVars, triggers, "typeInv:" + invFun.Name, -1, eq);
}
///////////////////////////////////////////////////////////////////////////
diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs
index 8187fa10..57218a73 100644
--- a/Source/VCExpr/TypeErasureArguments.cs
+++ b/Source/VCExpr/TypeErasureArguments.cs
@@ -60,7 +60,7 @@ namespace Microsoft.Boogie.TypeErasure {
List<VCTrigger/*!*/>/*!*/ triggers;
VCExprVar/*!*/ var;
VCExpr/*!*/ eq = GenReverseCastEq(castToU, castFromU, out var, out triggers);
- return Gen.Forall(HelperFuns.ToList(var), triggers, "cast:" + castFromU.Name, eq);
+ return Gen.Forall(HelperFuns.ToList(var), triggers, "cast:" + castFromU.Name, -1, eq);
}
protected override VCExpr GenCastTypeAxioms(Function castToU, Function castFromU) {
@@ -316,8 +316,7 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null);
VCExpr/*!*/ eq = Gen.Eq(selectExpr, val);
Contract.Assert(eq != null);
- return Gen.Forall(quantifiedVars, new List<VCTrigger/*!*/>(),
- "mapAx0:" + select.Name, eq);
+ return Gen.Forall(quantifiedVars, new List<VCTrigger/*!*/>(), "mapAx0:" + select.Name, 0, eq);
}
private VCExpr/*!*/ GenMapAxiom1(Function/*!*/ select, Function/*!*/ store,
@@ -397,8 +396,7 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null);
Contract.Assert(indexesEq != null);
VCExpr/*!*/ matrix = Gen.Or(indexesEq, selectEq);
Contract.Assert(matrix != null);
- VCExpr/*!*/ conjunct = Gen.Forall(quantifiedVars, triggers,
- "mapAx1:" + select.Name + ":" + n, matrix);
+ VCExpr/*!*/ conjunct = Gen.Forall(quantifiedVars, triggers, "mapAx1:" + select.Name + ":" + n, 0, matrix);
Contract.Assert(conjunct != null);
axiom = Gen.AndSimp(axiom, conjunct);
n = n + 1;
diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index b20fa143..df14eb01 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -119,7 +119,7 @@ namespace Microsoft.Boogie.TypeErasure
new Dictionary<TypeVariable/*!*/, VCExpr/*!*/>());
VCExpr/*!*/ matrix = Gen.ImpliesSimp(premiss, eq);
Contract.Assert(matrix != null);
- return Gen.Forall(HelperFuns.ToList(var), triggers, "cast:" + castFromU.Name, matrix);
+ return Gen.Forall(HelperFuns.ToList(var), triggers, "cast:" + castFromU.Name, -1, matrix);
}
protected override VCExpr GenCastTypeAxioms(Function castToU, Function castFromU) {
@@ -489,7 +489,7 @@ namespace Microsoft.Boogie.TypeErasure
if (boundVars.Count > 0) {
List<VCTrigger/*!*/> triggers = HelperFuns.ToList(Gen.Trigger(true, HelperFuns.ToList(funApp)));
Contract.Assert(cce.NonNullElements(triggers));
- return Gen.Forall(boundVars, triggers, "funType:" + fun.Name, conclusionWithPremisses);
+ return Gen.Forall(boundVars, triggers, "funType:" + fun.Name, -1, conclusionWithPremisses);
} else {
return conclusionWithPremisses;
}
@@ -846,7 +846,7 @@ namespace Microsoft.Boogie.TypeErasure
} else {
body = Gen.Let(letBindings_Implicit, Gen.Let(letBindings_Explicit, Gen.ImpliesSimp(ante, eq)));
}
- return Gen.Forall(quantifiedVars, new List<VCTrigger/*!*/>(), "mapAx0:" + select.Name, body);
+ return Gen.Forall(quantifiedVars, new List<VCTrigger/*!*/>(), "mapAx0:" + select.Name, 0, body);
}
private VCExpr GenMapAxiom1(Function select, Function store, Type mapResult, List<TypeVariable/*!*/>/*!*/ explicitSelectParams) {
@@ -924,8 +924,7 @@ namespace Microsoft.Boogie.TypeErasure
for (int i = 0; i < arity; ++i) {
VCExpr/*!*/ indexesEq = Gen.Eq(indexes0[i], indexes1[i]);
VCExpr/*!*/ matrix = Gen.Or(indexesEq, selectEq);
- VCExpr/*!*/ conjunct = Gen.Forall(quantifiedVars, triggers,
- "mapAx1:" + select.Name + ":" + i, matrix);
+ VCExpr/*!*/ conjunct = Gen.Forall(quantifiedVars, triggers, "mapAx1:" + select.Name + ":" + i, 0, matrix);
Contract.Assert(indexesEq != null);
Contract.Assert(matrix != null);
Contract.Assert(conjunct != null);
@@ -940,8 +939,7 @@ namespace Microsoft.Boogie.TypeErasure
typesEq = Gen.AndSimp(typesEq, Gen.Eq(b.V, b.E));
}
VCExpr/*!*/ matrix2 = Gen.Or(typesEq, selectEq);
- VCExpr/*!*/ conjunct2 = Gen.Forall(quantifiedVars, triggers,
- "mapAx2:" + select.Name, matrix2);
+ VCExpr/*!*/ conjunct2 = Gen.Forall(quantifiedVars, triggers, "mapAx2:" + select.Name, 0, matrix2);
axiom = Gen.AndSimp(axiom, conjunct2);
return axiom;
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index bb0539bf..38541881 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -587,14 +587,18 @@ namespace Microsoft.Boogie {
Contract.Ensures(Contract.Result<VCExpr>() != null);
return Quantify(Quantifier.ALL, typeParams, vars, triggers, infos, body);
}
- public VCExpr Forall(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, string qid, VCExpr body) {
+ public VCExpr Forall(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, string qid, int weight, VCExpr body) {
Contract.Requires(body != null);
Contract.Requires(qid != null);
Contract.Requires(cce.NonNullElements(triggers));
Contract.Requires(cce.NonNullElements(vars));
Contract.Ensures(Contract.Result<VCExpr>() != null);
+ QKeyValue kv = null;
+ if (0 <= weight) {
+ kv = new QKeyValue(Token.NoToken, "weight", new List<object>() { new LiteralExpr(Token.NoToken, BigNum.FromInt(0)) }, null);
+ }
return Quantify(Quantifier.ALL, new List<TypeVariable/*!*/>(), vars,
- triggers, new VCQuantifierInfos(qid, -1, false, null), body);
+ triggers, new VCQuantifierInfos(qid, -1, false, kv), body);
}
public VCExpr Forall(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCExpr body) {
Contract.Requires(body != null);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 25180c13..51d3efcd 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -200,8 +200,13 @@ Execution trace:
(0,0): anon24_Then
(0,0): anon15
(0,0): anon25_Else
+SmallTests.dfy(347,12): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon8_Then
+ (0,0): anon7
-Dafny program verifier finished with 43 verified, 14 errors
+Dafny program verifier finished with 44 verified, 15 errors
-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index ac7286e9..8393b1c7 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -330,3 +330,19 @@ class SomeType
}
}
}
+
+// ----------------------- tests of some theory axioms --------
+
+method TestSequences0()
+{
+ var s := [0, 2, 4];
+ if (*) {
+ assert 4 in s;
+ assert 0 in s;
+ assert 1 !in s;
+ } else {
+ assert 2 in s;
+ assert exists n :: n in s && -3 <= n && n < 2;
+ }
+ assert 7 in s; // error
+}
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-19 07:45:27 +0000