From f09bf83d24438d712021ada6fab252b0f7f11986 Mon Sep 17 00:00:00 2001 From: tabarbe Date: Fri, 27 Aug 2010 21:52:03 +0000 Subject: Boogie: Commented out all occurences of repeated inherited contracts - makes fewer error messages when compiling with runtime checking on. --- Source/VCExpr/SimplifyLikeLineariser.cs | 683 +++++++++++++++++--------------- 1 file changed, 355 insertions(+), 328 deletions(-) (limited to 'Source/VCExpr/SimplifyLikeLineariser.cs') 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() != null); - throw new NotImplementedException(); -} - + public override LineariserOptions SetAsTerm(bool newVal) { + Contract.Ensures(Contract.Result() != 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/*!*/ LetVariables { get {Contract.Ensures(cce.NonNullElements(Contract.Result>())); - return EmptyList; - } } + public virtual List/*!*/ LetVariables { + get { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + return EmptyList; + } + } - public virtual LineariserOptions AddLetVariable(VCExprVar furtherVar){ -Contract.Requires(furtherVar != null); -Contract.Ensures(Contract.Result() != null); + public virtual LineariserOptions AddLetVariable(VCExprVar furtherVar) { + Contract.Requires(furtherVar != null); + Contract.Ensures(Contract.Result() != null); return this; } - public virtual LineariserOptions AddLetVariables(List/*!*/ furtherVars){ -Contract.Requires(cce.NonNullElements(furtherVars)); -Contract.Ensures(Contract.Result() != null); + public virtual LineariserOptions AddLetVariables(List/*!*/ furtherVars) { + Contract.Requires(cce.NonNullElements(furtherVars)); + Contract.Ensures(Contract.Result() != null); return this; } - + private static readonly List/*!*/ EmptyList = new List(); [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() != null); + Contract.Ensures(Contract.Result() != null); if (newVal) return SimplifyDefaultTerm; else @@ -119,21 +143,21 @@ Contract.Ensures(Contract.Result() != null); // Lineariser for expressions. The result (bool) is currently not used for anything public class SimplifyLikeExprLineariser : IVCExprVisitor { - public static string ToSimplifyString(VCExpr e, UniqueNamer namer){ -Contract.Requires(namer != null); -Contract.Requires(e != null); -Contract.Ensures(Contract.Result() != null); + public static string ToSimplifyString(VCExpr e, UniqueNamer namer) { + Contract.Requires(namer != null); + Contract.Requires(e != null); + Contract.Ensures(Contract.Result() != 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() != 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() != 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/*!*/ OpLineariser { get {Contract.Ensures(Contract.Result>()!=null); - if (OpLinObject == null) - OpLinObject = new SimplifyLikeOpLineariser (this, wr); - return OpLinObject; - } } + private IVCExprOpVisitor/*!*/ OpLineariser { + get { + Contract.Ensures(Contract.Result>() != 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(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() != null); + public static string MakeIdPrintable(string s) { + Contract.Requires(s != null); + Contract.Ensures(Contract.Result() != 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() != 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, false)) { t.Emit(stream); @@ -276,8 +299,7 @@ Contract.Ensures(Contract.Result() != null); } - public static string TypeToString(Type t) - { + public static string TypeToString(Type t) { Contract.Requires(t != null); Contract.Ensures(Contract.Result() != null); @@ -294,39 +316,39 @@ Contract.Ensures(Contract.Result() != null); } } - public static string BvConcatOpName(VCExprNAry node){ -Contract.Requires(node != null); -Contract.Requires((node.Op is VCExprBvConcatOp)); -Contract.Ensures(Contract.Result() != null); + public static string BvConcatOpName(VCExprNAry node) { + Contract.Requires(node != null); + Contract.Requires((node.Op is VCExprBvConcatOp)); + Contract.Ensures(Contract.Result() != 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() != null); + public static string BvExtractOpName(VCExprNAry node) { + Contract.Requires(node != null); + Contract.Requires(node.Op is VCExprBvExtractOp); + Contract.Ensures(Contract.Result() != 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() != null); + public static string StoreOpName(VCExprNAry node) { + Contract.Requires(node != null); + Contract.Requires((node.Op is VCExprStoreOp)); + Contract.Ensures(Contract.Result() != 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() != null); + public static string SelectOpName(VCExprNAry node) { + Contract.Requires(node != null); + Contract.Requires((node.Op is VCExprSelectOp)); + Contract.Ensures(Contract.Result() != 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/*!*/ triggers, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(cce.NonNullElements(triggers)); + private void WriteTriggers(List/*!*/ 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/*!*/ args, LineariserOptions options, bool argsAsTerms){ -Contract.Requires(options != null); -Contract.Requires(op != null); -Contract.Requires(cce.NonNullElements(args)); + private void WriteApplication(string op, IEnumerable/*!*/ 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/*!*/ args,LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(op != null); -Contract.Requires(cce.NonNullElements(args)); + private void WriteApplication(string op, IEnumerable/*!*/ 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/*!*/ args,LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(op != null); -Contract.Requires(cce.NonNullElements(args)); + private void WriteTermApplication(string op, IEnumerable/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ args, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(termOp != null); -Contract.Requires(cce.NonNullElements(args)); + private void WriteApplicationTermOnly(string termOp, IEnumerable/*!*/ 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; } - + } } -- cgit v1.2.3