summaryrefslogtreecommitdiff
path: root/Source/VCExpr
diff options
context:
space:
mode:
authorGravatar tabarbe <unknown>2010-08-27 21:52:03 +0000
committerGravatar tabarbe <unknown>2010-08-27 21:52:03 +0000
commitf09bf83d24438d712021ada6fab252b0f7f11986 (patch)
tree8f17ca3c0a3cb1462e9742c19a826fe8a46e5e32 /Source/VCExpr
parentc333ecd2f30badea143e79f5f944a8c63398b959 (diff)
Boogie: Commented out all occurences of repeated inherited contracts - makes fewer error messages when compiling with runtime checking on.
Diffstat (limited to 'Source/VCExpr')
-rw-r--r--Source/VCExpr/BigLiteralAbstracter.cs83
-rw-r--r--Source/VCExpr/Boogie2VCExpr.cs197
-rw-r--r--Source/VCExpr/SimplifyLikeLineariser.cs683
-rw-r--r--Source/VCExpr/VCExprAST.cs221
-rw-r--r--Source/VCExpr/VCExprASTPrinter.cs300
-rw-r--r--Source/VCExpr/VCExprASTVisitors.cs1282
6 files changed, 1420 insertions, 1346 deletions
diff --git a/Source/VCExpr/BigLiteralAbstracter.cs b/Source/VCExpr/BigLiteralAbstracter.cs
index 63d87e17..7eb93541 100644
--- a/Source/VCExpr/BigLiteralAbstracter.cs
+++ b/Source/VCExpr/BigLiteralAbstracter.cs
@@ -15,23 +15,24 @@ using Microsoft.Basetypes;
// constants. This is necessary for Simplify, which cannot deal with
// literals larger than 32 bits
-namespace Microsoft.Boogie.VCExprAST
-{
+namespace Microsoft.Boogie.VCExprAST {
public class BigLiteralAbstracter : MutatingVCExprVisitor<bool>, ICloneable {
- public BigLiteralAbstracter(VCExpressionGenerator gen) :base(gen){
+ public BigLiteralAbstracter(VCExpressionGenerator gen)
+ : base(gen) {
Contract.Requires(gen != null);
DummyVar = gen.Variable("x", Type.Int);
- IncAxioms = new List<VCExpr> ();
- Literals = new List<KeyValuePair<BigNum, VCExprVar>> ();
+ IncAxioms = new List<VCExpr>();
+ Literals = new List<KeyValuePair<BigNum, VCExprVar>>();
}
- private BigLiteralAbstracter(BigLiteralAbstracter abstracter) :base(abstracter.Gen){
+ private BigLiteralAbstracter(BigLiteralAbstracter abstracter)
+ : base(abstracter.Gen) {
Contract.Requires(abstracter != null);
DummyVar = abstracter.DummyVar;
- IncAxioms = new List<VCExpr> (abstracter.IncAxioms);
- Literals = new List<KeyValuePair<BigNum, VCExprVar>> (abstracter.Literals);
+ IncAxioms = new List<VCExpr>(abstracter.IncAxioms);
+ Literals = new List<KeyValuePair<BigNum, VCExprVar>>(abstracter.Literals);
}
public Object Clone() {
@@ -59,10 +60,9 @@ namespace Microsoft.Boogie.VCExprAST
private readonly List<VCExpr/*!*/>/*!*/ IncAxioms;
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(cce.NonNullElements(IncAxioms));
-}
+ void ObjectInvariant() {
+ Contract.Invariant(cce.NonNullElements(IncAxioms));
+ }
private void AddAxiom(VCExpr/*!*/ axiom) {
Contract.Requires(axiom != null);
@@ -72,7 +72,7 @@ void ObjectInvariant()
// Return all axioms that were added since the last time NewAxioms
// was called
public VCExpr GetNewAxioms() {
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
VCExpr res = Gen.NAry(VCExpressionGenerator.AndOp, IncAxioms);
IncAxioms.Clear();
return res;
@@ -86,39 +86,38 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
private readonly List<KeyValuePair<BigNum, VCExprVar/*!*/>>/*!*/ Literals;
[ContractInvariantMethod]
-void ObjectInvariat()
-{
- Contract.Invariant(Literals!=null);
- Contract.Invariant(Contract.ForAll(Literals,i=>i.Value!=null));
-}
+ void ObjectInvariat() {
+ Contract.Invariant(Literals != null);
+ Contract.Invariant(Contract.ForAll(Literals, i => i.Value != null));
+ }
+
-
private class EntryComparerC : IComparer<KeyValuePair<BigNum, VCExprVar/*!*/>> {
public int Compare(KeyValuePair<BigNum, VCExprVar/*!*/> a,
- KeyValuePair<BigNum, VCExprVar/*!*/> b) {Contract.Requires(a.Value!=null);
- Contract.Requires(b.Value!=null);
+ KeyValuePair<BigNum, VCExprVar/*!*/> b) {
+ //Contract.Requires(a.Value!=null);
+ //Contract.Requires(b.Value!=null);
return a.Key.CompareTo(b.Key);
}
}
- private static readonly EntryComparerC EntryComparer = new EntryComparerC ();
+ private static readonly EntryComparerC EntryComparer = new EntryComparerC();
// variable used when searching for entries in the literal list
private readonly VCExprVar/*!*/ DummyVar;
[ContractInvariantMethod]
-void ObjectInvarint()
-{
- Contract.Invariant(DummyVar!=null);
-}
+ void ObjectInvarint() {
+ Contract.Invariant(DummyVar != null);
+ }
////////////////////////////////////////////////////////////////////////////
-
+
// Construct an expression to represent the given (large) integer
// literal. Constants are defined and axiomatised if necessary
private VCExpr Represent(BigNum lit) {
-Contract.Requires((NegConstantDistance > lit || lit > ConstantDistance));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires((NegConstantDistance > lit || lit > ConstantDistance));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
if (lit.IsNegative)
return Gen.Function(VCExpressionGenerator.SubOp,
@@ -128,14 +127,14 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
}
private VCExpr RepresentPos(BigNum lit) {
-Contract.Requires((lit > ConstantDistance));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
-
+ Contract.Requires((lit > ConstantDistance));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
int index = GetIndexFor(lit);
if (index >= 0)
// precise match
return Literals[index].Value;
-
+
// check whether a constant is defined that is at most
// ConstantDistance away from lit
index = ~index;
@@ -168,33 +167,33 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
}
private VCExpr AddConstantFor(BigNum lit) {
-Contract.Requires((lit > ConstantDistance));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
-
+ Contract.Requires((lit > ConstantDistance));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
VCExprVar res = Gen.Variable("int#" + lit, Type.Int);
int index = GetIndexFor(lit);
Contract.Assert(index < 0);
index = ~index;
Literals.Insert(index, new KeyValuePair<BigNum, VCExprVar>(lit, res));
-
+
// relate the new constant to the predecessor and successor
if (index > 0)
DefineRelationship(Literals[index - 1].Value, Literals[index - 1].Key,
res, lit);
else
DefineRelationship(Gen.Integer(BigNum.ZERO), BigNum.ZERO, res, lit);
-
+
if (index < Literals.Count - 1)
DefineRelationship(res, lit,
Literals[index + 1].Value, Literals[index + 1].Key);
return res;
}
-
+
private void DefineRelationship(VCExpr/*!*/ aExpr, BigNum aValue,
- VCExpr/*!*/ bExpr, BigNum bValue)
- {Contract.Requires(aValue < bValue);
+ VCExpr/*!*/ bExpr, BigNum bValue) {
+ Contract.Requires(aValue < bValue);
Contract.Requires(aExpr != null);
Contract.Requires(bExpr != null);
@@ -219,7 +218,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
public override VCExpr Visit(VCExprLiteral node, bool arg) {
Contract.Requires(node != null);
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
VCExprIntLit intLit = node as VCExprIntLit;
if (intLit != null) {
if (NegConstantDistance > intLit.Val || intLit.Val > ConstantDistance)
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index a2b0c041..b90196e2 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -200,10 +200,10 @@ namespace Microsoft.Boogie.VCExprAST {
VCExprVar res;
foreach (Dictionary<VarKind/*!*/, VCExprVar/*!*/>/*!*/ d in Mapping) {
//Contract.Assert(cce.NonNullElements(d));
- if (d.TryGetValue(boogieVar, out res)) {
- Contract.Assert(res != null);
- return res;
- }
+ if (d.TryGetValue(boogieVar, out res)) {
+ Contract.Assert(res != null);
+ return res;
+ }
}
return null;
}
@@ -288,7 +288,7 @@ namespace Microsoft.Boogie.VCExprAST {
///////////////////////////////////////////////////////////////////////////////////
public override LiteralExpr VisitLiteralExpr(LiteralExpr node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<LiteralExpr>() != null);
Push(TranslateLiteralExpr(node));
return node;
@@ -317,7 +317,7 @@ namespace Microsoft.Boogie.VCExprAST {
///////////////////////////////////////////////////////////////////////////////////
public override AIVariableExpr VisitAIVariableExpr(AIVariableExpr node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<AIVariableExpr>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
@@ -326,7 +326,7 @@ namespace Microsoft.Boogie.VCExprAST {
///////////////////////////////////////////////////////////////////////////////////
public override Expr VisitIdentifierExpr(IdentifierExpr node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Expr>() != null);
Contract.Assume(node.Decl != null); // the expression has to be resolved
Push(LookupVariable(node.Decl));
@@ -340,7 +340,7 @@ namespace Microsoft.Boogie.VCExprAST {
// causes it to become "x0". So we just remove old expressions with a visitor
// before transforming it into a VCExpr.
public override Expr VisitOldExpr(OldExpr node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Expr>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
@@ -349,7 +349,7 @@ namespace Microsoft.Boogie.VCExprAST {
///////////////////////////////////////////////////////////////////////////////////
public override Expr VisitNAryExpr(NAryExpr node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Expr>() != null);
Push(TranslateNAryExpr(node));
return node;
@@ -399,21 +399,21 @@ namespace Microsoft.Boogie.VCExprAST {
///////////////////////////////////////////////////////////////////////////////////
public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<QuantifierExpr>() != null);
Push(TranslateQuantifierExpr(node));
return node;
}
public override ExistsExpr VisitExistsExpr(ExistsExpr node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<ExistsExpr>() != null);
node = (ExistsExpr)this.VisitQuantifierExpr(node);
return node;
}
public override ForallExpr VisitForallExpr(ForallExpr node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<ForallExpr>() != null);
node = (ForallExpr)this.VisitQuantifierExpr(node);
return node;
@@ -509,32 +509,32 @@ namespace Microsoft.Boogie.VCExprAST {
///////////////////////////////////////////////////////////////////////////////////
public override BvExtractExpr VisitBvExtractExpr(BvExtractExpr node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<BvExtractExpr>() != null);
Push(TranslateBvExtractExpr(node));
return node;
}
- private VCExpr TranslateBvExtractExpr(BvExtractExpr node){
-Contract.Requires(node != null);
-Contract.Requires((node.Start <= node.End));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
-VCExpr/*!*/ bv = Translate(node.Bitvector);
- return Gen.BvExtract(bv,cce.NonNull(node.Bitvector.Type).BvBits, node.Start, node.End);
+ private VCExpr TranslateBvExtractExpr(BvExtractExpr node) {
+ Contract.Requires(node != null);
+ Contract.Requires((node.Start <= node.End));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ VCExpr/*!*/ bv = Translate(node.Bitvector);
+ return Gen.BvExtract(bv, cce.NonNull(node.Bitvector.Type).BvBits, node.Start, node.End);
}
///////////////////////////////////////////////////////////////////////////////////
public override BvConcatExpr VisitBvConcatExpr(BvConcatExpr node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<BvConcatExpr>() != null);
Push(TranslateBvConcatExpr(node));
return node;
}
- private VCExpr TranslateBvConcatExpr(BvConcatExpr node){
-Contract.Requires(node != null);
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ private VCExpr TranslateBvConcatExpr(BvConcatExpr node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
VCExpr/*!*/ bv0 = Translate(node.E0);
VCExpr/*!*/ bv1 = Translate(node.E1);
return Gen.BvConcat(bv0, bv1);
@@ -544,60 +544,59 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
// all the other cases should never happen
public override Cmd VisitAssertCmd(AssertCmd node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Cmd>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Cmd VisitAssignCmd(AssignCmd node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Cmd>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Cmd VisitAssumeCmd(AssumeCmd node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Cmd>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override AtomicRE VisitAtomicRE(AtomicRE node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<AtomicRE>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Axiom VisitAxiom(Axiom node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Axiom>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Type VisitBasicType(BasicType node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Type>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Type VisitBvType(BvType node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Type>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Block VisitBlock(Block node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Block>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
CodeExprConverter codeExprConverter = null;
- public void SetCodeExprConverter(CodeExprConverter f){
+ public void SetCodeExprConverter(CodeExprConverter f) {
this.codeExprConverter = f;
}
- public override Expr/*!*/ VisitCodeExpr(CodeExpr/*!*/ codeExpr)
- {
- Contract.Requires(codeExpr != null);
+ public override Expr/*!*/ VisitCodeExpr(CodeExpr/*!*/ codeExpr) {
+ //Contract.Requires(codeExpr != null);
Contract.Ensures(Contract.Result<Expr>() != null);
Contract.Assume(codeExprConverter != null);
@@ -609,271 +608,271 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
return codeExpr;
}
public override BlockSeq VisitBlockSeq(BlockSeq blockSeq) {
- Contract.Requires(blockSeq != null);
+ //Contract.Requires(blockSeq != null);
Contract.Ensures(Contract.Result<BlockSeq>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override List<Block/*!*/>/*!*/ VisitBlockList(List<Block/*!*/>/*!*/ blocks) {
- Contract.Requires(cce.NonNullElements(blocks));
+ //Contract.Requires(cce.NonNullElements(blocks));
Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override BoundVariable VisitBoundVariable(BoundVariable node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<BoundVariable>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Cmd VisitCallCmd(CallCmd node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Cmd>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Cmd VisitCallForallCmd(CallForallCmd node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Cmd>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {
- Contract.Requires(cmdSeq != null);
+ //Contract.Requires(cmdSeq != null);
Contract.Ensures(Contract.Result<CmdSeq>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Choice VisitChoice(Choice node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Choice>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Cmd VisitCommentCmd(CommentCmd node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Cmd>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Constant VisitConstant(Constant node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Constant>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override CtorType VisitCtorType(CtorType node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<CtorType>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Declaration VisitDeclaration(Declaration node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Declaration>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override List<Declaration/*!*/>/*!*/ VisitDeclarationList(List<Declaration/*!*/>/*!*/ declarationList) {
- Contract.Requires(cce.NonNullElements(declarationList));
+ //Contract.Requires(cce.NonNullElements(declarationList));
Contract.Ensures(cce.NonNullElements(Contract.Result<List<Declaration>>()));
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override DeclWithFormals VisitDeclWithFormals(DeclWithFormals node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<DeclWithFormals>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Requires VisitRequires(Requires @requires) {
- Contract.Requires(@requires != null);
+ //Contract.Requires(@requires != null);
Contract.Ensures(Contract.Result<Requires>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override RequiresSeq VisitRequiresSeq(RequiresSeq requiresSeq) {
- Contract.Requires(requiresSeq != null);
+ //Contract.Requires(requiresSeq != null);
Contract.Ensures(Contract.Result<RequiresSeq>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Ensures VisitEnsures(Ensures @ensures) {
- Contract.Requires(@ensures != null);
+ //Contract.Requires(@ensures != null);
Contract.Ensures(Contract.Result<Ensures>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override EnsuresSeq VisitEnsuresSeq(EnsuresSeq ensuresSeq) {
- Contract.Requires(ensuresSeq != null);
+ //Contract.Requires(ensuresSeq != null);
Contract.Ensures(Contract.Result<EnsuresSeq>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Formal VisitFormal(Formal node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Formal>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Function VisitFunction(Function node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Function>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override GlobalVariable VisitGlobalVariable(GlobalVariable node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<GlobalVariable>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override GotoCmd VisitGotoCmd(GotoCmd node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<GotoCmd>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Cmd VisitHavocCmd(HavocCmd node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Cmd>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Implementation VisitImplementation(Implementation node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Implementation>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override LocalVariable VisitLocalVariable(LocalVariable node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<LocalVariable>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override AssignLhs VisitMapAssignLhs(MapAssignLhs node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<AssignLhs>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override MapType VisitMapType(MapType node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<MapType>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Procedure VisitProcedure(Procedure node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Procedure>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Program VisitProgram(Program node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Program>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Cmd VisitRE(RE node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Cmd>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override RESeq VisitRESeq(RESeq reSeq) {
- Contract.Requires(reSeq != null);
+ //Contract.Requires(reSeq != null);
Contract.Ensures(Contract.Result<RESeq>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override ReturnCmd VisitReturnCmd(ReturnCmd node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<ReturnCmd>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override ReturnExprCmd VisitReturnExprCmd(ReturnExprCmd node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<ReturnExprCmd>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Sequential VisitSequential(Sequential node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Sequential>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<AssignLhs>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Cmd VisitStateCmd(StateCmd node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Cmd>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override TransferCmd VisitTransferCmd(TransferCmd node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<TransferCmd>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Trigger VisitTrigger(Trigger node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Trigger>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Type VisitType(Type node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Type>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override TypedIdent VisitTypedIdent(TypedIdent node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<TypedIdent>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Type VisitTypeSynonymAnnotation(TypeSynonymAnnotation node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Type>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Type VisitTypeVariable(TypeVariable node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Type>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Variable VisitVariable(Variable node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Variable>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override VariableSeq VisitVariableSeq(VariableSeq variableSeq) {
- Contract.Requires(variableSeq != null);
+ //Contract.Requires(variableSeq != null);
Contract.Ensures(Contract.Result<VariableSeq>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Cmd>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Cmd>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
@@ -924,13 +923,13 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
}
- public VCExpr Translate(IAppliable app, Type ty, List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs){
-Contract.Requires(ty != null);
-Contract.Requires(app != null);
-Contract.Requires(cce.NonNullElements(typeArgs));
-Contract.Requires(cce.NonNullElements(args));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
-
+ public VCExpr Translate(IAppliable app, Type ty, List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs) {
+ Contract.Requires(ty != null);
+ Contract.Requires(app != null);
+ Contract.Requires(cce.NonNullElements(typeArgs));
+ Contract.Requires(cce.NonNullElements(args));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
List<VCExpr/*!*/>/*!*/ oldArgs = this.args;
List<Type/*!*/>/*!*/ oldTypeArgs = this.typeArgs;
this.args = args;
@@ -946,45 +945,45 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
public VCExpr Visit(UnaryOperator unaryOperator) {
- Contract.Requires(unaryOperator != null);
+ //Contract.Requires(unaryOperator != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
Contract.Assert(unaryOperator.Op == UnaryOperator.Opcode.Not && this.args.Count == 1);
return Gen.Not(this.args);
}
public VCExpr Visit(BinaryOperator binaryOperator) {
- Contract.Requires(binaryOperator != null);
+ //Contract.Requires(binaryOperator != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
return TranslateBinaryOperator(binaryOperator, this.args);
}
public VCExpr Visit(FunctionCall functionCall) {
- Contract.Requires(functionCall != null);
+ //Contract.Requires(functionCall != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
return TranslateFunctionCall(functionCall, this.args, this.typeArgs);
}
public VCExpr Visit(MapSelect mapSelect) {
- Contract.Requires(mapSelect != null);
+ //Contract.Requires(mapSelect != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
return Gen.Select(this.args, this.typeArgs);
}
public VCExpr Visit(MapStore mapStore) {
- Contract.Requires(mapStore != null);
+ //Contract.Requires(mapStore != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
return Gen.Store(this.args, this.typeArgs);
}
public VCExpr Visit(TypeCoercion typeCoercion) {
- Contract.Requires(typeCoercion != null);
+ //Contract.Requires(typeCoercion != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
Contract.Assert(this.args.Count == 1);
return this.args[0];
}
public VCExpr Visit(IfThenElse ite) {
- Contract.Requires(ite != null);
+ //Contract.Requires(ite != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
return Gen.Function(VCExpressionGenerator.IfThenElseOp, this.args);
}
@@ -1038,12 +1037,12 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
///////////////////////////////////////////////////////////////////////////////
- private VCExpr/*!*/ TranslateFunctionCall(FunctionCall app, List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs){
+ private VCExpr/*!*/ TranslateFunctionCall(FunctionCall app, List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs) {
Contract.Requires(cce.NonNullElements(args));
Contract.Requires(cce.NonNullElements(typeArgs));
-Contract.Requires(app != null);
+ Contract.Requires(app != null);
Contract.Requires((app.Func != null));
-Contract.Ensures(Contract.Result<VCExpr>() != null); // resolution must have happened
+ Contract.Ensures(Contract.Result<VCExpr>() != null); // resolution must have happened
VCExpr res = ApplyExpansion(app, args, typeArgs);
if (res != null)
@@ -1053,8 +1052,8 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); // resolution must have
return Gen.Function(functionOp, args, typeArgs);
}
- private VCExpr ApplyExpansion(FunctionCall app, List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs){
-Contract.Requires(app != null);
+ private VCExpr ApplyExpansion(FunctionCall app, List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs) {
+ Contract.Requires(app != null);
Contract.Requires(cce.NonNullElements(args));
Contract.Requires(cce.NonNullElements(typeArgs));
Contract.Assert(app.Func != null); // resolution must have happened
diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs
index 693fcf76..45eeda43 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.cs
+++ b/Source/VCExpr/SimplifyLikeLineariser.cs
@@ -14,18 +14,17 @@ using Microsoft.Boogie.VCExprAST;
// a naive method to turn VCExprs into strings that can be fed into Simplify
-namespace Microsoft.Boogie.VCExprAST
-{
+namespace Microsoft.Boogie.VCExprAST {
[ContractClassFor(typeof(LineariserOptions))]
- public abstract class LinOptContracts:LineariserOptions{
- public LinOptContracts() : base(true) {
+ public abstract class LinOptContracts : LineariserOptions {
+ public LinOptContracts()
+ : base(true) {
}
- public override LineariserOptions SetAsTerm(bool newVal)
-{
- Contract.Ensures(Contract.Result<LineariserOptions>() != null);
- throw new NotImplementedException();
-}
-
+ public override LineariserOptions SetAsTerm(bool newVal) {
+ Contract.Ensures(Contract.Result<LineariserOptions>() != null);
+ throw new NotImplementedException();
+ }
+
}
// Options for the linearisation. Here one can choose, for instance,
@@ -36,52 +35,72 @@ namespace Microsoft.Boogie.VCExprAST
public readonly bool AsTerm;
public abstract LineariserOptions/*!*/ SetAsTerm(bool newVal);
- public abstract bool QuantifierIds { get; }
+ public abstract bool QuantifierIds {
+ get;
+ }
- public virtual bool UseWeights { get { return false; } }
+ public virtual bool UseWeights {
+ get {
+ return false;
+ }
+ }
- public virtual bool InverseImplies { get { return false; } }
+ public virtual bool InverseImplies {
+ get {
+ return false;
+ }
+ }
// whether to include type specifications in quantifiers
- public abstract bool UseTypes { get; }
+ public abstract bool UseTypes {
+ get;
+ }
- public virtual CommandLineOptions.BvHandling Bitvectors { get {
- return CommandLineOptions.BvHandling.None;
- } }
+ public virtual CommandLineOptions.BvHandling Bitvectors {
+ get {
+ return CommandLineOptions.BvHandling.None;
+ }
+ }
// variables representing formulas in let-bindings have to be
// printed in a different way than other variables
- public virtual List<VCExprVar/*!*/>/*!*/ LetVariables { get {Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
- return EmptyList;
- } }
+ public virtual List<VCExprVar/*!*/>/*!*/ LetVariables {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
+ return EmptyList;
+ }
+ }
- public virtual LineariserOptions AddLetVariable(VCExprVar furtherVar){
-Contract.Requires(furtherVar != null);
-Contract.Ensures(Contract.Result<LineariserOptions>() != null);
+ public virtual LineariserOptions AddLetVariable(VCExprVar furtherVar) {
+ Contract.Requires(furtherVar != null);
+ Contract.Ensures(Contract.Result<LineariserOptions>() != null);
return this;
}
- public virtual LineariserOptions AddLetVariables(List<VCExprVar/*!*/>/*!*/ furtherVars){
-Contract.Requires(cce.NonNullElements(furtherVars));
-Contract.Ensures(Contract.Result<LineariserOptions>() != null);
+ public virtual LineariserOptions AddLetVariables(List<VCExprVar/*!*/>/*!*/ furtherVars) {
+ Contract.Requires(cce.NonNullElements(furtherVars));
+ Contract.Ensures(Contract.Result<LineariserOptions>() != null);
return this;
}
-
+
private static readonly List<VCExprVar/*!*/>/*!*/ EmptyList = new List<VCExprVar/*!*/>();
[ContractInvariantMethod]
-void ObjectInvarinat()
-{
- Contract.Invariant(EmptyList!=null);
-}
+ void ObjectInvarinat() {
+ Contract.Invariant(EmptyList != null);
+ }
- public bool NativeBv { get {
- return Bitvectors == CommandLineOptions.BvHandling.Z3Native;
- } }
+ public bool NativeBv {
+ get {
+ return Bitvectors == CommandLineOptions.BvHandling.Z3Native;
+ }
+ }
- public bool IntBv { get {
- return Bitvectors == CommandLineOptions.BvHandling.ToInt;
- } }
+ public bool IntBv {
+ get {
+ return Bitvectors == CommandLineOptions.BvHandling.ToInt;
+ }
+ }
////////////////////////////////////////////////////////////////////////////////////////
@@ -89,23 +108,28 @@ void ObjectInvarinat()
this.AsTerm = asTerm;
}
- public static readonly LineariserOptions SimplifyDefault = new SimplifyOptions (false);
- internal static readonly LineariserOptions SimplifyDefaultTerm = new SimplifyOptions (true);
+ public static readonly LineariserOptions SimplifyDefault = new SimplifyOptions(false);
+ internal static readonly LineariserOptions SimplifyDefaultTerm = new SimplifyOptions(true);
////////////////////////////////////////////////////////////////////////////////////////
private class SimplifyOptions : LineariserOptions {
- internal SimplifyOptions(bool asTerm):base(asTerm) {
-
+ internal SimplifyOptions(bool asTerm)
+ : base(asTerm) {
+
+ }
+ public override bool QuantifierIds {
+ get {
+ return false;
+ }
+ }
+ public override bool UseTypes {
+ get {
+ return false;
+ }
}
- public override bool QuantifierIds { get {
- return false;
- } }
- public override bool UseTypes { get {
- return false;
- } }
public override LineariserOptions SetAsTerm(bool newVal) {
-Contract.Ensures(Contract.Result<LineariserOptions>() != null);
+ Contract.Ensures(Contract.Result<LineariserOptions>() != null);
if (newVal)
return SimplifyDefaultTerm;
else
@@ -119,21 +143,21 @@ Contract.Ensures(Contract.Result<LineariserOptions>() != null);
// Lineariser for expressions. The result (bool) is currently not used for anything
public class SimplifyLikeExprLineariser : IVCExprVisitor<bool, LineariserOptions/*!*/> {
- public static string ToSimplifyString(VCExpr e, UniqueNamer namer){
-Contract.Requires(namer != null);
-Contract.Requires(e != null);
-Contract.Ensures(Contract.Result<string>() != null);
+ public static string ToSimplifyString(VCExpr e, UniqueNamer namer) {
+ Contract.Requires(namer != null);
+ Contract.Requires(e != null);
+ Contract.Ensures(Contract.Result<string>() != null);
return ToString(e, LineariserOptions.SimplifyDefault, namer);
}
- public static string ToString(VCExpr/*!*/ e, LineariserOptions/*!*/ options,UniqueNamer/*!*/ namer) {
+ public static string ToString(VCExpr/*!*/ e, LineariserOptions/*!*/ options, UniqueNamer/*!*/ namer) {
Contract.Requires(e != null);
Contract.Requires(options != null);
Contract.Requires(namer != null);
Contract.Ensures(Contract.Result<string>() != null);
StringWriter sw = new StringWriter();
- SimplifyLikeExprLineariser lin = new SimplifyLikeExprLineariser (sw, namer);
+ SimplifyLikeExprLineariser lin = new SimplifyLikeExprLineariser(sw, namer);
lin.Linearise(e, options);
return sw.ToString();
}
@@ -141,60 +165,62 @@ Contract.Ensures(Contract.Result<string>() != null);
////////////////////////////////////////////////////////////////////////////////////////
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(wr!=null);
+ void ObjectInvariant() {
+ Contract.Invariant(wr != null);
Contract.Invariant(Namer != null);
-}
+ }
private readonly TextWriter/*!*/ wr;
private SimplifyLikeOpLineariser OpLinObject = null;
- private IVCExprOpVisitor<bool, LineariserOptions/*!*/>/*!*/ OpLineariser { get {Contract.Ensures(Contract.Result<IVCExprOpVisitor<bool, LineariserOptions>>()!=null);
- if (OpLinObject == null)
- OpLinObject = new SimplifyLikeOpLineariser (this, wr);
- return OpLinObject;
- } }
+ private IVCExprOpVisitor<bool, LineariserOptions/*!*/>/*!*/ OpLineariser {
+ get {
+ Contract.Ensures(Contract.Result<IVCExprOpVisitor<bool, LineariserOptions>>() != null);
+ if (OpLinObject == null)
+ OpLinObject = new SimplifyLikeOpLineariser(this, wr);
+ return OpLinObject;
+ }
+ }
internal readonly UniqueNamer Namer;
- public SimplifyLikeExprLineariser(TextWriter wr, UniqueNamer namer){
-Contract.Requires(namer != null);
-Contract.Requires(wr != null);
+ public SimplifyLikeExprLineariser(TextWriter wr, UniqueNamer namer) {
+ Contract.Requires(namer != null);
+ Contract.Requires(wr != null);
this.wr = wr;
this.Namer = namer;
}
- public void Linearise(VCExpr expr, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(expr != null);
+ public void Linearise(VCExpr expr, LineariserOptions options) {
+ Contract.Requires(options != null);
+ Contract.Requires(expr != null);
expr.Accept<bool, LineariserOptions>(this, options);
}
- public void LineariseAsTerm(VCExpr expr, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(expr != null);
+ public void LineariseAsTerm(VCExpr expr, LineariserOptions options) {
+ Contract.Requires(options != null);
+ Contract.Requires(expr != null);
Linearise(expr, options.SetAsTerm(true));
}
/////////////////////////////////////////////////////////////////////////////////////
- public static string MakeIdPrintable(string s){
-Contract.Requires(s != null);
-Contract.Ensures(Contract.Result<string>() != null);
+ public static string MakeIdPrintable(string s) {
+ Contract.Requires(s != null);
+ Contract.Ensures(Contract.Result<string>() != null);
// make sure that no keywords are used as identifiers
- switch(s) {
- case andName:
- case orName:
- case notName:
- case impliesName:
- case iffName:
- case eqName:
- case neqName:
- case distinctName:
- case TRUEName:
- case FALSEName:
- s = "nonkeyword_" + s;
- break;
+ switch (s) {
+ case andName:
+ case orName:
+ case notName:
+ case impliesName:
+ case iffName:
+ case eqName:
+ case neqName:
+ case distinctName:
+ case TRUEName:
+ case FALSEName:
+ s = "nonkeyword_" + s;
+ break;
}
if (CommandLineOptions.Clo.BracketIdsInVC == 0) {
@@ -242,29 +268,26 @@ Contract.Ensures(Contract.Result<string>() != null);
}
}
- private static void TypeToStringHelper(Type t, StringBuilder sb)
- {
+ private static void TypeToStringHelper(Type t, StringBuilder sb) {
Contract.Requires(t != null);
TypeSynonymAnnotation syn = t as TypeSynonymAnnotation;
if (syn != null) {
TypeToStringHelper(syn.ExpandedType, sb);
- }
- else {
+ } else {
if (t.IsMap) {
MapType m = t.AsMap;
sb.Append('[');
for (int i = 0; i < m.MapArity; ++i) {
- if (i != 0) sb.Append(',');
+ if (i != 0)
+ sb.Append(',');
TypeToStringHelper(m.Arguments[i], sb);
}
sb.Append(']');
TypeToStringHelper(m.Result, sb);
- }
- else if (t.IsBool || t.IsInt || t.IsBv) {
+ } else if (t.IsBool || t.IsInt || t.IsBv) {
sb.Append(TypeToString(t));
- }
- else {
+ } else {
System.IO.StringWriter buffer = new System.IO.StringWriter();
using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {
t.Emit(stream);
@@ -276,8 +299,7 @@ Contract.Ensures(Contract.Result<string>() != null);
}
- public static string TypeToString(Type t)
- {
+ public static string TypeToString(Type t) {
Contract.Requires(t != null);
Contract.Ensures(Contract.Result<string>() != null);
@@ -294,39 +316,39 @@ Contract.Ensures(Contract.Result<string>() != null);
}
}
- public static string BvConcatOpName(VCExprNAry node){
-Contract.Requires(node != null);
-Contract.Requires((node.Op is VCExprBvConcatOp));
-Contract.Ensures(Contract.Result<string>() != null);
+ public static string BvConcatOpName(VCExprNAry node) {
+ Contract.Requires(node != null);
+ Contract.Requires((node.Op is VCExprBvConcatOp));
+ Contract.Ensures(Contract.Result<string>() != null);
int bits1 = node[0].Type.BvBits;
int bits2 = node[1].Type.BvBits;
return "$bv" + (bits1 + bits2) + "_concat[" + bits1 + "." + bits2 + "]";
}
- public static string BvExtractOpName(VCExprNAry node){
-Contract.Requires(node != null);
-Contract.Requires(node.Op is VCExprBvExtractOp);
-Contract.Ensures(Contract.Result<string>() != null);
+ public static string BvExtractOpName(VCExprNAry node) {
+ Contract.Requires(node != null);
+ Contract.Requires(node.Op is VCExprBvExtractOp);
+ Contract.Ensures(Contract.Result<string>() != null);
VCExprBvExtractOp op = (VCExprBvExtractOp)node.Op;
return "$bv" + node.Type.BvBits + "_extract" + op.Total + "[" + op.Start + ":" + op.End + "]";
}
- public static string StoreOpName(VCExprNAry node){
-Contract.Requires(node != null);
-Contract.Requires((node.Op is VCExprStoreOp));
-Contract.Ensures(Contract.Result<string>() != null);
+ public static string StoreOpName(VCExprNAry node) {
+ Contract.Requires(node != null);
+ Contract.Requires((node.Op is VCExprStoreOp));
+ Contract.Ensures(Contract.Result<string>() != null);
return "Store_" + TypeToString(node[0].Type);
}
- public static string SelectOpName(VCExprNAry node){
-Contract.Requires(node != null);
-Contract.Requires((node.Op is VCExprSelectOp));
-Contract.Ensures(Contract.Result<string>() != null);
+ public static string SelectOpName(VCExprNAry node) {
+ Contract.Requires(node != null);
+ Contract.Requires((node.Op is VCExprSelectOp));
+ Contract.Ensures(Contract.Result<string>() != null);
return "Select_" + TypeToString(node[0].Type);
}
-
- internal void WriteId(string s){
-Contract.Requires(s != null);
+
+ internal void WriteId(string s) {
+ Contract.Requires(s != null);
wr.Write(MakeIdPrintable(s));
}
@@ -343,7 +365,7 @@ Contract.Requires(s != null);
internal const string eqName = "EQ"; // equality
internal const string neqName = "NEQ"; // inequality
internal const string lessName = "<";
- internal const string greaterName = ">";
+ internal const string greaterName = ">";
internal const string atmostName = "<=";
internal const string atleastName = ">=";
internal const string TRUEName = "TRUE"; // nullary predicate that is always true
@@ -373,25 +395,25 @@ Contract.Requires(s != null);
internal const string intDivName = "/";
internal const string intModName = "%";
- internal void AssertAsTerm(string x, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(x != null);
+ internal void AssertAsTerm(string x, LineariserOptions options) {
+ Contract.Requires(options != null);
+ Contract.Requires(x != null);
if (!options.AsTerm)
System.Diagnostics.Debug.Fail("One should never write " + x + " as a formula!");
}
- internal void AssertAsFormula(string x, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(x != null);
+ internal void AssertAsFormula(string x, LineariserOptions options) {
+ Contract.Requires(options != null);
+ Contract.Requires(x != null);
if (options.AsTerm)
System.Diagnostics.Debug.Fail("One should never write " + x + " as a term!");
}
/////////////////////////////////////////////////////////////////////////////////////
- public bool Visit(VCExprLiteral node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool Visit(VCExprLiteral node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
if (options.AsTerm) {
if (node == VCExpressionGenerator.True)
@@ -425,9 +447,9 @@ Contract.Requires(node != null);
/////////////////////////////////////////////////////////////////////////////////////
- public bool Visit(VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool Visit(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
VCExprOp op = node.Op;
Contract.Assert(op != null);
@@ -438,11 +460,11 @@ Contract.Requires(node != null);
wr.Write("({0}",
op.Equals(VCExpressionGenerator.AndOp) ? andName : orName);
- IEnumerator enumerator = new VCExprNAryUniformOpEnumerator (node);
+ IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);
Contract.Assert(enumerator != null);
while (enumerator.MoveNext()) {
VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
- if (naryExpr == null || !naryExpr.Op.Equals(op)) {
+ if (naryExpr == null || !naryExpr.Op.Equals(op)) {
wr.Write(" ");
Linearise(cce.NonNull((VCExpr)enumerator.Current), options);
}
@@ -458,24 +480,24 @@ Contract.Requires(node != null);
/////////////////////////////////////////////////////////////////////////////////////
- public bool Visit(VCExprVar node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool Visit(VCExprVar node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
string printedName = Namer.GetName(node, node.Name);
Contract.Assert(printedName != null);
if (options.AsTerm ||
- // variables for formulas bound in a let-binding are never
- // written as an equation
+ // variables for formulas bound in a let-binding are never
+ // written as an equation
options.LetVariables.Contains(node) ||
- // if variables are properly typed, they cannot be written as
- // equation either
+ // if variables are properly typed, they cannot be written as
+ // equation either
options.UseTypes) {
WriteId(printedName);
} else {
wr.Write("({0} ", eqName);
WriteId(printedName);
- wr.Write(" {0})", boolTrueName);
+ wr.Write(" {0})", boolTrueName);
}
return true;
@@ -483,71 +505,71 @@ Contract.Requires(node != null);
/////////////////////////////////////////////////////////////////////////////////////
- public bool Visit(VCExprQuantifier node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool Visit(VCExprQuantifier node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
AssertAsFormula(node.Quan.ToString(), options);
Contract.Assert(node.TypeParameters.Count == 0);
- Namer.PushScope(); try {
+ Namer.PushScope();
+ try {
- string kind = node.Quan == Quantifier.ALL ? "FORALL" : "EXISTS";
- wr.Write("({0} (", kind);
+ string kind = node.Quan == Quantifier.ALL ? "FORALL" : "EXISTS";
+ wr.Write("({0} (", kind);
- for (int i = 0; i < node.BoundVars.Count; i++)
- {
+ for (int i = 0; i < node.BoundVars.Count; i++) {
VCExprVar var = node.BoundVars[i];
- Contract.Assert(var != null);
+ Contract.Assert(var != null);
string printedName = Namer.GetLocalName(var, var.Name);
- Contract.Assert(printedName != null);
+ Contract.Assert(printedName != null);
if (i != 0)
wr.Write(" ");
WriteId(printedName);
if (options.UseTypes)
wr.Write(" :TYPE {0}", TypeToString(var.Type));
}
- wr.Write(") ");
-
- WriteTriggers(node.Triggers, options);
-
- if (options.QuantifierIds) {
- // only needed for Z3
- VCQuantifierInfos infos = node.Infos;
- Contract.Assert(infos != null);
- if (infos.qid != null) {
- wr.Write("(QID ");
- wr.Write(infos.qid);
- wr.Write(") ");
- }
- if (0 <= infos.uniqueId) {
- wr.Write("(SKOLEMID ");
- wr.Write(infos.uniqueId);
- wr.Write(") ");
+ wr.Write(") ");
+
+ WriteTriggers(node.Triggers, options);
+
+ if (options.QuantifierIds) {
+ // only needed for Z3
+ VCQuantifierInfos infos = node.Infos;
+ Contract.Assert(infos != null);
+ if (infos.qid != null) {
+ wr.Write("(QID ");
+ wr.Write(infos.qid);
+ wr.Write(") ");
+ }
+ if (0 <= infos.uniqueId) {
+ wr.Write("(SKOLEMID ");
+ wr.Write(infos.uniqueId);
+ wr.Write(") ");
+ }
}
- }
- if (options.UseWeights) {
- int weight = QKeyValue.FindIntAttribute(node.Infos.attributes, "weight", 1);
- if (weight != 1) {
- wr.Write("(WEIGHT ");
- wr.Write(weight);
- wr.Write(") ");
+ if (options.UseWeights) {
+ int weight = QKeyValue.FindIntAttribute(node.Infos.attributes, "weight", 1);
+ if (weight != 1) {
+ wr.Write("(WEIGHT ");
+ wr.Write(weight);
+ wr.Write(") ");
+ }
}
- }
- Linearise(node.Body, options);
- wr.Write(")");
+ Linearise(node.Body, options);
+ wr.Write(")");
- return true;
+ return true;
} finally {
Namer.PopScope();
}
}
- private void WriteTriggers(List<VCTrigger/*!*/>/*!*/ triggers, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(cce.NonNullElements(triggers));
+ private void WriteTriggers(List<VCTrigger/*!*/>/*!*/ triggers, LineariserOptions options) {
+ Contract.Requires(options != null);
+ Contract.Requires(cce.NonNullElements(triggers));
// first, count how many neg/pos triggers there are
int negTriggers = 0;
int posTriggers = 0;
@@ -568,7 +590,8 @@ Contract.Requires(cce.NonNullElements(triggers));
if (vcTrig.Exprs.Count > 1) {
wr.Write(" (MPAT");
}
- foreach (VCExpr e in vcTrig.Exprs) {Contract.Assert(e != null);
+ foreach (VCExpr e in vcTrig.Exprs) {
+ Contract.Assert(e != null);
wr.Write(" ");
LineariseAsTerm(e, options);
}
@@ -598,37 +621,39 @@ Contract.Requires(cce.NonNullElements(triggers));
/////////////////////////////////////////////////////////////////////////////////////
- public bool Visit(VCExprLet node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
- Namer.PushScope(); try {
+ public bool Visit(VCExprLet node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ Namer.PushScope();
+ try {
- wr.Write("(LET (");
+ wr.Write("(LET (");
- LineariserOptions optionsWithVars = options.AddLetVariables(node.BoundVars);
+ LineariserOptions optionsWithVars = options.AddLetVariables(node.BoundVars);
Contract.Assert(optionsWithVars != null);
-
- string s = "(";
- foreach (VCExprLetBinding b in node) {Contract.Assert(b != null);
- wr.Write(s);
- string printedName = Namer.GetLocalName(b.V, b.V.Name);
-
- bool formula = b.V.Type.IsBool;
- if (formula)
- wr.Write("FORMULA ");
- else
- wr.Write("TERM ");
- WriteId(printedName);
- wr.Write(" ");
- Linearise(b.E, optionsWithVars.SetAsTerm(!formula));
+
+ string s = "(";
+ foreach (VCExprLetBinding b in node) {
+ Contract.Assert(b != null);
+ wr.Write(s);
+ string printedName = Namer.GetLocalName(b.V, b.V.Name);
+
+ bool formula = b.V.Type.IsBool;
+ if (formula)
+ wr.Write("FORMULA ");
+ else
+ wr.Write("TERM ");
+ WriteId(printedName);
+ wr.Write(" ");
+ Linearise(b.E, optionsWithVars.SetAsTerm(!formula));
+ wr.Write(")");
+ s = " (";
+ }
+ wr.Write(") ");
+ Linearise(node.Body, optionsWithVars);
wr.Write(")");
- s = " (";
- }
- wr.Write(") ");
- Linearise(node.Body, optionsWithVars);
- wr.Write(")");
- return true;
+ return true;
} finally {
Namer.PopScope();
@@ -648,50 +673,50 @@ Contract.Requires(node != null);
private readonly SimplifyLikeExprLineariser/*!*/ ExprLineariser;
private readonly TextWriter/*!*/ wr;
- public SimplifyLikeOpLineariser(SimplifyLikeExprLineariser ExprLineariser, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(ExprLineariser != null);
+ public SimplifyLikeOpLineariser(SimplifyLikeExprLineariser ExprLineariser, TextWriter wr) {
+ Contract.Requires(wr != null);
+ Contract.Requires(ExprLineariser != null);
this.ExprLineariser = ExprLineariser;
this.wr = wr;
}
///////////////////////////////////////////////////////////////////////////////////
- private void WriteApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options, bool argsAsTerms){
-Contract.Requires(options != null);
-Contract.Requires(op != null);
-Contract.Requires(cce.NonNullElements(args));
+ private void WriteApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options, bool argsAsTerms) {
+ Contract.Requires(options != null);
+ Contract.Requires(op != null);
+ Contract.Requires(cce.NonNullElements(args));
WriteApplication(op, op, args, options, argsAsTerms);
}
- private void WriteApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args,LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(op != null);
-Contract.Requires(cce.NonNullElements(args));
+ private void WriteApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options) {
+ Contract.Requires(options != null);
+ Contract.Requires(op != null);
+ Contract.Requires(cce.NonNullElements(args));
WriteApplication(op, op, args, options, options.AsTerm);
}
- private void WriteTermApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args,LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(op != null);
-Contract.Requires(cce.NonNullElements(args));
+ private void WriteTermApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options) {
+ Contract.Requires(options != null);
+ Contract.Requires(op != null);
+ Contract.Requires(cce.NonNullElements(args));
ExprLineariser.AssertAsTerm(op, options);
WriteApplication(op, op, args, options, options.AsTerm);
}
- private void WriteApplication(string termOp, string predOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(predOp != null);
-Contract.Requires(termOp != null);
-Contract.Requires(cce.NonNullElements(args));
+ private void WriteApplication(string termOp, string predOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options) {
+ Contract.Requires(options != null);
+ Contract.Requires(predOp != null);
+ Contract.Requires(termOp != null);
+ Contract.Requires(cce.NonNullElements(args));
WriteApplication(termOp, predOp, args, options, options.AsTerm);
}
- private void WriteApplication(string termOp, string predOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options, bool argsAsTerms){
-Contract.Requires(options != null);
-Contract.Requires(predOp != null);
-Contract.Requires(termOp != null);
-Contract.Requires(cce.NonNullElements(args));// change the AsTerm option for the arguments?
+ private void WriteApplication(string termOp, string predOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options, bool argsAsTerms) {
+ Contract.Requires(options != null);
+ Contract.Requires(predOp != null);
+ Contract.Requires(termOp != null);
+ Contract.Requires(cce.NonNullElements(args));// change the AsTerm option for the arguments?
wr.Write("({0}", options.AsTerm ? termOp : predOp);
LineariserOptions newOptions = options.SetAsTerm(argsAsTerms);
@@ -701,17 +726,17 @@ Contract.Requires(cce.NonNullElements(args));// change the AsTerm option for the
wr.Write(" ");
ExprLineariser.Linearise(e, newOptions);
}
-
+
wr.Write(")");
}
// write an application that can only be a term.
// if the expression is supposed to be printed as a formula,
// it is turned into an equation (EQ (f args) |@true|)
- private void WriteApplicationTermOnly(string termOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(termOp != null);
-Contract.Requires(cce.NonNullElements(args));
+ private void WriteApplicationTermOnly(string termOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options) {
+ Contract.Requires(options != null);
+ Contract.Requires(termOp != null);
+ Contract.Requires(cce.NonNullElements(args));
if (!options.AsTerm)
// Write: (EQ (f args) |@true|)
// where "args" are written as terms
@@ -724,17 +749,17 @@ Contract.Requires(cce.NonNullElements(args));
}
///////////////////////////////////////////////////////////////////////////////////
-
- public bool VisitNotOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+
+ public bool VisitNotOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
WriteApplication(boolNotName, notName, node, options); // arguments can be both terms and formulas
return true;
}
- public bool VisitEqOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitEqOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
if (options.AsTerm) {
// use equality on terms, also if the arguments have type bool
WriteApplication(termEqName, node, options);
@@ -753,9 +778,9 @@ Contract.Requires(node != null);
return true;
}
- public bool VisitNeqOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitNeqOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
if (options.AsTerm) {
// use equality on terms, also if the arguments have type bool
WriteApplication(termNeqName, node, options);
@@ -771,29 +796,29 @@ Contract.Requires(node != null);
WriteApplication(neqName, node, options, true);
}
}
-
+
return true;
}
- public bool VisitAndOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitAndOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
Contract.Assert(options.AsTerm);
WriteApplication(boolAndName, andName, node, options); // arguments can be both terms and formulas
return true;
}
- public bool VisitOrOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitOrOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
Contract.Assert(options.AsTerm);
WriteApplication(boolOrName, orName, node, options); // arguments can be both terms and formulas
return true;
}
- public bool VisitImpliesOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitImpliesOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
if (options.AsTerm) {
wr.Write("({0} ({1} ", boolOrName, boolNotName);
ExprLineariser.Linearise(node[0], options);
@@ -807,16 +832,16 @@ Contract.Requires(node != null);
ExprLineariser.Linearise(node[0], options);
wr.Write("))");
} else {
- WriteApplication(impliesName, node, options);
+ WriteApplication(impliesName, node, options);
}
return true;
}
- public bool VisitDistinctOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitDistinctOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
ExprLineariser.AssertAsFormula(distinctName, options);
-
+
if (node.Length < 2) {
ExprLineariser.Linearise(VCExpressionGenerator.True, options);
} else {
@@ -832,19 +857,20 @@ Contract.Requires(node != null);
return true;
}
- public bool VisitLabelOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitLabelOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
VCExprLabelOp op = (VCExprLabelOp)node.Op;
Contract.Assert(op != null);
wr.Write(String.Format("({0} |{1}| ", op.pos ? "LBLPOS" : "LBLNEG", op.label));
- ExprLineariser.Linearise(node[0], options); wr.Write(")");
+ ExprLineariser.Linearise(node[0], options);
+ wr.Write(")");
return true;
}
- public bool VisitSelectOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitSelectOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
wr.Write("(" + SelectOpName(node));
foreach (VCExpr/*!*/ e in node) {
Contract.Assert(e != null);
@@ -855,9 +881,9 @@ Contract.Requires(node != null);
return true;
}
- public bool VisitStoreOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitStoreOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
wr.Write("(" + StoreOpName(node));
foreach (VCExpr e in node) {
Contract.Assert(e != null);
@@ -868,31 +894,31 @@ Contract.Requires(node != null);
return true;
}
- public bool VisitBvOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitBvOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
WriteTermApplication("$make_bv" + node.Type.BvBits, node, options);
return true;
}
- public bool VisitBvExtractOp(VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitBvExtractOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
WriteTermApplication(BvExtractOpName(node), node, options);
return true;
}
- public bool VisitBvConcatOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitBvConcatOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
WriteTermApplication(BvConcatOpName(node), node, options);
return true;
}
- public bool VisitIfThenElseOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
-
+ public bool VisitIfThenElseOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+
wr.Write("(ITE ");
ExprLineariser.Linearise(node[0], options.SetAsTerm(false));
wr.Write(" ");
@@ -905,8 +931,8 @@ Contract.Requires(node != null);
}
public bool VisitCustomOp(VCExprNAry/*!*/ node, LineariserOptions/*!*/ options) {
- Contract.Requires(node != null);
- Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
VCExprCustomOp op = (VCExprCustomOp)node.Op;
wr.Write("({0}", op.Name);
foreach (VCExpr arg in node) {
@@ -917,9 +943,9 @@ Contract.Requires(node != null);
return true;
}
- public bool VisitAddOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitAddOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
if (CommandLineOptions.Clo.ReflectAdd) {
WriteTermApplication(intAddNameReflect, node, options);
} else {
@@ -928,79 +954,79 @@ Contract.Requires(node != null);
return true;
}
- public bool VisitSubOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitSubOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
WriteTermApplication(intSubName, node, options);
return true;
}
- public bool VisitMulOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitMulOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
WriteTermApplication(intMulName, node, options);
return true;
}
- public bool VisitDivOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitDivOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
WriteTermApplication(intDivName, node, options);
return true;
}
- public bool VisitModOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitModOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
WriteTermApplication(intModName, node, options);
return true;
}
- public bool VisitLtOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitLtOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
WriteApplication(termLessName, lessName, node, options, true); // arguments are always terms
return true;
}
- public bool VisitLeOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitLeOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
WriteApplication(termAtmostName, atmostName, node, options, true); // arguments are always terms
return true;
}
- public bool VisitGtOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitGtOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
WriteApplication(termGreaterName, greaterName, node, options, true); // arguments are always terms
return true;
}
- public bool VisitGeOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitGeOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
WriteApplication(termAtleastName, atleastName, node, options, true); // arguments are always terms
return true;
}
- public bool VisitSubtypeOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitSubtypeOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
WriteApplication(subtypeName, node, options, true); // arguments are always terms
return true;
}
- public bool VisitSubtype3Op (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitSubtype3Op(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
WriteApplication(subtypeArgsName, node, options, true); // arguments are always terms
return true;
}
- public bool VisitBoogieFunctionOp (VCExprNAry node, LineariserOptions options){
-Contract.Requires(options != null);
-Contract.Requires(node != null);
+ public bool VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op;
Contract.Assert(op != null);
string funcName = op.Func.Name;
@@ -1008,7 +1034,8 @@ Contract.Requires(node != null);
string bvzName = op.Func.FindStringAttribute("external");
string printedName = ExprLineariser.Namer.GetName(op.Func, funcName);
Contract.Assert(printedName != null);
- if (bvzName != null) printedName = bvzName;
+ if (bvzName != null)
+ printedName = bvzName;
if (options.UseTypes) {
// we use term notation for arguments whose type is not bool, and
@@ -1022,7 +1049,7 @@ Contract.Requires(node != null);
wr.Write(" ");
ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));
}
-
+
wr.Write(")");
} else {
// arguments are always terms
@@ -1031,7 +1058,7 @@ Contract.Requires(node != null);
}
return true;
}
-
+
}
}
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 7fc8073a..89c615ad 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -571,17 +571,22 @@ 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){
-Contract.Requires(body != null);Contract.Requires(qid != null);Contract.Requires(cce.NonNullElements(triggers));Contract.Requires(cce.NonNullElements(vars));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
-return Quantify(Quantifier.ALL, new List<TypeVariable/*!*/>(), vars,
- triggers, new VCQuantifierInfos (qid, -1, false, null), body);
- }
- public VCExpr Forall(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCExpr body){
-Contract.Requires(body != null);Contract.Requires(cce.NonNullElements(triggers));Contract.Requires(cce.NonNullElements(vars));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
-return Quantify(Quantifier.ALL, new List<TypeVariable/*!*/>(), vars,
- triggers, new VCQuantifierInfos (null, -1, false, null), body);
+ public VCExpr Forall(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, string qid, 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);
+ return Quantify(Quantifier.ALL, new List<TypeVariable/*!*/>(), vars,
+ triggers, new VCQuantifierInfos(qid, -1, false, null), body);
+ }
+ public VCExpr Forall(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCExpr body) {
+ Contract.Requires(body != null);
+ Contract.Requires(cce.NonNullElements(triggers));
+ Contract.Requires(cce.NonNullElements(vars));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return Quantify(Quantifier.ALL, new List<TypeVariable/*!*/>(), vars,
+ triggers, new VCQuantifierInfos(null, -1, false, null), body);
}
public VCExpr Forall(VCExprVar var, VCTrigger trigger, VCExpr body) {
Contract.Requires(body != null);
@@ -599,13 +604,13 @@ return Quantify(Quantifier.ALL, new List<TypeVariable/*!*/>(), vars,
Contract.Ensures(Contract.Result<VCExpr>() != null);
return Quantify(Quantifier.EX, typeParams, vars, triggers, infos, body);
}
- public VCExpr Exists(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCExpr body){
-Contract.Requires(body != null);
+ public VCExpr Exists(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCExpr body) {
+ Contract.Requires(body != null);
Contract.Requires(cce.NonNullElements(triggers));
Contract.Requires(cce.NonNullElements(vars));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
- return Quantify(Quantifier.EX, new List<TypeVariable/*!*/> (), vars,
- triggers, new VCQuantifierInfos (null, -1, false, null), body);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return Quantify(Quantifier.EX, new List<TypeVariable/*!*/>(), vars,
+ triggers, new VCQuantifierInfos(null, -1, false, null), body);
}
public VCExpr Exists(VCExprVar var, VCTrigger trigger, VCExpr body) {
Contract.Requires(body != null);
@@ -679,11 +684,11 @@ namespace Microsoft.Boogie.VCExprAST {
return res;
}
- public static TypeSeq ToTypeSeq(VCExpr[] exprs, int startIndex){
-Contract.Requires(exprs != null);
-Contract.Requires((Contract.ForAll(0,exprs.Length, i=> exprs[i] != null)));
-Contract.Ensures(Contract.Result<TypeSeq>() != null);
-TypeSeq/*!*/ res = new TypeSeq();
+ public static TypeSeq ToTypeSeq(VCExpr[] exprs, int startIndex) {
+ Contract.Requires(exprs != null);
+ Contract.Requires((Contract.ForAll(0, exprs.Length, i => exprs[i] != null)));
+ Contract.Ensures(Contract.Result<TypeSeq>() != null);
+ TypeSeq/*!*/ res = new TypeSeq();
for (int i = startIndex; i < exprs.Length; ++i)
res.Add(cce.NonNull(exprs[i]).Type);
return res;
@@ -760,14 +765,15 @@ TypeSeq/*!*/ res = new TypeSeq();
this.LitType = type;
}
public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {
- Contract.Requires(visitor != null);
+ //Contract.Requires(visitor != null);
return visitor.Visit(this, arg);
}
}
public class VCExprIntLit : VCExprLiteral {
public readonly BigNum Val;
- internal VCExprIntLit(BigNum val) :base(Type.Int){
+ internal VCExprIntLit(BigNum val)
+ : base(Type.Int) {
this.Val = val;
}
[Pure]
@@ -899,7 +905,7 @@ TypeSeq/*!*/ res = new TypeSeq();
this.Op = op;
}
public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {
- Contract.Requires(visitor != null);
+ //Contract.Requires(visitor != null);
return visitor.Visit(this, arg);
}
public Result Accept<Result, Arg>(IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
@@ -944,7 +950,8 @@ TypeSeq/*!*/ res = new TypeSeq();
}
}
- internal VCExprNullary(VCExprOp op):base(op) {
+ internal VCExprNullary(VCExprOp op)
+ : base(op) {
Contract.Requires(op != null);
Contract.Requires(op.Arity == 0 && op.TypeParamArity == 0);
this.ExprType = op.InferType(EMPTY_VCEXPR_LIST, EMPTY_TYPE_LIST);
@@ -984,21 +991,23 @@ TypeSeq/*!*/ res = new TypeSeq();
}
}
- internal VCExprUnary(VCExprOp op, List<VCExpr> arguments) :base(op){
+ internal VCExprUnary(VCExprOp op, List<VCExpr> arguments)
+ : base(op) {
Contract.Requires(op != null);
Contract.Requires(cce.NonNullElements(arguments));
Contract.Requires(op.Arity == 1 && op.TypeParamArity == 0 && arguments.Count == 1);
-
+
this.Argument = arguments[0];
this.ExprType =
op.InferType(arguments, EMPTY_TYPE_LIST);
}
- internal VCExprUnary(VCExprOp op, VCExpr argument) :base(op){
+ internal VCExprUnary(VCExprOp op, VCExpr argument)
+ : base(op) {
Contract.Requires(argument != null);
Contract.Requires(op != null);
Contract.Requires(op.Arity == 1 && op.TypeParamArity == 0);
-
+
this.Argument = argument;
// PR: could be optimised so that the argument does
// not have to be boxed in an array each time
@@ -1049,17 +1058,19 @@ TypeSeq/*!*/ res = new TypeSeq();
}
}
- internal VCExprBinary(VCExprOp op, List<VCExpr> arguments) :base(op){
+ internal VCExprBinary(VCExprOp op, List<VCExpr> arguments)
+ : base(op) {
Contract.Requires(op != null);
Contract.Requires(cce.NonNullElements(arguments));
Contract.Requires(op.Arity == 2 && op.TypeParamArity == 0 && arguments.Count == 2);
-
+
this.Argument0 = arguments[0];
this.Argument1 = arguments[1];
this.ExprType = op.InferType(arguments, EMPTY_TYPE_LIST);
}
- internal VCExprBinary(VCExprOp op, VCExpr argument0, VCExpr argument1) :base(op){
+ internal VCExprBinary(VCExprOp op, VCExpr argument0, VCExpr argument1)
+ : base(op) {
Contract.Requires(argument1 != null);
Contract.Requires(argument0 != null);
Contract.Requires(op != null);
@@ -1109,7 +1120,8 @@ TypeSeq/*!*/ res = new TypeSeq();
}
}
- internal VCExprMultiAry(VCExprOp op, List<VCExpr> arguments) :base(op){
+ internal VCExprMultiAry(VCExprOp op, List<VCExpr> arguments)
+ : base(op) {
Contract.Requires(op != null);
Contract.Requires(cce.NonNullElements(arguments));
//this(op, arguments, EMPTY_TYPE_LIST);
@@ -1117,7 +1129,8 @@ TypeSeq/*!*/ res = new TypeSeq();
this.TypeArgumentsAttr = EMPTY_TYPE_LIST;
this.ExprType = op.InferType(arguments, TypeArgumentsAttr);
}
- internal VCExprMultiAry(VCExprOp op, List<VCExpr> arguments, List<Type/*!*/>/*!*/ typeArguments):base(op){
+ internal VCExprMultiAry(VCExprOp op, List<VCExpr> arguments, List<Type/*!*/>/*!*/ typeArguments)
+ : base(op) {
Contract.Requires(op != null);
Contract.Requires(cce.NonNullElements(typeArguments));
Contract.Requires(cce.NonNullElements(arguments));
@@ -1227,8 +1240,8 @@ TypeSeq/*!*/ res = new TypeSeq();
}
}
public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
- Contract.Requires(cce.NonNullElements(typeArgs));
- Contract.Requires(cce.NonNullElements(args));
+ //Contract.Requires(cce.NonNullElements(typeArgs));
+ //Contract.Requires(cce.NonNullElements(args));
Contract.Ensures(Contract.Result<Type>() != null);
return OpType;
}
@@ -1241,7 +1254,8 @@ TypeSeq/*!*/ res = new TypeSeq();
}
public class VCExprDistinctOp : VCExprNAryOp {
- internal VCExprDistinctOp(int arity) :base(arity, Type.Bool){
+ internal VCExprDistinctOp(int arity)
+ : base(arity, Type.Bool) {
}
[Pure]
[Reads(ReadsAttribute.Reads.Nothing)]
@@ -1258,8 +1272,8 @@ TypeSeq/*!*/ res = new TypeSeq();
}
public override Result Accept<Result, Arg>
(VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
- Contract.Requires(visitor != null);
- Contract.Requires(expr != null);
+ //Contract.Requires(visitor != null);
+ //Contract.Requires(expr != null);
return visitor.VisitDistinctOp(expr, arg);
}
}
@@ -1276,8 +1290,8 @@ TypeSeq/*!*/ res = new TypeSeq();
}
}
public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
- Contract.Requires(cce.NonNullElements(typeArgs));
- Contract.Requires(cce.NonNullElements(args));
+ //Contract.Requires(cce.NonNullElements(typeArgs));
+ //Contract.Requires(cce.NonNullElements(args));
Contract.Ensures(Contract.Result<Type>() != null);
return args[0].Type;
}
@@ -1312,8 +1326,8 @@ TypeSeq/*!*/ res = new TypeSeq();
}
public override Result Accept<Result, Arg>
(VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
- Contract.Requires(visitor != null);
- Contract.Requires(expr != null);
+ //Contract.Requires(visitor != null);
+ //Contract.Requires(expr != null);
return visitor.VisitLabelOp(expr, arg);
}
}
@@ -1332,10 +1346,10 @@ TypeSeq/*!*/ res = new TypeSeq();
}
}
- public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs){
-Contract.Requires(cce.NonNullElements(typeArgs));
-Contract.Requires(cce.NonNullElements(args));
-Contract.Ensures(Contract.Result<Type>() != null);
+ public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
+ //Contract.Requires(cce.NonNullElements(typeArgs));
+ //Contract.Requires(cce.NonNullElements(args));
+ Contract.Ensures(Contract.Result<Type>() != null);
MapType/*!*/ mapType = args[0].Type.AsMap;
Contract.Assert(TypeParamArity == mapType.TypeParameters.Length);
IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst = new Dictionary<TypeVariable/*!*/, Type/*!*/>();
@@ -1366,8 +1380,8 @@ Contract.Ensures(Contract.Result<Type>() != null);
}
public override Result Accept<Result, Arg>
(VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
- Contract.Requires(visitor != null);
- Contract.Requires(expr != null);
+ //Contract.Requires(visitor != null);
+ //Contract.Requires(expr != null);
return visitor.VisitSelectOp(expr, arg);
}
}
@@ -1389,8 +1403,8 @@ Contract.Ensures(Contract.Result<Type>() != null);
}
public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
- Contract.Requires(cce.NonNullElements(typeArgs));
- Contract.Requires(cce.NonNullElements(args));
+ //Contract.Requires(cce.NonNullElements(typeArgs));
+ //Contract.Requires(cce.NonNullElements(args));
Contract.Ensures(Contract.Result<Type>() != null);
return args[0].Type;
}
@@ -1416,8 +1430,8 @@ Contract.Ensures(Contract.Result<Type>() != null);
}
public override Result Accept<Result, Arg>
(VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
- Contract.Requires(visitor != null);
- Contract.Requires(expr != null);
+ //Contract.Requires(visitor != null);
+ //Contract.Requires(expr != null);
return visitor.VisitStoreOp(expr, arg);
}
}
@@ -1434,8 +1448,8 @@ Contract.Ensures(Contract.Result<Type>() != null);
}
}
public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
- Contract.Requires(cce.NonNullElements(typeArgs));
- Contract.Requires(cce.NonNullElements(args));
+ //Contract.Requires(cce.NonNullElements(typeArgs));
+ //Contract.Requires(cce.NonNullElements(args));
Contract.Ensures(Contract.Result<Type>() != null);
return args[1].Type;
}
@@ -1458,8 +1472,8 @@ Contract.Ensures(Contract.Result<Type>() != null);
}
public override Result Accept<Result, Arg>
(VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
- Contract.Requires(visitor != null);
- Contract.Requires(expr != null);
+ //Contract.Requires(visitor != null);
+ //Contract.Requires(expr != null);
return visitor.VisitIfThenElseOp(expr, arg);
}
}
@@ -1469,11 +1483,10 @@ Contract.Ensures(Contract.Result<Type>() != null);
int arity;
public readonly Type/*!*/ Type;
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(Name!=null);
+ void ObjectInvariant() {
+ Contract.Invariant(Name != null);
Contract.Invariant(Type != null);
-}
+ }
public VCExprCustomOp(string/*!*/ name, int arity, Type/*!*/ type) {
Contract.Requires(name != null);
@@ -1482,7 +1495,8 @@ void ObjectInvariant()
this.arity = arity;
this.Type = type;
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object that) {
if (Object.ReferenceEquals(this, that))
return true;
@@ -1491,15 +1505,26 @@ void ObjectInvariant()
return false;
return this.Name == t.Name && this.arity == t.arity && this.Type == t.Type;
}
- public override int Arity { get { return arity; } }
- public override int TypeParamArity { get { return 0; } }
- public override Type/*!*/ InferType(List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs) {Contract.Requires((cce.NonNullElements(args)));
-Contract.Requires((cce.NonNullElements(typeArgs)));
-Contract.Ensures(Contract.Result<Type>() != null); return Type; }
+ public override int Arity {
+ get {
+ return arity;
+ }
+ }
+ public override int TypeParamArity {
+ get {
+ return 0;
+ }
+ }
+ public override Type/*!*/ InferType(List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs) {
+ //Contract.Requires((cce.NonNullElements(args)));
+ //Contract.Requires((cce.NonNullElements(typeArgs)));
+ Contract.Ensures(Contract.Result<Type>() != null);
+ return Type;
+ }
public override Result Accept<Result, Arg>
(VCExprNAry/*!*/ expr, IVCExprOpVisitor<Result, Arg>/*!*/ visitor, Arg arg) {
- Contract.Requires(expr != null);
- Contract.Requires(visitor != null);
+ //Contract.Requires(expr != null);
+ //Contract.Requires(visitor != null);
return visitor.VisitCustomOp(expr, arg);
}
}
@@ -1521,8 +1546,8 @@ Contract.Ensures(Contract.Result<Type>() != null); return Type; }
}
}
public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
- Contract.Requires(cce.NonNullElements(typeArgs));
- Contract.Requires(cce.NonNullElements(args));
+ //Contract.Requires(cce.NonNullElements(typeArgs));
+ //Contract.Requires(cce.NonNullElements(args));
Contract.Ensures(Contract.Result<Type>() != null);
return Type.GetBvType(Bits);
}
@@ -1546,8 +1571,8 @@ Contract.Ensures(Contract.Result<Type>() != null); return Type; }
}
public override Result Accept<Result, Arg>
(VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
- Contract.Requires(visitor != null);
- Contract.Requires(expr != null);
+ //Contract.Requires(visitor != null);
+ //Contract.Requires(expr != null);
return visitor.VisitBvOp(expr, arg);
}
}
@@ -1568,8 +1593,8 @@ Contract.Ensures(Contract.Result<Type>() != null); return Type; }
}
}
public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
- Contract.Requires(cce.NonNullElements(typeArgs));
- Contract.Requires(cce.NonNullElements(args));
+ //Contract.Requires(cce.NonNullElements(typeArgs));
+ //Contract.Requires(cce.NonNullElements(args));
Contract.Ensures(Contract.Result<Type>() != null);
return Type.GetBvType(End - Start);
}
@@ -1598,8 +1623,8 @@ Contract.Ensures(Contract.Result<Type>() != null); return Type; }
}
public override Result Accept<Result, Arg>
(VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
- Contract.Requires(visitor != null);
- Contract.Requires(expr != null);
+ //Contract.Requires(visitor != null);
+ //Contract.Requires(expr != null);
return visitor.VisitBvExtractOp(expr, arg);
}
}
@@ -1619,8 +1644,8 @@ Contract.Ensures(Contract.Result<Type>() != null); return Type; }
}
}
public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
- Contract.Requires(cce.NonNullElements(typeArgs));
- Contract.Requires(cce.NonNullElements(args));
+ //Contract.Requires(cce.NonNullElements(typeArgs));
+ //Contract.Requires(cce.NonNullElements(args));
Contract.Ensures(Contract.Result<Type>() != null);
return Type.GetBvType(args[0].Type.BvBits + args[1].Type.BvBits);
}
@@ -1648,8 +1673,8 @@ Contract.Ensures(Contract.Result<Type>() != null); return Type; }
}
public override Result Accept<Result, Arg>
(VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
- Contract.Requires(visitor != null);
- Contract.Requires(expr != null);
+ //Contract.Requires(visitor != null);
+ //Contract.Requires(expr != null);
return visitor.VisitBvConcatOp(expr, arg);
}
}
@@ -1675,10 +1700,10 @@ Contract.Ensures(Contract.Result<Type>() != null); return Type; }
return Func.TypeParameters.Length;
}
}
- public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs){
-Contract.Requires(cce.NonNullElements(typeArgs));
-Contract.Requires(cce.NonNullElements(args));
-Contract.Ensures(Contract.Result<Type>() != null);
+ public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
+ //Contract.Requires(cce.NonNullElements(typeArgs));
+ //Contract.Requires(cce.NonNullElements(args));
+ Contract.Ensures(Contract.Result<Type>() != null);
Contract.Assert(TypeParamArity == Func.TypeParameters.Length);
if (TypeParamArity == 0)
return cce.NonNull(Func.OutParams[0]).TypedIdent.Type;
@@ -1710,8 +1735,8 @@ Contract.Ensures(Contract.Result<Type>() != null);
}
public override Result Accept<Result, Arg>
(VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
- Contract.Requires(visitor != null);
- Contract.Requires(expr != null);
+ //Contract.Requires(visitor != null);
+ //Contract.Requires(expr != null);
return visitor.VisitBoogieFunctionOp(expr, arg);
}
}
@@ -1745,7 +1770,7 @@ Contract.Ensures(Contract.Result<Type>() != null);
this.VarType = type;
}
public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {
- Contract.Requires(visitor != null);
+ //Contract.Requires(visitor != null);
return visitor.Visit(this, arg);
}
}
@@ -1870,19 +1895,20 @@ Contract.Ensures(Contract.Result<Type>() != null);
HelperFuns.PolyHash(123, 11, Triggers);
}
- internal VCExprQuantifier(Quantifier kind, List<TypeVariable/*!*/>/*!*/ typeParams, List<VCExprVar/*!*/>/*!*/ boundVars, List<VCTrigger/*!*/>/*!*/ triggers, VCQuantifierInfos infos, VCExpr body) :base(typeParams, boundVars, body){
+ internal VCExprQuantifier(Quantifier kind, List<TypeVariable/*!*/>/*!*/ typeParams, List<VCExprVar/*!*/>/*!*/ boundVars, List<VCTrigger/*!*/>/*!*/ triggers, VCQuantifierInfos infos, VCExpr body)
+ : base(typeParams, boundVars, body) {
Contract.Requires(body != null);
Contract.Requires(infos != null);
Contract.Requires(cce.NonNullElements(triggers));
Contract.Requires(cce.NonNullElements(boundVars));
Contract.Requires(cce.NonNullElements(typeParams));
-
+
this.Quan = kind;
this.Triggers = triggers;
this.Infos = infos;
}
public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {
- Contract.Requires(visitor != null);
+ //Contract.Requires(visitor != null);
return visitor.Visit(this, arg);
}
}
@@ -1978,22 +2004,23 @@ Contract.Ensures(Contract.Result<Type>() != null);
return Bindings.GetEnumerator();
}
- private static List<VCExprVar/*!*/>/*!*/ toSeq(List<VCExprLetBinding/*!*/>/*!*/ bindings){
-Contract.Requires(cce.NonNullElements(bindings));
-Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
- List<VCExprVar> res = new List<VCExprVar> ();
+ private static List<VCExprVar/*!*/>/*!*/ toSeq(List<VCExprLetBinding/*!*/>/*!*/ bindings) {
+ Contract.Requires(cce.NonNullElements(bindings));
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
+ List<VCExprVar> res = new List<VCExprVar>();
foreach (VCExprLetBinding/*!*/ b in bindings)
res.Add(b.V);
return res;
}
- internal VCExprLet(List<VCExprLetBinding/*!*/>/*!*/ bindings, VCExpr/*!*/ body) :base(new List<TypeVariable/*!*/>(), toSeq(bindings), body){
+ internal VCExprLet(List<VCExprLetBinding/*!*/>/*!*/ bindings, VCExpr/*!*/ body)
+ : base(new List<TypeVariable/*!*/>(), toSeq(bindings), body) {
Contract.Requires(cce.NonNullElements(bindings));
Contract.Requires(body != null);
this.Bindings = bindings;
}
public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {
- Contract.Requires(visitor != null);
+ //Contract.Requires(visitor != null);
return visitor.Visit(this, arg);
}
}
diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs
index c79c08db..adb3b27e 100644
--- a/Source/VCExpr/VCExprASTPrinter.cs
+++ b/Source/VCExpr/VCExprASTPrinter.cs
@@ -14,50 +14,44 @@ using Microsoft.Basetypes;
// A simple visitor for turning a VCExpr into a human-readable string
// (S-expr syntax)
-namespace Microsoft.Boogie.VCExprAST
-{
+namespace Microsoft.Boogie.VCExprAST {
public class VCExprPrinter : IVCExprVisitor<bool, TextWriter/*!*/> {
private VCExprOpPrinter OpPrinterVar = null;
- private VCExprOpPrinter/*!*/ OpPrinter { get {Contract.Ensures(Contract.Result<VCExprOpPrinter>() != null);
+ private VCExprOpPrinter/*!*/ OpPrinter {
+ get {
+ Contract.Ensures(Contract.Result<VCExprOpPrinter>() != null);
- if (OpPrinterVar == null)
- OpPrinterVar = new VCExprOpPrinter(this);
- return OpPrinterVar;
- } }
+ if (OpPrinterVar == null)
+ OpPrinterVar = new VCExprOpPrinter(this);
+ return OpPrinterVar;
+ }
+ }
- public void Print(VCExpr expr, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(expr != null);
+ public void Print(VCExpr expr, TextWriter wr) {
+ Contract.Requires(wr != null);
+ Contract.Requires(expr != null);
expr.Accept<bool, TextWriter/*!*/>(this, wr);
}
- public bool Visit(VCExprLiteral node, TextWriter wr)
- {
- Contract.Requires(wr != null);
- Contract.Requires(node != null);
- if (node == VCExpressionGenerator.True)
- {
- wr.Write("true");
- }
- else if (node == VCExpressionGenerator.False)
- {
- wr.Write("false");
- }
- else if (node is VCExprIntLit)
- {
- wr.Write(((VCExprIntLit)node).Val);
- }
- else
- {
- Contract.Assert(false); throw new cce.UnreachableException();
- }
- return true;
+ public bool Visit(VCExprLiteral node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ if (node == VCExpressionGenerator.True) {
+ wr.Write("true");
+ } else if (node == VCExpressionGenerator.False) {
+ wr.Write("false");
+ } else if (node is VCExprIntLit) {
+ wr.Write(((VCExprIntLit)node).Val);
+ } else {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
+ return true;
}
- public bool Visit(VCExprNAry node, TextWriter wr)
- {
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool Visit(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
VCExprOp/*!*/ op = node.Op;
Contract.Assert(op != null);
@@ -67,7 +61,7 @@ Contract.Requires(node != null);
wr.Write("({0}",
op.Equals(VCExpressionGenerator.AndOp) ? "And" : "Or");
- IEnumerator/*!*/ enumerator = new VCExprNAryUniformOpEnumerator (node);
+ IEnumerator/*!*/ enumerator = new VCExprNAryUniformOpEnumerator(node);
Contract.Assert(enumerator != null);
while (enumerator.MoveNext()) {
VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
@@ -84,15 +78,15 @@ Contract.Requires(node != null);
return node.Accept<bool, TextWriter/*!*/>(OpPrinter, wr);
}
- public bool Visit(VCExprVar node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool Visit(VCExprVar node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
wr.Write(node.Name);
return true;
}
- public bool Visit(VCExprQuantifier node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool Visit(VCExprQuantifier node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
string/*!*/ quan = node.Quan == Quantifier.ALL ? "Forall" : "Exists";
Contract.Assert(quan != null);
@@ -101,8 +95,8 @@ Contract.Requires(node != null);
if (node.TypeParameters.Count > 0) {
wr.Write("<");
string/*!*/ sep = "";
- foreach(TypeVariable/*!*/ v in node.TypeParameters){
-Contract.Assert(v != null);
+ foreach (TypeVariable/*!*/ v in node.TypeParameters) {
+ Contract.Assert(v != null);
wr.Write(sep);
sep = ", ";
wr.Write("{0}", v.Name);
@@ -112,27 +106,27 @@ Contract.Assert(v != null);
if (node.BoundVars.Count > 0) {
string/*!*/ sep = "";
- foreach(VCExprVar/*!*/ v in node.BoundVars){
-Contract.Assert(v != null);
+ foreach (VCExprVar/*!*/ v in node.BoundVars) {
+ Contract.Assert(v != null);
wr.Write(sep);
sep = ", ";
Print(v, wr);
}
wr.Write(" ");
}
-
+
wr.Write(":: ");
if (node.Triggers.Count > 0) {
wr.Write("{0} ", "{");
string/*!*/ sep = "";
- foreach(VCTrigger/*!*/ t in node.Triggers){
-Contract.Assert(t != null);
+ foreach (VCTrigger/*!*/ t in node.Triggers) {
+ Contract.Assert(t != null);
wr.Write(sep);
sep = ", ";
string/*!*/ sep2 = "";
- foreach(VCExpr/*!*/ e in t.Exprs){
-Contract.Assert(e != null);
+ foreach (VCExpr/*!*/ e in t.Exprs) {
+ Contract.Assert(e != null);
wr.Write(sep2);
sep2 = "+";
Print(e, wr);
@@ -145,14 +139,14 @@ Contract.Assert(e != null);
wr.Write(")");
return true;
}
- public bool Visit(VCExprLet node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool Visit(VCExprLet node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
wr.Write("(Let ");
string/*!*/ sep = "";
- foreach(VCExprLetBinding/*!*/ b in node){
-Contract.Assert(b != null);
+ foreach (VCExprLetBinding/*!*/ b in node) {
+ Contract.Assert(b != null);
wr.Write(sep);
sep = ", ";
Print(b.V, wr);
@@ -175,18 +169,18 @@ Contract.Assert(b != null);
}
- public VCExprOpPrinter(VCExprPrinter exprPrinter){
-Contract.Requires(exprPrinter != null);
+ public VCExprOpPrinter(VCExprPrinter exprPrinter) {
+ Contract.Requires(exprPrinter != null);
this.ExprPrinter = exprPrinter;
}
- private bool PrintNAry(string op, VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
-Contract.Requires(op != null);
+ private bool PrintNAry(string op, VCExprNAry node, TextWriter wr) {
+ Contract.Requires(wr != null);
+ Contract.Requires(node != null);
+ Contract.Requires(op != null);
wr.Write("({0}", op);
- foreach(VCExpr/*!*/ arg in node){
-Contract.Assert(arg != null);
+ foreach (VCExpr/*!*/ arg in node) {
+ Contract.Assert(arg != null);
wr.Write(" ");
ExprPrinter.Print(arg, wr);
}
@@ -194,148 +188,150 @@ Contract.Assert(arg != null);
return true;
}
- public bool VisitNotOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitNotOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry("!", node, wr);
}
- public bool VisitEqOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitEqOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry("==", node, wr);
}
- public bool VisitNeqOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitNeqOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry("!=", node, wr);
}
- public bool VisitAndOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
- Contract.Assert(false); throw new cce.UnreachableException();
- }
- public bool VisitOrOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
- Contract.Assert(false); throw new cce.UnreachableException();
- }
- public bool VisitImpliesOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitAndOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
+ public bool VisitOrOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
+ public bool VisitImpliesOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry("Implies", node, wr);
}
- public bool VisitDistinctOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitDistinctOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry("Distinct", node, wr);
}
- public bool VisitLabelOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
-VCExprLabelOp/*!*/ op = (VCExprLabelOp)node.Op;
-Contract.Assert(op != null);
+ public bool VisitLabelOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ VCExprLabelOp/*!*/ op = (VCExprLabelOp)node.Op;
+ Contract.Assert(op != null);
return PrintNAry("Label " + op.label, node, wr);
}
- public bool VisitSelectOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitSelectOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry("Select", node, wr);
}
- public bool VisitStoreOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitStoreOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry("Store", node, wr);
}
- public bool VisitBvOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitBvOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry("Bv", node, wr);
}
- public bool VisitBvExtractOp(VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitBvExtractOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry("BvExtract", node, wr);
}
- public bool VisitBvConcatOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitBvConcatOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry("BvConcat", node, wr);
}
- public bool VisitIfThenElseOp(VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitIfThenElseOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry("if-then-else", node, wr);
}
public bool VisitCustomOp(VCExprNAry/*!*/ node, TextWriter/*!*/ wr) {
- Contract.Requires(node!=null);
- Contract.Requires(wr != null);
+ //Contract.Requires(node!=null);
+ //Contract.Requires(wr != null);
VCExprCustomOp op = (VCExprCustomOp)node.Op;
return PrintNAry(op.Name, node, wr);
}
- public bool VisitAddOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitAddOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
if (CommandLineOptions.Clo.ReflectAdd) {
return PrintNAry("Reflect$Add", node, wr);
} else {
return PrintNAry("+", node, wr);
}
}
- public bool VisitSubOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitSubOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry("-", node, wr);
}
- public bool VisitMulOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitMulOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry("*", node, wr);
}
- public bool VisitDivOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitDivOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry("/", node, wr);
}
- public bool VisitModOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitModOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry("%", node, wr);
}
- public bool VisitLtOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitLtOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry("<", node, wr);
}
- public bool VisitLeOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitLeOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry("<=", node, wr);
}
- public bool VisitGtOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitGtOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry(">", node, wr);
}
- public bool VisitGeOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitGeOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry(">=", node, wr);
}
- public bool VisitSubtypeOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitSubtypeOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry("<:", node, wr);
}
- public bool VisitSubtype3Op (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
+ public bool VisitSubtype3Op(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
return PrintNAry("<::", node, wr);
}
- public bool VisitBoogieFunctionOp (VCExprNAry node, TextWriter wr){
-Contract.Requires(wr != null);
-Contract.Requires(node != null);
-VCExprBoogieFunctionOp/*!*/ op = (VCExprBoogieFunctionOp)node.Op;
-Contract.Assert(op != null);
+ public bool VisitBoogieFunctionOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ VCExprBoogieFunctionOp/*!*/ op = (VCExprBoogieFunctionOp)node.Op;
+ Contract.Assert(op != null);
return PrintNAry(op.Func.Name, node, wr);
}
}
diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index e87b04ce..3e65ec23 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -17,7 +17,7 @@ namespace Microsoft.Boogie.VCExprAST {
using Microsoft.Boogie;
[ContractClass(typeof(IVCExprVisitorContracts<,>))]
- public interface IVCExprVisitor<Result,Arg> {
+ public interface IVCExprVisitor<Result, Arg> {
Result Visit(VCExprLiteral/*!*/ node, Arg arg);
Result Visit(VCExprNAry/*!*/ node, Arg arg);
Result Visit(VCExprVar/*!*/ node, Arg arg);
@@ -25,7 +25,7 @@ namespace Microsoft.Boogie.VCExprAST {
Result Visit(VCExprLet/*!*/ node, Arg arg);
}
[ContractClassFor(typeof(IVCExprVisitor<,>))]
- public abstract class IVCExprVisitorContracts<Result,Arg> : IVCExprVisitor<Result,Arg> {
+ public abstract class IVCExprVisitorContracts<Result, Arg> : IVCExprVisitor<Result, Arg> {
#region IVCExprVisitor Members
public Result Visit(VCExprLiteral node, Arg arg) {
@@ -83,10 +83,10 @@ namespace Microsoft.Boogie.VCExprAST {
Result VisitSubtype3Op(VCExprNAry node, Arg arg);
Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg);
Result VisitIfThenElseOp(VCExprNAry node, Arg arg);
- Result VisitCustomOp (VCExprNAry node, Arg arg);
+ Result VisitCustomOp(VCExprNAry node, Arg arg);
}
[ContractClassFor(typeof(IVCExprOpVisitor<,>))]
- public abstract class IVCExprOpVisitorContracts<Result, Arg>:IVCExprOpVisitor<Result,Arg> {
+ public abstract class IVCExprOpVisitorContracts<Result, Arg> : IVCExprOpVisitor<Result, Arg> {
#region IVCExprOpVisitor<Result,Arg> Members
public Result VisitNotOp(VCExprNAry node, Arg arg) {
@@ -248,23 +248,22 @@ namespace Microsoft.Boogie.VCExprAST {
}
public virtual Result Visit(VCExprLiteral node, Arg arg) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
return StandardResult(node, arg);
}
- public virtual Result Visit(VCExprNAry node, Arg arg){
-Contract.Requires(node != null);
+ public virtual Result Visit(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
Result res = StandardResult(node, arg);
if (node.TypeParamArity == 0 &&
(node.Op == VCExpressionGenerator.AndOp ||
- node.Op == VCExpressionGenerator.OrOp ||
- node.Op == VCExpressionGenerator.ImpliesOp))
- {
+ node.Op == VCExpressionGenerator.OrOp ||
+ node.Op == VCExpressionGenerator.ImpliesOp)) {
Contract.Assert(node.Op != null);
VCExprOp op = node.Op;
-
+
IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);
enumerator.MoveNext(); // skip the node itself
@@ -278,34 +277,40 @@ Contract.Requires(node != null);
}
}
} else {
- foreach (VCExpr e in node){Contract.Assert(e != null);
- e.Accept(this, arg);}
+ foreach (VCExpr e in node) {
+ Contract.Assert(e != null);
+ e.Accept(this, arg);
+ }
}
return res;
}
public virtual Result Visit(VCExprVar node, Arg arg) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
return StandardResult(node, arg);
}
- public virtual Result Visit(VCExprQuantifier node, Arg arg){
-Contract.Requires(node != null);
+ public virtual Result Visit(VCExprQuantifier node, Arg arg) {
+ //Contract.Requires(node != null);
Result res = StandardResult(node, arg);
- foreach (VCTrigger/*!*/ trigger in node.Triggers){Contract.Assert(trigger != null);
- foreach (VCExpr/*!*/ expr in trigger.Exprs) {
- Contract.Assert(expr != null);
- expr.Accept(this, arg);}}
+ foreach (VCTrigger/*!*/ trigger in node.Triggers) {
+ Contract.Assert(trigger != null);
+ foreach (VCExpr/*!*/ expr in trigger.Exprs) {
+ Contract.Assert(expr != null);
+ expr.Accept(this, arg);
+ }
+ }
node.Body.Accept(this, arg);
return res;
}
- public virtual Result Visit(VCExprLet node, Arg arg){
-Contract.Requires(node != null);
+ public virtual Result Visit(VCExprLet node, Arg arg) {
+ //Contract.Requires(node != null);
Result res = StandardResult(node, arg);
// visit the bound expressions first
foreach (VCExprLetBinding/*!*/ binding in node) {
Contract.Assert(binding != null);
- binding.E.Accept(this, arg);}
+ binding.E.Accept(this, arg);
+ }
node.Body.Accept(this, arg);
return res;
}
@@ -333,8 +338,8 @@ Contract.Requires(node != null);
Contract.Invariant(cce.NonNullElements(ExprTodo));
}
- public VCExprNAryEnumerator(VCExprNAry completeExpr){
-Contract.Requires(completeExpr != null);
+ public VCExprNAryEnumerator(VCExprNAry completeExpr) {
+ Contract.Requires(completeExpr != null);
this.CompleteExpr = completeExpr;
Stack<VCExpr/*!*/>/*!*/ exprTodo = new Stack<VCExpr/*!*/>();
exprTodo.Push(completeExpr);
@@ -395,7 +400,7 @@ Contract.Requires(completeExpr != null);
this.Op = completeExpr.Op;
}
protected override bool Descend(VCExprNAry expr) {
- Contract.Requires(expr != null);
+ //Contract.Requires(expr != null);
return expr.Op.Equals(Op) &&
// we never skip nodes with type parameters
// (those are too interesting ...)
@@ -456,33 +461,42 @@ Contract.Requires(completeExpr != null);
dict[sym] = n - 1;
}
- public override Result Visit(VCExprQuantifier node, Arg arg){
-Contract.Requires(node != null);
+ public override Result Visit(VCExprQuantifier node, Arg arg) {
+ Contract.Requires(node != null);
// we temporarily add bound (term and type) variables to the
// corresponding lists
- foreach (VCExprVar/*!*/ v in node.BoundVars){Contract.Assert(v != null);
- AddBoundVar<VCExprVar>(BoundTermVarsDict, v);}
- foreach (TypeVariable/*!*/ v in node.TypeParameters){Contract.Assert(v != null);
- AddBoundVar<TypeVariable>(BoundTypeVarsDict, v);}
+ foreach (VCExprVar/*!*/ v in node.BoundVars) {
+ Contract.Assert(v != null);
+ AddBoundVar<VCExprVar>(BoundTermVarsDict, v);
+ }
+ foreach (TypeVariable/*!*/ v in node.TypeParameters) {
+ Contract.Assert(v != null);
+ AddBoundVar<TypeVariable>(BoundTypeVarsDict, v);
+ }
Result res;
try {
res = VisitAfterBinding(node, arg);
} finally {
- foreach (VCExprVar/*!*/ v in node.BoundVars){Contract.Assert(v != null);
- RemoveBoundVar<VCExprVar>(BoundTermVarsDict, v);}
+ foreach (VCExprVar/*!*/ v in node.BoundVars) {
+ Contract.Assert(v != null);
+ RemoveBoundVar<VCExprVar>(BoundTermVarsDict, v);
+ }
foreach (TypeVariable/*!*/ v in node.TypeParameters) {
Contract.Assert(v != null);
- RemoveBoundVar<TypeVariable>(BoundTypeVarsDict, v);}
+ RemoveBoundVar<TypeVariable>(BoundTypeVarsDict, v);
+ }
}
return res;
}
- public override Result Visit(VCExprLet node, Arg arg){
-Contract.Requires(node != null);
+ public override Result Visit(VCExprLet node, Arg arg) {
+ Contract.Requires(node != null);
// we temporarily add bound term variables to the
// corresponding lists
- foreach (VCExprVar/*!*/ v in node.BoundVars){Contract.Assert(v != null);
- AddBoundVar<VCExprVar>(BoundTermVarsDict, v);}
+ foreach (VCExprVar/*!*/ v in node.BoundVars) {
+ Contract.Assert(v != null);
+ AddBoundVar<VCExprVar>(BoundTermVarsDict, v);
+ }
Result res;
try {
@@ -529,34 +543,38 @@ Contract.Requires(node != null);
}
public virtual Result Visit(VCExprLiteral node, Arg arg) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
return CombineResults(new List<Result>(), arg);
}
- public virtual Result Visit(VCExprNAry node, Arg arg){
-Contract.Requires(node != null);
- List<Result>/*!*/ results = new List<Result> ();
+ public virtual Result Visit(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ List<Result>/*!*/ results = new List<Result>();
foreach (VCExpr/*!*/ subnode in node) {
Contract.Assert(subnode != null);
- results.Add(subnode.Accept(this, arg));}
+ results.Add(subnode.Accept(this, arg));
+ }
return CombineResults(results, arg);
}
public virtual Result Visit(VCExprVar node, Arg arg) {
- Contract.Requires(node != null);
+ //Contract.Requires(node != null);
return CombineResults(new List<Result>(), arg);
}
- public virtual Result Visit(VCExprQuantifier node, Arg arg){
-Contract.Requires(node != null);
- List<Result>/*!*/ result = new List<Result> ();
+ public virtual Result Visit(VCExprQuantifier node, Arg arg) {
+ //Contract.Requires(node != null);
+ List<Result>/*!*/ result = new List<Result>();
result.Add(node.Body.Accept(this, arg));
- foreach (VCTrigger/*!*/ trigger in node.Triggers){Contract.Assert(trigger != null);
- foreach (VCExpr/*!*/ expr in trigger.Exprs) {
- Contract.Assert(expr != null);
- result.Add(expr.Accept(this, arg));}}
+ foreach (VCTrigger/*!*/ trigger in node.Triggers) {
+ Contract.Assert(trigger != null);
+ foreach (VCExpr/*!*/ expr in trigger.Exprs) {
+ Contract.Assert(expr != null);
+ result.Add(expr.Accept(this, arg));
+ }
+ }
return CombineResults(result, arg);
}
- public virtual Result Visit(VCExprLet node, Arg arg){
-Contract.Requires(node != null);
- List<Result>/*!*/ results = new List<Result> ();
+ public virtual Result Visit(VCExprLet node, Arg arg) {
+ //Contract.Requires(node != null);
+ List<Result>/*!*/ results = new List<Result>();
// visit the bound expressions first
foreach (VCExprLetBinding/*!*/ binding in node) {
Contract.Assert(binding != null);
@@ -575,160 +593,161 @@ Contract.Requires(node != null);
}
////////////////////////////////////////////////////////////////////////////
- public class SizeComputingVisitor : TraversingVCExprVisitor<bool, bool> {
+ public class SizeComputingVisitor : TraversingVCExprVisitor<bool, bool> {
- private int Size = 0;
+ private int Size = 0;
- public static int ComputeSize(VCExpr expr) {
- Contract.Requires(expr != null);
- SizeComputingVisitor/*!*/ visitor = new SizeComputingVisitor();
- visitor.Traverse(expr, true);
- return visitor.Size;
- }
+ public static int ComputeSize(VCExpr expr) {
+ Contract.Requires(expr != null);
+ SizeComputingVisitor/*!*/ visitor = new SizeComputingVisitor();
+ visitor.Traverse(expr, true);
+ return visitor.Size;
+ }
- protected override bool StandardResult(VCExpr node, bool arg) {
- Contract.Requires(node != null);
- Size = Size + 1;
- return true;
- }
+ protected override bool StandardResult(VCExpr node, bool arg) {
+ //Contract.Requires(node != null);
+ Size = Size + 1;
+ return true;
}
+ }
- ////////////////////////////////////////////////////////////////////////////
+ ////////////////////////////////////////////////////////////////////////////
- // Collect all free term and type variables in a VCExpr. Type variables
- // can occur free either in the types of bound variables, or in the type
- // parameters of VCExprNAry.
-
- // the result and argument (of type bool) are not used currently
- public class FreeVariableCollector : BoundVarTraversingVCExprVisitor<bool, bool> {
- public readonly Dictionary<VCExprVar/*!*/, object>/*!*/ FreeTermVars = new Dictionary<VCExprVar/*!*/, object>();
- public readonly List<TypeVariable/*!*/>/*!*/ FreeTypeVars = new List<TypeVariable/*!*/>();
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(cce.NonNullElements(FreeTermVars));
- Contract.Invariant(cce.NonNullElements(FreeTypeVars));
- }
+ // Collect all free term and type variables in a VCExpr. Type variables
+ // can occur free either in the types of bound variables, or in the type
+ // parameters of VCExprNAry.
+
+ // the result and argument (of type bool) are not used currently
+ public class FreeVariableCollector : BoundVarTraversingVCExprVisitor<bool, bool> {
+ public readonly Dictionary<VCExprVar/*!*/, object>/*!*/ FreeTermVars = new Dictionary<VCExprVar/*!*/, object>();
+ public readonly List<TypeVariable/*!*/>/*!*/ FreeTypeVars = new List<TypeVariable/*!*/>();
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(cce.NonNullElements(FreeTermVars));
+ Contract.Invariant(cce.NonNullElements(FreeTypeVars));
+ }
- // not used
- protected override bool StandardResult(VCExpr node, bool arg) {
- Contract.Requires(node != null);
- return true;
- }
+ // not used
+ protected override bool StandardResult(VCExpr node, bool arg) {
+ //Contract.Requires(node != null);
+ return true;
+ }
- public static Dictionary<VCExprVar/*!*/, object/*!*/>/*!*/ FreeTermVariables(VCExpr node) {
- Contract.Requires(node != null);
- Contract.Ensures(cce.NonNullElements(Contract.Result<Dictionary<VCExprVar, object>>()));
- FreeVariableCollector collector = new FreeVariableCollector();
- collector.Traverse(node, true);
- return collector.FreeTermVars;
- }
+ public static Dictionary<VCExprVar/*!*/, object/*!*/>/*!*/ FreeTermVariables(VCExpr node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(cce.NonNullElements(Contract.Result<Dictionary<VCExprVar, object>>()));
+ FreeVariableCollector collector = new FreeVariableCollector();
+ collector.Traverse(node, true);
+ return collector.FreeTermVars;
+ }
- public static List<TypeVariable/*!*/>/*!*/ FreeTypeVariables(VCExpr node) {
- Contract.Requires(node != null);
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeVariable>>()));
- FreeVariableCollector collector = new FreeVariableCollector();
- collector.Traverse(node, true);
- return collector.FreeTypeVars;
- }
+ public static List<TypeVariable/*!*/>/*!*/ FreeTypeVariables(VCExpr node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeVariable>>()));
+ FreeVariableCollector collector = new FreeVariableCollector();
+ collector.Traverse(node, true);
+ return collector.FreeTypeVars;
+ }
- public void Reset() {
- FreeTermVars.Clear();
- FreeTypeVars.Clear();
- }
+ public void Reset() {
+ FreeTermVars.Clear();
+ FreeTypeVars.Clear();
+ }
- public void Collect(VCExpr node) {
- Contract.Requires(node != null);
- Traverse(node, true);
- }
+ public void Collect(VCExpr node) {
+ Contract.Requires(node != null);
+ Traverse(node, true);
+ }
- public void Collect(Type type) {
- Contract.Requires(type != null);
- AddTypeVariables(type.FreeVariables.ToList());
- }
+ public void Collect(Type type) {
+ Contract.Requires(type != null);
+ AddTypeVariables(type.FreeVariables.ToList());
+ }
- /////////////////////////////////////////////////////////////////////////
+ /////////////////////////////////////////////////////////////////////////
- private void CollectTypeVariables(IEnumerable<VCExprVar/*!*/>/*!*/ boundVars){Contract.Requires(cce.NonNullElements(boundVars));
+ private void CollectTypeVariables(IEnumerable<VCExprVar/*!*/>/*!*/ boundVars) {
+ Contract.Requires(cce.NonNullElements(boundVars));
foreach (VCExprVar/*!*/ var in boundVars) {
Contract.Assert(var != null);
Collect(var.Type);
}
}
- private void AddTypeVariables(IEnumerable<TypeVariable/*!*/>/*!*/ typeVars) {
- Contract.Requires(cce.NonNullElements(typeVars));
- foreach (TypeVariable/*!*/ tvar in typeVars) {
- Contract.Assert(tvar != null);
- if (!BoundTypeVars.Contains(tvar) && !FreeTypeVars.Contains(tvar))
- FreeTypeVars.Add(tvar);
- }
+ private void AddTypeVariables(IEnumerable<TypeVariable/*!*/>/*!*/ typeVars) {
+ Contract.Requires(cce.NonNullElements(typeVars));
+ foreach (TypeVariable/*!*/ tvar in typeVars) {
+ Contract.Assert(tvar != null);
+ if (!BoundTypeVars.Contains(tvar) && !FreeTypeVars.Contains(tvar))
+ FreeTypeVars.Add(tvar);
}
+ }
- public override bool Visit(VCExprVar node, bool arg) {
- Contract.Requires(node != null);
- if (!BoundTermVars.Contains(node) && !FreeTermVars.ContainsKey(node)) {
- FreeTermVars.Add(node, null);
- Collect(node.Type);
- }
- return true;
+ public override bool Visit(VCExprVar node, bool arg) {
+ Contract.Requires(node != null);
+ if (!BoundTermVars.Contains(node) && !FreeTermVars.ContainsKey(node)) {
+ FreeTermVars.Add(node, null);
+ Collect(node.Type);
}
+ return true;
+ }
- public override bool Visit(VCExprNAry node, bool arg) {
- Contract.Requires(node != null);
- foreach (Type/*!*/ t in node.TypeArguments) {
- Contract.Assert(t != null);
- Collect(t);
- }
- return base.Visit(node, arg);
+ public override bool Visit(VCExprNAry node, bool arg) {
+ Contract.Requires(node != null);
+ foreach (Type/*!*/ t in node.TypeArguments) {
+ Contract.Assert(t != null);
+ Collect(t);
}
+ return base.Visit(node, arg);
+ }
- protected override bool VisitAfterBinding(VCExprQuantifier node, bool arg) {
- Contract.Requires(node != null);
- CollectTypeVariables(node.BoundVars);
- return base.VisitAfterBinding(node, arg);
- }
+ protected override bool VisitAfterBinding(VCExprQuantifier node, bool arg) {
+ //Contract.Requires(node != null);
+ CollectTypeVariables(node.BoundVars);
+ return base.VisitAfterBinding(node, arg);
+ }
- protected override bool VisitAfterBinding(VCExprLet node, bool arg) {
- Contract.Requires(node != null);
- CollectTypeVariables(node.BoundVars);
- return base.VisitAfterBinding(node, arg);
- }
+ protected override bool VisitAfterBinding(VCExprLet node, bool arg) {
+ //Contract.Requires(node != null);
+ CollectTypeVariables(node.BoundVars);
+ return base.VisitAfterBinding(node, arg);
}
+ }
- ////////////////////////////////////////////////////////////////////////////
- // Framework for mutating VCExprs
-
- // The Visit implementations in the following visitor work
- // recursively, apart from the implementation for VCExprNAry that
- // uses its own stack when applied to nested nodes with the same
- // operator, e.g., (AND (AND (AND ...) ...) ...). This is necessary
- // to avoid stack overflows (like in TraversingVCExprVisitor)
-
- public abstract class MutatingVCExprVisitor<Arg>
- : IVCExprVisitor<VCExpr/*!*/, Arg> {
- protected readonly VCExpressionGenerator/*!*/ Gen;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(Gen != null);
- }
+ ////////////////////////////////////////////////////////////////////////////
+ // Framework for mutating VCExprs
+ // The Visit implementations in the following visitor work
+ // recursively, apart from the implementation for VCExprNAry that
+ // uses its own stack when applied to nested nodes with the same
+ // operator, e.g., (AND (AND (AND ...) ...) ...). This is necessary
+ // to avoid stack overflows (like in TraversingVCExprVisitor)
- public MutatingVCExprVisitor(VCExpressionGenerator gen) {
- Contract.Requires(gen != null);
- this.Gen = gen;
- }
+ public abstract class MutatingVCExprVisitor<Arg>
+ : IVCExprVisitor<VCExpr/*!*/, Arg> {
+ protected readonly VCExpressionGenerator/*!*/ Gen;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Gen != null);
+ }
- public VCExpr Mutate(VCExpr expr, Arg arg) {
- Contract.Requires(expr != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
- return expr.Accept(this, arg);
- }
- public List<VCExpr/*!*/>/*!*/ MutateSeq(IEnumerable<VCExpr/*!*/>/*!*/ exprs, Arg arg){
-Contract.Requires(cce.NonNullElements(exprs));
-Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
- List<VCExpr/*!*/>/*!*/ res = new List<VCExpr/*!*/> ();
+ public MutatingVCExprVisitor(VCExpressionGenerator gen) {
+ Contract.Requires(gen != null);
+ this.Gen = gen;
+ }
+
+ public VCExpr Mutate(VCExpr expr, Arg arg) {
+ Contract.Requires(expr != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return expr.Accept(this, arg);
+ }
+
+ public List<VCExpr/*!*/>/*!*/ MutateSeq(IEnumerable<VCExpr/*!*/>/*!*/ exprs, Arg arg) {
+ Contract.Requires(cce.NonNullElements(exprs));
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
+ List<VCExpr/*!*/>/*!*/ res = new List<VCExpr/*!*/>();
foreach (VCExpr/*!*/ expr in exprs) {
Contract.Assert(expr != null);
res.Add(expr.Accept(this, arg));
@@ -736,13 +755,14 @@ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
return res;
}
- private List<VCExpr/*!*/>/*!*/ MutateList(List<VCExpr/*!*/>/*!*/ exprs, Arg arg){
-Contract.Requires(cce.NonNullElements(exprs));
-Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
+ private List<VCExpr/*!*/>/*!*/ MutateList(List<VCExpr/*!*/>/*!*/ exprs, Arg arg) {
+ Contract.Requires(cce.NonNullElements(exprs));
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
bool changed = false;
- List<VCExpr/*!*/>/*!*/ res = new List<VCExpr/*!*/> ();
- foreach (VCExpr/*!*/ expr in exprs) {Contract.Assert(expr != null);
- VCExpr/*!*/ newExpr = expr.Accept(this, arg);
+ List<VCExpr/*!*/>/*!*/ res = new List<VCExpr/*!*/>();
+ foreach (VCExpr/*!*/ expr in exprs) {
+ Contract.Assert(expr != null);
+ VCExpr/*!*/ newExpr = expr.Accept(this, arg);
if (!Object.ReferenceEquals(expr, newExpr))
changed = true;
res.Add(newExpr);
@@ -752,65 +772,65 @@ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
return res;
}
- public virtual VCExpr Visit(VCExprLiteral node, Arg arg) {
- Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
- return node;
- }
+ public virtual VCExpr Visit(VCExprLiteral node, Arg arg) {
+ //Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return node;
+ }
- ////////////////////////////////////////////////////////////////////////////
-
- // Special element used to mark the positions in the todo-stack where
- // results have to be popped from the result-stack.
- private static readonly VCExpr/*!*/ CombineResultsMarker = new VCExprLiteral(Type.Bool);
-
- // The todo-stack contains records of the shape
- //
- // arg0
- // arg1
- // arg2
- // ...
- // CombineResultsMarker
- // f(arg0, arg1, arg2, ...) (the original expression)
-
- private readonly Stack<VCExpr/*!*/>/*!*/ NAryExprTodoStack = new Stack<VCExpr/*!*/>();
- private readonly Stack<VCExpr/*!*/>/*!*/ NAryExprResultStack = new Stack<VCExpr/*!*/>();
- [ContractInvariantMethod]
- void ObjectInvarianta() {
- Contract.Invariant(cce.NonNullElements(NAryExprResultStack));
- Contract.Invariant(cce.NonNullElements(NAryExprTodoStack));
- }
+ ////////////////////////////////////////////////////////////////////////////
+
+ // Special element used to mark the positions in the todo-stack where
+ // results have to be popped from the result-stack.
+ private static readonly VCExpr/*!*/ CombineResultsMarker = new VCExprLiteral(Type.Bool);
+
+ // The todo-stack contains records of the shape
+ //
+ // arg0
+ // arg1
+ // arg2
+ // ...
+ // CombineResultsMarker
+ // f(arg0, arg1, arg2, ...) (the original expression)
+
+ private readonly Stack<VCExpr/*!*/>/*!*/ NAryExprTodoStack = new Stack<VCExpr/*!*/>();
+ private readonly Stack<VCExpr/*!*/>/*!*/ NAryExprResultStack = new Stack<VCExpr/*!*/>();
+ [ContractInvariantMethod]
+ void ObjectInvarianta() {
+ Contract.Invariant(cce.NonNullElements(NAryExprResultStack));
+ Contract.Invariant(cce.NonNullElements(NAryExprTodoStack));
+ }
- private void PushTodo(VCExprNAry exprTodo) {
- Contract.Requires(exprTodo != null);
- NAryExprTodoStack.Push(exprTodo);
- NAryExprTodoStack.Push(CombineResultsMarker);
- for (int i = exprTodo.Arity - 1; i >= 0; --i)
- NAryExprTodoStack.Push(exprTodo[i]);
- }
+ private void PushTodo(VCExprNAry exprTodo) {
+ Contract.Requires(exprTodo != null);
+ NAryExprTodoStack.Push(exprTodo);
+ NAryExprTodoStack.Push(CombineResultsMarker);
+ for (int i = exprTodo.Arity - 1; i >= 0; --i)
+ NAryExprTodoStack.Push(exprTodo[i]);
+ }
- public virtual VCExpr Visit(VCExprNAry node, Arg arg){
-Contract.Requires(node != null);
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ public virtual VCExpr Visit(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
VCExprOp/*!*/ op = node.Op;
- Contract.Assert(op != null);
+ Contract.Assert(op != null);
int initialStackSize = NAryExprTodoStack.Count;
int initialResultStackSize = NAryExprResultStack.Count;
PushTodo(node);
-
+
while (NAryExprTodoStack.Count > initialStackSize) {
VCExpr/*!*/ subExpr = NAryExprTodoStack.Pop();
Contract.Assert(subExpr != null);
-
+
if (Object.ReferenceEquals(subExpr, CombineResultsMarker)) {
//
// assemble a result
VCExprNAry/*!*/ originalExpr = (VCExprNAry)NAryExprTodoStack.Pop();
Contract.Assert(originalExpr != null);
bool changed = false;
- List<VCExpr/*!*/>/*!*/ newSubExprs = new List<VCExpr/*!*/> ();
+ List<VCExpr/*!*/>/*!*/ newSubExprs = new List<VCExpr/*!*/>();
for (int i = op.Arity - 1; i >= 0; --i) {
VCExpr/*!*/ nextSubExpr = NAryExprResultStack.Pop();
@@ -819,15 +839,15 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
changed = true;
newSubExprs.Insert(0, nextSubExpr);
}
-
+
NAryExprResultStack.Push(UpdateModifiedNode(originalExpr, newSubExprs, changed, arg));
//
} else {
//
VCExprNAry narySubExpr = subExpr as VCExprNAry;
if (narySubExpr != null && narySubExpr.Op.Equals(op) &&
- // as in VCExprNAryUniformOpEnumerator, all expressions with
- // type parameters are allowed to be inspected more closely
+ // as in VCExprNAryUniformOpEnumerator, all expressions with
+ // type parameters are allowed to be inspected more closely
narySubExpr.TypeParamArity == 0) {
PushTodo(narySubExpr);
} else {
@@ -841,37 +861,37 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
return NAryExprResultStack.Pop();
}
- protected virtual VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, List<VCExpr/*!*/>/*!*/ newSubExprs, // has any of the subexpressions changed?
- bool changed,
- Arg arg) {
- Contract.Requires(cce.NonNullElements(newSubExprs));
- Contract.Ensures(Contract.Result<VCExpr>() != null);
+ protected virtual VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, List<VCExpr/*!*/>/*!*/ newSubExprs, // has any of the subexpressions changed?
+ bool changed,
+ Arg arg) {
+ Contract.Requires(cce.NonNullElements(newSubExprs));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
- if (changed)
- return Gen.Function(originalNode.Op,
- newSubExprs, originalNode.TypeArguments);
- else
- return originalNode;
- }
+ if (changed)
+ return Gen.Function(originalNode.Op,
+ newSubExprs, originalNode.TypeArguments);
+ else
+ return originalNode;
+ }
- ////////////////////////////////////////////////////////////////////////////
+ ////////////////////////////////////////////////////////////////////////////
- public virtual VCExpr Visit(VCExprVar node, Arg arg) {
- Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
- return node;
- }
+ public virtual VCExpr Visit(VCExprVar node, Arg arg) {
+ //Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return node;
+ }
- protected List<VCTrigger/*!*/>/*!*/ MutateTriggers(List<VCTrigger/*!*/>/*!*/ triggers, Arg arg){
-Contract.Requires(cce.NonNullElements(triggers));
-Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCTrigger>>()));
- List<VCTrigger/*!*/>/*!*/ newTriggers = new List<VCTrigger/*!*/> ();
+ protected List<VCTrigger/*!*/>/*!*/ MutateTriggers(List<VCTrigger/*!*/>/*!*/ triggers, Arg arg) {
+ Contract.Requires(cce.NonNullElements(triggers));
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCTrigger>>()));
+ List<VCTrigger/*!*/>/*!*/ newTriggers = new List<VCTrigger/*!*/>();
bool changed = false;
foreach (VCTrigger/*!*/ trigger in triggers) {
Contract.Assert(trigger != null);
List<VCExpr/*!*/>/*!*/ exprs = trigger.Exprs;
List<VCExpr/*!*/>/*!*/ newExprs = MutateList(exprs, arg);
-
+
if (Object.ReferenceEquals(exprs, newExprs)) {
newTriggers.Add(trigger);
} else {
@@ -884,15 +904,15 @@ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCTrigger>>()));
return newTriggers;
}
- public virtual VCExpr Visit(VCExprQuantifier node, Arg arg){
-Contract.Requires(node != null);
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ public virtual VCExpr Visit(VCExprQuantifier node, Arg arg) {
+ //Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
bool changed = false;
VCExpr/*!*/ body = node.Body;
- Contract.Assert(body != null);
+ Contract.Assert(body != null);
VCExpr/*!*/ newbody = body.Accept(this, arg);
- Contract.Assert(newbody != null);
+ Contract.Assert(newbody != null);
if (!Object.ReferenceEquals(body, newbody))
changed = true;
@@ -910,9 +930,9 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
newTriggers, node.Infos, newbody);
}
- public virtual VCExpr Visit(VCExprLet node, Arg arg){
-Contract.Requires(node != null);
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ public virtual VCExpr Visit(VCExprLet node, Arg arg) {
+ //Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
bool changed = false;
VCExpr/*!*/ body = node.Body;
@@ -920,7 +940,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
if (!Object.ReferenceEquals(body, newbody))
changed = true;
- List<VCExprLetBinding/*!*/>/*!*/ newbindings = new List<VCExprLetBinding/*!*/> ();
+ List<VCExprLetBinding/*!*/>/*!*/ newbindings = new List<VCExprLetBinding/*!*/>();
for (int i = 0; i < node.Length; ++i) {
VCExprLetBinding/*!*/ binding = node[i];
Contract.Assert(binding != null);
@@ -938,29 +958,29 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
return node;
return Gen.Let(newbindings, newbody);
}
- }
+ }
- ////////////////////////////////////////////////////////////////////////////
- // Substitutions and a visitor for applying substitutions. A substitution can
- // substitute both type variables and term variables
-
- public class VCExprSubstitution {
- private readonly List<IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/>/*!*/ TermSubsts;
- [ContractInvariantMethod]
- void TermSubstsInvariantMethod() {
- Contract.Invariant(TermSubsts != null && Contract.ForAll(TermSubsts, i => cce.NonNullElements(i)));
- }
- private readonly List<IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/>/*!*/ TypeSubsts;
- [ContractInvariantMethod]
- void TypeSubstsInvariantMethod() {
- Contract.Invariant(TermSubsts != null && Contract.ForAll(TypeSubsts, i => cce.NonNullElements(i)));
- }
+ ////////////////////////////////////////////////////////////////////////////
+ // Substitutions and a visitor for applying substitutions. A substitution can
+ // substitute both type variables and term variables
+
+ public class VCExprSubstitution {
+ private readonly List<IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/>/*!*/ TermSubsts;
+ [ContractInvariantMethod]
+ void TermSubstsInvariantMethod() {
+ Contract.Invariant(TermSubsts != null && Contract.ForAll(TermSubsts, i => cce.NonNullElements(i)));
+ }
+ private readonly List<IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/>/*!*/ TypeSubsts;
+ [ContractInvariantMethod]
+ void TypeSubstsInvariantMethod() {
+ Contract.Invariant(TermSubsts != null && Contract.ForAll(TypeSubsts, i => cce.NonNullElements(i)));
+ }
- public VCExprSubstitution(IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/ termSubst, IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst) {
+ public VCExprSubstitution(IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/ termSubst, IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst) {
Contract.Requires(cce.NonNullElements(termSubst));
Contract.Requires(cce.NonNullElements(typeSubst));
List<IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/>/*!*/ termSubsts =
- new List<IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/> ();
+ new List<IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/>();
termSubsts.Add(termSubst);
List<IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/>/*!*/ typeSubsts =
new List<IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/>();
@@ -969,185 +989,190 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
this.TypeSubsts = typeSubsts;
}
- public VCExprSubstitution() :this(new Dictionary<VCExprVar/*!*/, VCExpr/*!*/>(), new Dictionary<TypeVariable/*!*/, Type/*!*/>()){
-
+ public VCExprSubstitution()
+ : this(new Dictionary<VCExprVar/*!*/, VCExpr/*!*/>(), new Dictionary<TypeVariable/*!*/, Type/*!*/>()) {
+
}
- public void PushScope() {
- TermSubsts.Add(new Dictionary<VCExprVar/*!*/, VCExpr/*!*/> ());
+ public void PushScope() {
+ TermSubsts.Add(new Dictionary<VCExprVar/*!*/, VCExpr/*!*/>());
TypeSubsts.Add(new Dictionary<TypeVariable/*!*/, Type/*!*/>());
}
- public void PopScope() {
- TermSubsts.RemoveAt(TermSubsts.Count - 1);
- TypeSubsts.RemoveAt(TypeSubsts.Count - 1);
- }
+ public void PopScope() {
+ TermSubsts.RemoveAt(TermSubsts.Count - 1);
+ TypeSubsts.RemoveAt(TypeSubsts.Count - 1);
+ }
- public VCExpr this[VCExprVar/*!*/ var] {
- get {
- Contract.Requires(var != null);
- VCExpr res;
- for (int i = TermSubsts.Count - 1; i >= 0; --i) {
- if (TermSubsts[i].TryGetValue(var, out res))
- return res;
- }
- return null;
- }
- set {
- TermSubsts[TermSubsts.Count - 1][var] = cce.NonNull(value);
+ public VCExpr this[VCExprVar/*!*/ var] {
+ get {
+ Contract.Requires(var != null);
+ VCExpr res;
+ for (int i = TermSubsts.Count - 1; i >= 0; --i) {
+ if (TermSubsts[i].TryGetValue(var, out res))
+ return res;
}
+ return null;
}
-
- public Type this[TypeVariable/*!*/ var] {
- get {
- Contract.Requires(var != null);
- Type res;
- for (int i = TypeSubsts.Count - 1; i >= 0; --i) {
- if (TypeSubsts[i].TryGetValue(var, out res))
- return res;
- }
- return null;
- }
- set {
- TypeSubsts[TypeSubsts.Count - 1][var] = cce.NonNull(value);
- }
+ set {
+ TermSubsts[TermSubsts.Count - 1][var] = cce.NonNull(value);
}
+ }
- public bool ContainsKey(VCExprVar var) {
+ public Type this[TypeVariable/*!*/ var] {
+ get {
Contract.Requires(var != null);
- return this[var] != null;
+ Type res;
+ for (int i = TypeSubsts.Count - 1; i >= 0; --i) {
+ if (TypeSubsts[i].TryGetValue(var, out res))
+ return res;
+ }
+ return null;
}
-
- public bool ContainsKey(TypeVariable var) {
- Contract.Requires(var != null);
- return this[var] != null;
+ set {
+ TypeSubsts[TypeSubsts.Count - 1][var] = cce.NonNull(value);
}
+ }
- public bool TermSubstIsEmpty {
- get {
- return Contract.ForAll(TermSubsts, dict => dict.Count == 0);
- }
+ public bool ContainsKey(VCExprVar var) {
+ Contract.Requires(var != null);
+ return this[var] != null;
+ }
+
+ public bool ContainsKey(TypeVariable var) {
+ Contract.Requires(var != null);
+ return this[var] != null;
+ }
+
+ public bool TermSubstIsEmpty {
+ get {
+ return Contract.ForAll(TermSubsts, dict => dict.Count == 0);
}
+ }
- public bool TypeSubstIsEmpty {
- get {
- return Contract.ForAll(TypeSubsts, dict => dict.Count == 0);
- }
+ public bool TypeSubstIsEmpty {
+ get {
+ return Contract.ForAll(TypeSubsts, dict => dict.Count == 0);
}
+ }
- public IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ ToTypeSubst {
- get {
- Contract.Ensures(cce.NonNullElements(Contract.Result < IDictionary<TypeVariable, Type>>()));
- IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ res = new Dictionary<TypeVariable/*!*/, Type/*!*/>();
- foreach (IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ dict in TypeSubsts) {
- foreach (KeyValuePair<TypeVariable/*!*/, Type/*!*/> pair in dict) {
- Contract.Assert(cce.NonNullElements(pair));
- // later ones overwrite earlier ones
- res[pair.Key] = pair.Value;
- }
+ public IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ ToTypeSubst {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<IDictionary<TypeVariable, Type>>()));
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ res = new Dictionary<TypeVariable/*!*/, Type/*!*/>();
+ foreach (IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ dict in TypeSubsts) {
+ foreach (KeyValuePair<TypeVariable/*!*/, Type/*!*/> pair in dict) {
+ Contract.Assert(cce.NonNullElements(pair));
+ // later ones overwrite earlier ones
+ res[pair.Key] = pair.Value;
}
- return res;
}
+ return res;
}
+ }
- // the variables that are not mapped to themselves
- public IEnumerable<VCExprVar/*!*/>/*!*/ TermDomain {
- get {Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<VCExprVar>>()));
- Dictionary<VCExprVar/*!*/, bool>/*!*/ domain = new Dictionary<VCExprVar/*!*/, bool> ();
- foreach (IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/ dict in TermSubsts) {
- Contract.Assert(dict != null);
- foreach (VCExprVar/*!*/ var in dict.Keys) {
- Contract.Assert(var != null);
- if (!var.Equals(this[var]))
- domain.Add(var, true);
- }
- }
- return domain.Keys;
+ // the variables that are not mapped to themselves
+ public IEnumerable<VCExprVar/*!*/>/*!*/ TermDomain {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<VCExprVar>>()));
+ Dictionary<VCExprVar/*!*/, bool>/*!*/ domain = new Dictionary<VCExprVar/*!*/, bool>();
+ foreach (IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/ dict in TermSubsts) {
+ Contract.Assert(dict != null);
+ foreach (VCExprVar/*!*/ var in dict.Keys) {
+ Contract.Assert(var != null);
+ if (!var.Equals(this[var]))
+ domain.Add(var, true);
+ }
}
+ return domain.Keys;
}
+ }
- // the variables that are not mapped to themselves
- public IEnumerable<TypeVariable/*!*/>/*!*/ TypeDomain {
- get {Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<TypeVariable>>()));
- Dictionary<TypeVariable/*!*/, bool>/*!*/ domain = new Dictionary<TypeVariable/*!*/, bool> ();
- foreach (IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ dict in TypeSubsts) {
- Contract.Assert(dict != null);
- foreach (TypeVariable/*!*/ var in dict.Keys) {
- Contract.Assert(var != null);
- if (!var.Equals(this[var]))
- domain.Add(var, true);
+ // the variables that are not mapped to themselves
+ public IEnumerable<TypeVariable/*!*/>/*!*/ TypeDomain {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<TypeVariable>>()));
+ Dictionary<TypeVariable/*!*/, bool>/*!*/ domain = new Dictionary<TypeVariable/*!*/, bool>();
+ foreach (IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ dict in TypeSubsts) {
+ Contract.Assert(dict != null);
+ foreach (TypeVariable/*!*/ var in dict.Keys) {
+ Contract.Assert(var != null);
+ if (!var.Equals(this[var]))
+ domain.Add(var, true);
+ }
}
+ return domain.Keys;
}
- return domain.Keys;
}
- }
- public FreeVariableCollector/*!*/ Codomains {
- get {Contract.Ensures(Contract.Result<FreeVariableCollector>() != null);
+ public FreeVariableCollector/*!*/ Codomains {
+ get {
+ Contract.Ensures(Contract.Result<FreeVariableCollector>() != null);
- FreeVariableCollector/*!*/ coll = new FreeVariableCollector ();
+ FreeVariableCollector/*!*/ coll = new FreeVariableCollector();
foreach (VCExprVar/*!*/ var in TermDomain)
coll.Collect(cce.NonNull(this)[var]);
foreach (TypeVariable/*!*/ var in TypeDomain)
coll.Collect(cce.NonNull(this)[var]);
return coll;
}
- }
+ }
- public VCExprSubstitution Clone() {
-Contract.Ensures(Contract.Result<VCExprSubstitution>() != null);
- VCExprSubstitution/*!*/ res = new VCExprSubstitution ();
+ public VCExprSubstitution Clone() {
+ Contract.Ensures(Contract.Result<VCExprSubstitution>() != null);
+ VCExprSubstitution/*!*/ res = new VCExprSubstitution();
foreach (IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/ dict in TermSubsts)
res.TermSubsts.Add(HelperFuns.Clone(dict));
foreach (IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ dict in TypeSubsts)
res.TypeSubsts.Add(HelperFuns.Clone(dict));
return res;
}
- }
+ }
- /////////////////////////////////////////////////////////////////////////////////
+ /////////////////////////////////////////////////////////////////////////////////
- public class SubstitutingVCExprVisitor
- : MutatingVCExprVisitor<VCExprSubstitution/*!*/> {
- public SubstitutingVCExprVisitor(VCExpressionGenerator gen) :base(gen){
- Contract.Requires(gen != null);
-
- }
+ public class SubstitutingVCExprVisitor
+ : MutatingVCExprVisitor<VCExprSubstitution/*!*/> {
+ public SubstitutingVCExprVisitor(VCExpressionGenerator gen)
+ : base(gen) {
+ Contract.Requires(gen != null);
+
+ }
- // when descending across a binder, we have to check that no collisions
- // or variable capture can occur. if this might happen, we replace the
- // term and type variables bound by the binder with fresh variables
- private bool CollisionPossible(IEnumerable<TypeVariable/*!*/>/*!*/ typeParams, IEnumerable<VCExprVar/*!*/>/*!*/ boundVars, VCExprSubstitution/*!*/ substitution) {
+ // when descending across a binder, we have to check that no collisions
+ // or variable capture can occur. if this might happen, we replace the
+ // term and type variables bound by the binder with fresh variables
+ private bool CollisionPossible(IEnumerable<TypeVariable/*!*/>/*!*/ typeParams, IEnumerable<VCExprVar/*!*/>/*!*/ boundVars, VCExprSubstitution/*!*/ substitution) {
Contract.Requires(cce.NonNullElements(typeParams));
Contract.Requires(cce.NonNullElements(boundVars));
Contract.Requires(substitution != null);
// variables can be shadowed by a binder
- if (Contract.Exists(typeParams, var=> substitution.ContainsKey(var)) ||
- Contract.Exists(boundVars, var=> substitution.ContainsKey(var)))
+ if (Contract.Exists(typeParams, var => substitution.ContainsKey(var)) ||
+ Contract.Exists(boundVars, var => substitution.ContainsKey(var)))
return true;
// compute the codomain of the substitution
FreeVariableCollector coll = substitution.Codomains;
Contract.Assert(coll != null);
// variables could be captured when applying the substitution
- return Contract.Exists(typeParams, var=> coll.FreeTypeVars.Contains(var)) ||
- Contract.Exists(boundVars, var=> coll.FreeTermVars.ContainsKey(var));
+ return Contract.Exists(typeParams, var => coll.FreeTypeVars.Contains(var)) ||
+ Contract.Exists(boundVars, var => coll.FreeTermVars.ContainsKey(var));
}
- // can be overwritten if names of bound variables are to be changed
- protected virtual string ChooseNewVariableName(string oldName) {
- Contract.Requires(oldName != null);
- Contract.Ensures(Contract.Result<string>() != null);
- return oldName;
- }
+ // can be overwritten if names of bound variables are to be changed
+ protected virtual string ChooseNewVariableName(string oldName) {
+ Contract.Requires(oldName != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+ return oldName;
+ }
- // handle type parameters in VCExprNAry
- protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, List<VCExpr/*!*/>/*!*/ newSubExprs, bool changed, VCExprSubstitution/*!*/ substitution) {
- Contract.Requires(originalNode != null);
- Contract.Requires(cce.NonNullElements(newSubExprs));
- Contract.Requires(substitution != null);
+ // handle type parameters in VCExprNAry
+ protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, List<VCExpr/*!*/>/*!*/ newSubExprs, bool changed, VCExprSubstitution/*!*/ substitution) {
+ //Contract.Requires(originalNode != null);
+ //Contract.Requires(cce.NonNullElements(newSubExprs));
+ //Contract.Requires(substitution != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
- List<Type/*!*/>/*!*/ typeParams = new List<Type/*!*/> ();
+ List<Type/*!*/>/*!*/ typeParams = new List<Type/*!*/>();
foreach (Type/*!*/ t in originalNode.TypeArguments) {
Contract.Assert(t != null);
Type/*!*/ newType = t.Substitute(substitution.ToTypeSubst);
@@ -1162,272 +1187,273 @@ Contract.Ensures(Contract.Result<VCExprSubstitution>() != null);
return originalNode;
}
- public override VCExpr/*!*/ Visit(VCExprQuantifier/*!*/ node, VCExprSubstitution/*!*/ substitution) {
- Contract.Requires(node != null);
- Contract.Requires(substitution != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
+ public override VCExpr/*!*/ Visit(VCExprQuantifier/*!*/ node, VCExprSubstitution/*!*/ substitution) {
+ Contract.Requires(node != null);
+ Contract.Requires(substitution != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
- // the default is to refresh bound variables only if necessary
- // because of collisions
- return Visit(node, substitution, false);
- }
+ // the default is to refresh bound variables only if necessary
+ // because of collisions
+ return Visit(node, substitution, false);
+ }
- public VCExpr/*!*/ Visit(VCExprQuantifier/*!*/ node, VCExprSubstitution/*!*/ substitution, bool refreshBoundVariables) {
- Contract.Requires(node != null);
- Contract.Requires(substitution != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- substitution.PushScope();
- try {
-
- List<TypeVariable/*!*/>/*!*/ typeParams = node.TypeParameters;
- Contract.Assert(cce.NonNullElements(typeParams));
- bool refreshAllVariables = refreshBoundVariables ||
- CollisionPossible(node.TypeParameters, node.BoundVars, substitution);
- if (refreshAllVariables) {
- // we introduce fresh type variables to ensure that none gets captured
- typeParams = new List<TypeVariable/*!*/>();
- foreach (TypeVariable/*!*/ var in node.TypeParameters) {
- Contract.Assert(var != null);
- TypeVariable/*!*/ freshVar =
- new TypeVariable(Token.NoToken, ChooseNewVariableName(var.Name));
- Contract.Assert(freshVar != null);
- typeParams.Add(freshVar);
- substitution[var] = freshVar;
- // this might overwrite other elements of the substitution, deliberately
- }
- }
+ public VCExpr/*!*/ Visit(VCExprQuantifier/*!*/ node, VCExprSubstitution/*!*/ substitution, bool refreshBoundVariables) {
+ Contract.Requires(node != null);
+ Contract.Requires(substitution != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ substitution.PushScope();
+ try {
- List<VCExprVar/*!*/>/*!*/ boundVars = node.BoundVars;
- Contract.Assert(cce.NonNullElements(boundVars));
- if (refreshAllVariables || !substitution.TypeSubstIsEmpty) {
- // collisions are possible, or we also substitute type variables. in this case
- // the bound term variables have to be replaced with fresh variables with the
- // right types
- boundVars = new List<VCExprVar/*!*/>();
- IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst = substitution.ToTypeSubst;
- Contract.Assert(cce.NonNullElements(typeSubst));
- foreach (VCExprVar/*!*/ var in node.BoundVars) {
- Contract.Assert(var != null);
- VCExprVar/*!*/ freshVar =
- Gen.Variable(ChooseNewVariableName(var.Name),
- var.Type.Substitute(typeSubst));
- Contract.Assert(freshVar != null);
- boundVars.Add(freshVar);
- substitution[var] = freshVar;
- // this might overwrite other elements of the substitution, deliberately
- }
+ List<TypeVariable/*!*/>/*!*/ typeParams = node.TypeParameters;
+ Contract.Assert(cce.NonNullElements(typeParams));
+ bool refreshAllVariables = refreshBoundVariables ||
+ CollisionPossible(node.TypeParameters, node.BoundVars, substitution);
+ if (refreshAllVariables) {
+ // we introduce fresh type variables to ensure that none gets captured
+ typeParams = new List<TypeVariable/*!*/>();
+ foreach (TypeVariable/*!*/ var in node.TypeParameters) {
+ Contract.Assert(var != null);
+ TypeVariable/*!*/ freshVar =
+ new TypeVariable(Token.NoToken, ChooseNewVariableName(var.Name));
+ Contract.Assert(freshVar != null);
+ typeParams.Add(freshVar);
+ substitution[var] = freshVar;
+ // this might overwrite other elements of the substitution, deliberately
}
+ }
- List<VCTrigger/*!*/>/*!*/ newTriggers = new List<VCTrigger/*!*/>();
- foreach (VCTrigger/*!*/ trigger in node.Triggers) {
- Contract.Assert(trigger != null);
- newTriggers.Add(Gen.Trigger(trigger.Pos, MutateSeq(trigger.Exprs, substitution)));
+ List<VCExprVar/*!*/>/*!*/ boundVars = node.BoundVars;
+ Contract.Assert(cce.NonNullElements(boundVars));
+ if (refreshAllVariables || !substitution.TypeSubstIsEmpty) {
+ // collisions are possible, or we also substitute type variables. in this case
+ // the bound term variables have to be replaced with fresh variables with the
+ // right types
+ boundVars = new List<VCExprVar/*!*/>();
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst = substitution.ToTypeSubst;
+ Contract.Assert(cce.NonNullElements(typeSubst));
+ foreach (VCExprVar/*!*/ var in node.BoundVars) {
+ Contract.Assert(var != null);
+ VCExprVar/*!*/ freshVar =
+ Gen.Variable(ChooseNewVariableName(var.Name),
+ var.Type.Substitute(typeSubst));
+ Contract.Assert(freshVar != null);
+ boundVars.Add(freshVar);
+ substitution[var] = freshVar;
+ // this might overwrite other elements of the substitution, deliberately
}
+ }
- VCExpr/*!*/ newBody = Mutate(node.Body, substitution);
- Contract.Assert(newBody != null);
+ List<VCTrigger/*!*/>/*!*/ newTriggers = new List<VCTrigger/*!*/>();
+ foreach (VCTrigger/*!*/ trigger in node.Triggers) {
+ Contract.Assert(trigger != null);
+ newTriggers.Add(Gen.Trigger(trigger.Pos, MutateSeq(trigger.Exprs, substitution)));
+ }
- return Gen.Quantify(node.Quan, typeParams, boundVars,
- newTriggers, node.Infos, newBody);
+ VCExpr/*!*/ newBody = Mutate(node.Body, substitution);
+ Contract.Assert(newBody != null);
- } finally {
- substitution.PopScope();
- }
- }
+ return Gen.Quantify(node.Quan, typeParams, boundVars,
+ newTriggers, node.Infos, newBody);
- public override VCExpr Visit(VCExprVar node, VCExprSubstitution substitution) {
- Contract.Requires(substitution != null);
- Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
- VCExpr res = substitution[node];
- if (res != null)
- return res;
- return node;
+ } finally {
+ substitution.PopScope();
}
+ }
- public override VCExpr Visit(VCExprLet node, VCExprSubstitution substitution) {
- Contract.Requires(substitution != null);
- Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
- // the default is to refresh bound variables only if necessary
- // because of collisions
- return Visit(node, substitution, false);
- }
+ public override VCExpr Visit(VCExprVar node, VCExprSubstitution substitution) {
+ Contract.Requires(substitution != null);
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ VCExpr res = substitution[node];
+ if (res != null)
+ return res;
+ return node;
+ }
+
+ public override VCExpr Visit(VCExprLet node, VCExprSubstitution substitution) {
+ Contract.Requires(substitution != null);
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ // the default is to refresh bound variables only if necessary
+ // because of collisions
+ return Visit(node, substitution, false);
+ }
- public VCExpr Visit(VCExprLet node, VCExprSubstitution substitution, bool refreshBoundVariables){
-Contract.Requires(substitution != null);
-Contract.Requires(node != null);
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ public VCExpr Visit(VCExprLet node, VCExprSubstitution substitution, bool refreshBoundVariables) {
+ Contract.Requires(substitution != null);
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
// let-expressions do not have type parameters (fortunately ...)
- substitution.PushScope (); try {
+ substitution.PushScope();
+ try {
- bool refreshAllVariables =
- refreshBoundVariables ||
- !substitution.TypeSubstIsEmpty ||
- CollisionPossible(new List<TypeVariable/*!*/> (), node.BoundVars, substitution);
+ bool refreshAllVariables =
+ refreshBoundVariables ||
+ !substitution.TypeSubstIsEmpty ||
+ CollisionPossible(new List<TypeVariable/*!*/>(), node.BoundVars, substitution);
- List<VCExprVar/*!*/>/*!*/ newBoundVars = node.BoundVars;
+ List<VCExprVar/*!*/>/*!*/ newBoundVars = node.BoundVars;
Contract.Assert(cce.NonNullElements(newBoundVars));
- if (refreshAllVariables) {
- // collisions are possible, or we also substitute type variables. in this case
- // the bound term variables have to be replaced with fresh variables with the
- // right types
- newBoundVars = new List<VCExprVar/*!*/> ();
- IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst = substitution.ToTypeSubst;
- Contract.Assert(cce.NonNullElements(typeSubst));
- foreach (VCExprVar/*!*/ var in node.BoundVars) {
- Contract.Assert(var != null);
- VCExprVar/*!*/ freshVar =
- Gen.Variable(ChooseNewVariableName(var.Name),
- var.Type.Substitute(typeSubst));
- Contract.Assert(freshVar != null);
- newBoundVars.Add(freshVar);
- substitution[var] = freshVar;
- // this might overwrite other elements of the substitution, deliberately
+ if (refreshAllVariables) {
+ // collisions are possible, or we also substitute type variables. in this case
+ // the bound term variables have to be replaced with fresh variables with the
+ // right types
+ newBoundVars = new List<VCExprVar/*!*/>();
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst = substitution.ToTypeSubst;
+ Contract.Assert(cce.NonNullElements(typeSubst));
+ foreach (VCExprVar/*!*/ var in node.BoundVars) {
+ Contract.Assert(var != null);
+ VCExprVar/*!*/ freshVar =
+ Gen.Variable(ChooseNewVariableName(var.Name),
+ var.Type.Substitute(typeSubst));
+ Contract.Assert(freshVar != null);
+ newBoundVars.Add(freshVar);
+ substitution[var] = freshVar;
+ // this might overwrite other elements of the substitution, deliberately
+ }
}
- }
- List<VCExprLetBinding/*!*/>/*!*/ newbindings = new List<VCExprLetBinding/*!*/> ();
- for (int i = 0; i < node.Length; ++i) {
- VCExprLetBinding/*!*/ binding = node[i];
- Contract.Assert(binding != null);
- newbindings.Add(Gen.LetBinding(newBoundVars[i], Mutate(binding.E, substitution)));
- }
+ List<VCExprLetBinding/*!*/>/*!*/ newbindings = new List<VCExprLetBinding/*!*/>();
+ for (int i = 0; i < node.Length; ++i) {
+ VCExprLetBinding/*!*/ binding = node[i];
+ Contract.Assert(binding != null);
+ newbindings.Add(Gen.LetBinding(newBoundVars[i], Mutate(binding.E, substitution)));
+ }
- VCExpr/*!*/ newBody = Mutate(node.Body, substitution);
- Contract.Assert(newBody != null);
- return Gen.Let(newbindings, newBody);
+ VCExpr/*!*/ newBody = Mutate(node.Body, substitution);
+ Contract.Assert(newBody != null);
+ return Gen.Let(newbindings, newBody);
} finally {
substitution.PopScope();
}
}
- }
+ }
- ////////////////////////////////////////////////////////////////////////////
- [ContractClassFor(typeof(StandardVCExprOpVisitor<,>))]
- public abstract class StandardVCExprOpVisitorContracts<Result, Arg> : StandardVCExprOpVisitor<Result, Arg> {
- protected override Result StandardResult(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- throw new NotImplementedException();
- }
+ ////////////////////////////////////////////////////////////////////////////
+ [ContractClassFor(typeof(StandardVCExprOpVisitor<,>))]
+ public abstract class StandardVCExprOpVisitorContracts<Result, Arg> : StandardVCExprOpVisitor<Result, Arg> {
+ protected override Result StandardResult(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
}
+ }
- [ContractClass(typeof(StandardVCExprOpVisitorContracts<,>))]
- public abstract class StandardVCExprOpVisitor<Result, Arg>
- : IVCExprOpVisitor<Result, Arg> {
- protected abstract Result StandardResult(VCExprNAry/*!*/ node, Arg arg);
+ [ContractClass(typeof(StandardVCExprOpVisitorContracts<,>))]
+ public abstract class StandardVCExprOpVisitor<Result, Arg>
+ : IVCExprOpVisitor<Result, Arg> {
+ protected abstract Result StandardResult(VCExprNAry/*!*/ node, Arg arg);
- public virtual Result VisitNotOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitEqOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitNeqOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitAndOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitOrOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitImpliesOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitDistinctOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitLabelOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitSelectOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitStoreOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitBvOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitBvExtractOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitBvConcatOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitIfThenElseOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitCustomOp (VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
+ public virtual Result VisitNotOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
return StandardResult(node, arg);
}
- public virtual Result VisitAddOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitSubOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitMulOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitDivOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitModOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitLtOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitLeOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitGtOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitGeOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitSubtypeOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitSubtype3Op(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
- public virtual Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) {
- Contract.Requires(node != null);
- return StandardResult(node, arg);
- }
+ public virtual Result VisitEqOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitNeqOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitAndOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitOrOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitImpliesOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitDistinctOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitLabelOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
}
+ public virtual Result VisitSelectOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitStoreOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitBvOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitBvExtractOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitBvConcatOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitIfThenElseOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitCustomOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitAddOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitSubOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitMulOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitDivOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitModOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitLtOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitLeOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitGtOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitGeOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitSubtypeOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitSubtype3Op(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ }
- } \ No newline at end of file
+} \ No newline at end of file