From 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 28 Jun 2015 01:44:30 +0100 Subject: Normalise line endings using a .gitattributes file. Unfortunately this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. --- Source/VCExpr/TermFormulaFlattening.cs | 494 ++++++++++++++++----------------- 1 file changed, 247 insertions(+), 247 deletions(-) (limited to 'Source/VCExpr/TermFormulaFlattening.cs') diff --git a/Source/VCExpr/TermFormulaFlattening.cs b/Source/VCExpr/TermFormulaFlattening.cs index 7815413f..c4150024 100644 --- a/Source/VCExpr/TermFormulaFlattening.cs +++ b/Source/VCExpr/TermFormulaFlattening.cs @@ -1,248 +1,248 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.Text; -using System.IO; -using System.Linq; -using System.Collections; -using System.Collections.Generic; -using System.Diagnostics.Contracts; -using Microsoft.Basetypes; -using Microsoft.Boogie.VCExprAST; - -// Ensure that no formulas (expressions of type boolean that are not -// just a variable) occur with terms (expressions of some other -// type). This is done by introducing let-binders for boolean -// variables. - -namespace Microsoft.Boogie.VCExprAST -{ - - public struct FlattenerState { - public readonly int Polarity; - public readonly bool InTerm; - - public static FlattenerState INITIAL = new FlattenerState(1, false); - - public FlattenerState(int polarity, bool inTerm) { - Polarity = polarity; - InTerm = inTerm; - } - - public FlattenerState TogglePolarity { get { - return new FlattenerState(-Polarity, InTerm); - } } - - public FlattenerState ZeroPolarity { get { - return new FlattenerState(0, InTerm); - } } - - public FlattenerState EnterTerm { get { - return new FlattenerState(Polarity, true); - } } - } - - ////////////////////////////////////////////////////////////////////////////// - - public class TermFormulaFlattener : MutatingVCExprVisitor { - - public TermFormulaFlattener(VCExpressionGenerator gen):base(gen){ -Contract.Requires(gen != null); - - } - - private readonly IDictionary/*!*/ Bindings = - new Dictionary (); - - private int varNameCounter = 0; - - public VCExpr Flatten(VCExpr expr){ -Contract.Requires(expr != null); -Contract.Ensures(Contract.Result() != null); - VCExpr/*!*/ res = Mutate(expr, FlattenerState.INITIAL); - Contract.Assert(res != null); - while (Bindings.Count > 0) { - List/*!*/ letBindings = new List (); - foreach (KeyValuePair pair in Bindings){Contract.Assert(cce.NonNullElements(pair)); - letBindings.Add(Gen.LetBinding(pair.Value, pair.Key));} - Bindings.Clear(); - res = AddBindings(letBindings, res, FlattenerState.INITIAL); - } - return res; - } - - private VCExprVar GetVarFor(VCExpr expr){ -Contract.Requires(expr != null); -Contract.Requires((expr.Type.IsBool)); -Contract.Ensures(Contract.Result() != null); - VCExprVar res; - if (!Bindings.TryGetValue(expr, out res)) { - string name = "flt" + varNameCounter; - varNameCounter = varNameCounter + 1; - res = Gen.Variable(name, Type.Bool); - Bindings.Add(expr, res); - } - return cce.NonNull(res); - } - - // Remove all let-bindings from the field bindings whose rhs - // contains any of the specified variables - private List/*!*/ RemoveBindingsWithVars(List/*!*/ boundVars, List/*!*/ boundTypeVars){ -Contract.Requires(cce.NonNullElements(boundTypeVars)); -Contract.Requires(cce.NonNullElements(boundVars)); -Contract.Ensures(cce.NonNullElements(Contract.Result>())); - List/*!*/ res = new List (); - FreeVariableCollector/*!*/ coll = new FreeVariableCollector (); - - foreach (KeyValuePair pair in Bindings) { - Contract.Assert(cce.NonNullElements(pair)); - coll.Collect(pair.Key); - if (boundVars.Any(var => coll.FreeTermVars.ContainsKey(var)) || - boundTypeVars.Any(var => coll.FreeTypeVars.Contains(var))) - res.Add(Gen.LetBinding(pair.Value, pair.Key)); - coll.Reset(); - } - - foreach (VCExprLetBinding b in res){Contract.Assert(b != null); - Bindings.Remove(b.E);} - - return res; - } - - // Add bindings to a formula using an implication or - // conjunction. The bindings themselves will be flattened as well, - // which might introduce further bindings - private VCExpr AddBindings(List/*!*/ bindings, VCExpr body, FlattenerState state){ -Contract.Requires(body != null); -Contract.Requires(cce.NonNullElements(bindings)); -Contract.Requires((body.Type.IsBool)); -Contract.Ensures(Contract.Result() != null); - - List/*!*/ mutatedBindings = FlattenBindings(bindings, state); - Contract.Assert(mutatedBindings != null); - VCExpr/*!*/ bindingEquations = Gen.AsEquations(mutatedBindings); - Contract.Assert(bindingEquations != null); - switch(state.Polarity) { - case 1: - return Gen.Implies(bindingEquations, body); - case -1: - return Gen.And(bindingEquations, body); - case 0: - // also add explicit quantifiers for the bound variables - List/*!*/ vars = new List (); - foreach (VCExprLetBinding/*!*/ binding in mutatedBindings){Contract.Assert(binding != null); - vars.Add(binding.V);} - return Gen.Forall(vars, new List(), - Gen.Implies(bindingEquations, body)); - } - Contract.Assert(false); throw new cce.UnreachableException(); - } - - private List/*!*/ FlattenBindings(List/*!*/ bindings, FlattenerState state){ -Contract.Requires(cce.NonNullElements(bindings)); -Contract.Ensures(cce.NonNullElements(Contract.Result>())); - FlattenerState stateInBindings = state.ZeroPolarity; - List/*!*/ mutatedBindings = new List (); - foreach (VCExprLetBinding/*!*/ b in bindings) { - Contract.Assert(b != null); - mutatedBindings.Add(Gen.LetBinding(b.V, Mutate(b.E, stateInBindings))); - } - return mutatedBindings; - } - - //////////////////////////////////////////////////////////////////////////// - - public override bool AvoidVisit(VCExprNAry node, FlattenerState arg) - { - return node.Op.Equals(VCExpressionGenerator.AndOp) || - node.Op.Equals(VCExpressionGenerator.OrOp); - } - - public override VCExpr Visit(VCExprNAry node, FlattenerState state){ -Contract.Requires(node != null); -Contract.Ensures(Contract.Result() != null); - // track the polarity to know whether implications or conjunctions - // are to be introduced - - if (node.Op.Equals(VCExpressionGenerator.NotOp)) - return Gen.Not(Mutate(node[0], state.TogglePolarity)); - - if (node.Op.Equals(VCExpressionGenerator.ImpliesOp)) { - VCExpr newArg0 = Mutate(node[0], state.TogglePolarity); - VCExpr newArg1 = Mutate(node[1], state); - return Gen.Implies(newArg0, newArg1); - } - - if (!node.Type.IsBool) - state = state.EnterTerm; - - if (!node.Op.Equals(VCExpressionGenerator.AndOp) && - !node.Op.Equals(VCExpressionGenerator.OrOp) && - !(node.Op is VCExprLabelOp)) - // standard is to set the polarity to 0 (fits most operators) - return base.Visit(node, state.ZeroPolarity); - - return base.Visit(node, state); - } - - public override VCExpr Visit(VCExprQuantifier node, FlattenerState state){ -Contract.Requires(node != null); -Contract.Ensures(Contract.Result() != null); - if (state.InTerm) - return GetVarFor(node); - - // we only flatten within the matrix of the quantified formula, - // not within the triggers (since SMT-solvers do not seem to - // appreciate triggers with let-binders) - VCExpr newBody = Mutate(node.Body, state); - - // Check whether any of the extracted terms contain variables - // bound by this quantifier. In this case, we have to add - // let-binders and remove the extracted terms - bool cont = true; - while (cont) { - List/*!*/ localBindings = - RemoveBindingsWithVars(node.BoundVars, node.TypeParameters); - Contract.Assert(cce.NonNullElements(localBindings)); - if (localBindings.Count > 0) - newBody = AddBindings(localBindings, newBody, state); - else - cont = false; - } - - return Gen.Quantify(node.Quan, node.TypeParameters, node.BoundVars, node.Triggers, node.Infos, newBody); - } - - public override VCExpr Visit(VCExprLet node, FlattenerState state){ -Contract.Requires(node != null); -Contract.Ensures(Contract.Result() != null); - if (state.InTerm) - return GetVarFor(node); - - VCExprLet prelimRes = (VCExprLet)cce.NonNull(base.Visit(node, state)); - - List/*!*/ allBindings = new List (); - allBindings.AddRange(prelimRes); - - // Check whether any of the extracted terms contain variables - // bound by this binder. In this case, we have to add - // let-binders and remove the extracted terms - bool cont = true; - while (cont) { - List/*!*/ localBindings = - RemoveBindingsWithVars(prelimRes.BoundVars, new List()); - if (localBindings.Count > 0) - allBindings.AddRange(FlattenBindings(localBindings, state)); - else - cont = false; - } - - return Gen.Let(allBindings, prelimRes.Body); - } - - } - +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Text; +using System.IO; +using System.Linq; +using System.Collections; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using Microsoft.Basetypes; +using Microsoft.Boogie.VCExprAST; + +// Ensure that no formulas (expressions of type boolean that are not +// just a variable) occur with terms (expressions of some other +// type). This is done by introducing let-binders for boolean +// variables. + +namespace Microsoft.Boogie.VCExprAST +{ + + public struct FlattenerState { + public readonly int Polarity; + public readonly bool InTerm; + + public static FlattenerState INITIAL = new FlattenerState(1, false); + + public FlattenerState(int polarity, bool inTerm) { + Polarity = polarity; + InTerm = inTerm; + } + + public FlattenerState TogglePolarity { get { + return new FlattenerState(-Polarity, InTerm); + } } + + public FlattenerState ZeroPolarity { get { + return new FlattenerState(0, InTerm); + } } + + public FlattenerState EnterTerm { get { + return new FlattenerState(Polarity, true); + } } + } + + ////////////////////////////////////////////////////////////////////////////// + + public class TermFormulaFlattener : MutatingVCExprVisitor { + + public TermFormulaFlattener(VCExpressionGenerator gen):base(gen){ +Contract.Requires(gen != null); + + } + + private readonly IDictionary/*!*/ Bindings = + new Dictionary (); + + private int varNameCounter = 0; + + public VCExpr Flatten(VCExpr expr){ +Contract.Requires(expr != null); +Contract.Ensures(Contract.Result() != null); + VCExpr/*!*/ res = Mutate(expr, FlattenerState.INITIAL); + Contract.Assert(res != null); + while (Bindings.Count > 0) { + List/*!*/ letBindings = new List (); + foreach (KeyValuePair pair in Bindings){Contract.Assert(cce.NonNullElements(pair)); + letBindings.Add(Gen.LetBinding(pair.Value, pair.Key));} + Bindings.Clear(); + res = AddBindings(letBindings, res, FlattenerState.INITIAL); + } + return res; + } + + private VCExprVar GetVarFor(VCExpr expr){ +Contract.Requires(expr != null); +Contract.Requires((expr.Type.IsBool)); +Contract.Ensures(Contract.Result() != null); + VCExprVar res; + if (!Bindings.TryGetValue(expr, out res)) { + string name = "flt" + varNameCounter; + varNameCounter = varNameCounter + 1; + res = Gen.Variable(name, Type.Bool); + Bindings.Add(expr, res); + } + return cce.NonNull(res); + } + + // Remove all let-bindings from the field bindings whose rhs + // contains any of the specified variables + private List/*!*/ RemoveBindingsWithVars(List/*!*/ boundVars, List/*!*/ boundTypeVars){ +Contract.Requires(cce.NonNullElements(boundTypeVars)); +Contract.Requires(cce.NonNullElements(boundVars)); +Contract.Ensures(cce.NonNullElements(Contract.Result>())); + List/*!*/ res = new List (); + FreeVariableCollector/*!*/ coll = new FreeVariableCollector (); + + foreach (KeyValuePair pair in Bindings) { + Contract.Assert(cce.NonNullElements(pair)); + coll.Collect(pair.Key); + if (boundVars.Any(var => coll.FreeTermVars.ContainsKey(var)) || + boundTypeVars.Any(var => coll.FreeTypeVars.Contains(var))) + res.Add(Gen.LetBinding(pair.Value, pair.Key)); + coll.Reset(); + } + + foreach (VCExprLetBinding b in res){Contract.Assert(b != null); + Bindings.Remove(b.E);} + + return res; + } + + // Add bindings to a formula using an implication or + // conjunction. The bindings themselves will be flattened as well, + // which might introduce further bindings + private VCExpr AddBindings(List/*!*/ bindings, VCExpr body, FlattenerState state){ +Contract.Requires(body != null); +Contract.Requires(cce.NonNullElements(bindings)); +Contract.Requires((body.Type.IsBool)); +Contract.Ensures(Contract.Result() != null); + + List/*!*/ mutatedBindings = FlattenBindings(bindings, state); + Contract.Assert(mutatedBindings != null); + VCExpr/*!*/ bindingEquations = Gen.AsEquations(mutatedBindings); + Contract.Assert(bindingEquations != null); + switch(state.Polarity) { + case 1: + return Gen.Implies(bindingEquations, body); + case -1: + return Gen.And(bindingEquations, body); + case 0: + // also add explicit quantifiers for the bound variables + List/*!*/ vars = new List (); + foreach (VCExprLetBinding/*!*/ binding in mutatedBindings){Contract.Assert(binding != null); + vars.Add(binding.V);} + return Gen.Forall(vars, new List(), + Gen.Implies(bindingEquations, body)); + } + Contract.Assert(false); throw new cce.UnreachableException(); + } + + private List/*!*/ FlattenBindings(List/*!*/ bindings, FlattenerState state){ +Contract.Requires(cce.NonNullElements(bindings)); +Contract.Ensures(cce.NonNullElements(Contract.Result>())); + FlattenerState stateInBindings = state.ZeroPolarity; + List/*!*/ mutatedBindings = new List (); + foreach (VCExprLetBinding/*!*/ b in bindings) { + Contract.Assert(b != null); + mutatedBindings.Add(Gen.LetBinding(b.V, Mutate(b.E, stateInBindings))); + } + return mutatedBindings; + } + + //////////////////////////////////////////////////////////////////////////// + + public override bool AvoidVisit(VCExprNAry node, FlattenerState arg) + { + return node.Op.Equals(VCExpressionGenerator.AndOp) || + node.Op.Equals(VCExpressionGenerator.OrOp); + } + + public override VCExpr Visit(VCExprNAry node, FlattenerState state){ +Contract.Requires(node != null); +Contract.Ensures(Contract.Result() != null); + // track the polarity to know whether implications or conjunctions + // are to be introduced + + if (node.Op.Equals(VCExpressionGenerator.NotOp)) + return Gen.Not(Mutate(node[0], state.TogglePolarity)); + + if (node.Op.Equals(VCExpressionGenerator.ImpliesOp)) { + VCExpr newArg0 = Mutate(node[0], state.TogglePolarity); + VCExpr newArg1 = Mutate(node[1], state); + return Gen.Implies(newArg0, newArg1); + } + + if (!node.Type.IsBool) + state = state.EnterTerm; + + if (!node.Op.Equals(VCExpressionGenerator.AndOp) && + !node.Op.Equals(VCExpressionGenerator.OrOp) && + !(node.Op is VCExprLabelOp)) + // standard is to set the polarity to 0 (fits most operators) + return base.Visit(node, state.ZeroPolarity); + + return base.Visit(node, state); + } + + public override VCExpr Visit(VCExprQuantifier node, FlattenerState state){ +Contract.Requires(node != null); +Contract.Ensures(Contract.Result() != null); + if (state.InTerm) + return GetVarFor(node); + + // we only flatten within the matrix of the quantified formula, + // not within the triggers (since SMT-solvers do not seem to + // appreciate triggers with let-binders) + VCExpr newBody = Mutate(node.Body, state); + + // Check whether any of the extracted terms contain variables + // bound by this quantifier. In this case, we have to add + // let-binders and remove the extracted terms + bool cont = true; + while (cont) { + List/*!*/ localBindings = + RemoveBindingsWithVars(node.BoundVars, node.TypeParameters); + Contract.Assert(cce.NonNullElements(localBindings)); + if (localBindings.Count > 0) + newBody = AddBindings(localBindings, newBody, state); + else + cont = false; + } + + return Gen.Quantify(node.Quan, node.TypeParameters, node.BoundVars, node.Triggers, node.Infos, newBody); + } + + public override VCExpr Visit(VCExprLet node, FlattenerState state){ +Contract.Requires(node != null); +Contract.Ensures(Contract.Result() != null); + if (state.InTerm) + return GetVarFor(node); + + VCExprLet prelimRes = (VCExprLet)cce.NonNull(base.Visit(node, state)); + + List/*!*/ allBindings = new List (); + allBindings.AddRange(prelimRes); + + // Check whether any of the extracted terms contain variables + // bound by this binder. In this case, we have to add + // let-binders and remove the extracted terms + bool cont = true; + while (cont) { + List/*!*/ localBindings = + RemoveBindingsWithVars(prelimRes.BoundVars, new List()); + if (localBindings.Count > 0) + allBindings.AddRange(FlattenBindings(localBindings, state)); + else + cont = false; + } + + return Gen.Let(allBindings, prelimRes.Body); + } + + } + } \ No newline at end of file -- cgit v1.2.3