diff options
Diffstat (limited to 'Source/VCGeneration/OrderingAxioms.cs')
-rw-r--r-- | Source/VCGeneration/OrderingAxioms.cs | 676 |
1 files changed, 338 insertions, 338 deletions
diff --git a/Source/VCGeneration/OrderingAxioms.cs b/Source/VCGeneration/OrderingAxioms.cs index dbb97764..9284601f 100644 --- a/Source/VCGeneration/OrderingAxioms.cs +++ b/Source/VCGeneration/OrderingAxioms.cs @@ -1,338 +1,338 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Collections.Generic;
-using System.IO;
-using System.Text;
-using System.Linq;
-using System.Diagnostics.Contracts;
-using Microsoft.Boogie.VCExprAST;
-
-// Class for constructing and collecting the axioms of the partial
-// order <:. The class also manages "unique" attributes of constants
-// and generated the necessary assumptions for the theorem prover.
-
-// TODO: there should be an interface so that different ways to handle
-// ordering relations can be accessed uniformly
-
-namespace Microsoft.Boogie {
-
- public class OrderingAxiomBuilder {
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(Gen != null);
- Contract.Invariant(Translator != null);
- Contract.Invariant(cce.NonNullDictionaryAndValues(OneStepFuns));
- Contract.Invariant(cce.NonNullElements(Constants));
- Contract.Invariant(cce.NonNullElements(CompleteConstantsOpen));
- Contract.Invariant(cce.NonNullElements(AllAxioms));
- Contract.Invariant(cce.NonNullElements(IncAxioms));
- }
-
-
- private readonly VCExpressionGenerator Gen;
- private readonly Boogie2VCExprTranslator Translator;
- private readonly IDictionary<Type, Function> OneStepFuns;
- private readonly List<Constant> Constants = new List<Constant>();
-
- // A list to handle constants whose direct children are fully
- // specified (the "complete" keyword). Constants are removed from
- // the list as soon as the corresponding axiom has been generated,
- // which means that from this point on no further children can be
- // added
- private readonly List<Constant> CompleteConstantsOpen = new List<Constant>();
-
- // list in which all axioms are collected
- private readonly List<VCExpr> AllAxioms = new List<VCExpr>();
-
- // list in which axioms are incrementally collected
- private readonly List<VCExpr> IncAxioms = new List<VCExpr>();
-
-
- public OrderingAxiomBuilder(VCExpressionGenerator gen,
- Boogie2VCExprTranslator translator) {
- Contract.Requires(gen != null);
- Contract.Requires(translator != null);
- this.Gen = gen;
- this.Translator = translator;
- OneStepFuns = new Dictionary<Type, Function>();
- Constants = new List<Constant>();
- CompleteConstantsOpen = new List<Constant>();
- AllAxioms = new List<VCExpr>();
- IncAxioms = new List<VCExpr>();
- }
-
- public OrderingAxiomBuilder(VCExpressionGenerator gen,
- Boogie2VCExprTranslator translator,
- OrderingAxiomBuilder builder) {
- Contract.Requires(gen != null);
- Contract.Requires(translator != null);
- Contract.Requires(builder != null);
- this.Gen = gen;
- this.Translator = translator;
- OneStepFuns = new Dictionary<Type, Function>(builder.OneStepFuns);
- Constants = new List<Constant>(builder.Constants);
- CompleteConstantsOpen = new List<Constant>(builder.CompleteConstantsOpen);
- AllAxioms = new List<VCExpr>(builder.AllAxioms);
- IncAxioms = new List<VCExpr>(builder.IncAxioms);
- }
-
- ////////////////////////////////////////////////////////////////////////////
-
- // Used to axiomatise the disjoint-sub-dag specs that are
- // described by parents with the "unique" flag
-
-
- private Function OneStepFunFor(Type t) {
- Contract.Requires(t != null);
- Contract.Ensures(Contract.Result<Function>() != null);
-
- Function res;
- if (!OneStepFuns.TryGetValue(t, out res)) {
- List<Variable> args = new List<Variable>();
- args.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "arg0", t), true));
- args.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "arg1", t), true));
- Formal result = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "res", t), false);
- res = new Function(Token.NoToken, "oneStep", new List<TypeVariable>(), args, result);
- OneStepFuns.Add(t, res);
- }
- return cce.NonNull(res);
- }
-
- ////////////////////////////////////////////////////////////////////////////
-
-
- private void AddAxiom(VCExpr axiom) {
- Contract.Requires(axiom != null);
- if (axiom.Equals(VCExpressionGenerator.True))
- return;
- AllAxioms.Add(axiom);
- IncAxioms.Add(axiom);
- }
-
- // Return all axioms that were added since the last time NewAxioms
- // was called
- public VCExpr GetNewAxioms() {
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- CloseChildrenCompleteConstants();
- VCExpr res = Gen.NAry(VCExpressionGenerator.AndOp, IncAxioms);
- IncAxioms.Clear();
- return res;
- }
-
- // return all axioms
- public VCExpr Axioms {
- get {
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- CloseChildrenCompleteConstants();
- return Gen.NAry(VCExpressionGenerator.AndOp, AllAxioms);
- }
- }
-
- ////////////////////////////////////////////////////////////////////////////
-
- // Generate the normal axioms for a partial order relation
- public void Setup() {
- TypeVariable alpha = new TypeVariable(Token.NoToken, "alpha");
- Contract.Assert(alpha != null);
- List<TypeVariable> typeParams = new List<TypeVariable>();
- typeParams.Add(alpha);
-
- List<VCTrigger> triggers = new List<VCTrigger>();
-
- VCExprVar x = Gen.Variable("x", alpha);
- Contract.Assert(x != null);
- VCExprVar y = Gen.Variable("y", alpha);
- Contract.Assert(y != null);
- VCExprVar z = Gen.Variable("z", alpha);
- Contract.Assert(z != null);
-
- List<VCExprVar> boundVars = new List<VCExprVar>();
-
- // reflexivity
- boundVars.Add(x);
- AddAxiom(Gen.Forall(typeParams, boundVars, triggers,
- new VCQuantifierInfos("bg:subtype-refl", -1, false, null),
- Gen.AtMost(x, x)));
-
- // transitivity
- boundVars = new List<VCExprVar>();
- boundVars.Add(x);
- boundVars.Add(y);
- boundVars.Add(z);
- triggers = new List<VCTrigger>();
- triggers.Add(Gen.Trigger(true, Gen.AtMost(x, y), Gen.AtMost(y, z)));
- VCExpr body = Gen.Implies(Gen.And(Gen.AtMost(x, y), Gen.AtMost(y, z)),
- Gen.AtMost(x, z));
- Contract.Assert(body != null);
- AddAxiom(Gen.Forall(typeParams, boundVars, triggers,
- new VCQuantifierInfos("bg:subtype-trans", -1, false, null),
- body));
-
- // anti-symmetry
- boundVars = new List<VCExprVar>();
- boundVars.Add(x);
- boundVars.Add(y);
- triggers = new List<VCTrigger>();
- triggers.Add(Gen.Trigger(true, Gen.AtMost(x, y), Gen.AtMost(y, x)));
- body = Gen.Implies(Gen.And(Gen.AtMost(x, y), Gen.AtMost(y, x)),
- Gen.Eq(x, y));
- AddAxiom(Gen.Forall(typeParams, boundVars, triggers,
- new VCQuantifierInfos("bg:subtype-antisymm", -1, false, null),
- body));
- }
-
- ////////////////////////////////////////////////////////////////////////////
-
- public void AddConstant(Constant c) {
- Contract.Requires(c != null);
- AddAxiom(GenParentConstraints(c));
- Constants.Add(c);
- if (c.ChildrenComplete)
- CompleteConstantsOpen.Add(c);
-
- // ensure that no further children are added to closed
- // children-complete constants
- Contract.Assert(!(c.Parents != null && Contract.Exists(c.Parents, p => cce.NonNull((Constant)p.Parent.Decl).ChildrenComplete && !CompleteConstantsOpen.Contains((Constant)p.Parent.Decl))));
- }
-
- // Generate the constraints telling that parents of a constant are
- // strictly greater than the constant itself, and are the minimal
- // elements with this property
- private VCExpr GenParentConstraints(Constant c) {
- Contract.Requires(c != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- VCExpr res = VCExpressionGenerator.True;
-
- if (c.Parents == null)
- return res;
-
- VCExprVar cAsVar = Translator.LookupVariable(c);
- VCExprVar w = Gen.Variable("w", c.TypedIdent.Type);
-
- // Parents of c are proper ancestors of c
- foreach (ConstantParent p in c.Parents) {
- Contract.Assert(p != null);
- VCExprVar par = Translator.LookupVariable(cce.NonNull(p.Parent.Decl));
- res = Gen.AndSimp(res, Gen.Neq(cAsVar, par));
- res = Gen.AndSimp(res, Gen.AtMost(cAsVar, par));
- }
-
- // Parents are direct ancestors of c (no other elements are in
- // between c and a parent)
- foreach (ConstantParent p in c.Parents) {
- Contract.Assert(p != null);
- VCExprVar par = Translator.LookupVariable(cce.NonNull(p.Parent.Decl));
- Contract.Assert(par != null);
- VCExpr antecedent1 = Gen.AtMost(cAsVar, w);
- Contract.Assert(antecedent1 != null);
- VCExpr antecedent2 = Gen.AtMost(w, par);
- Contract.Assert(antecedent2 != null);
- VCExpr body = Gen.Implies(Gen.And(antecedent1, antecedent2),
- Gen.Or(Gen.Eq(cAsVar, w), Gen.Eq(par, w)));
- Contract.Assert(body != null);
- res = Gen.AndSimp(res,
- Gen.Forall(w,
- Gen.Trigger(true, antecedent1, antecedent2),
- body));
- }
-
- // Ancestors of c are only c itself and the ancestors of the
- // parents of c
- VCExpr minAncestors = Gen.Eq(cAsVar, w);
- Contract.Assert(minAncestors != null);
- foreach (ConstantParent p in c.Parents) {
- Contract.Assert(p != null);
- minAncestors =
- Gen.Or(minAncestors,
- Gen.AtMost(Translator.LookupVariable(cce.NonNull(p.Parent.Decl)), w));
- }
- VCExpr antecedent = Gen.AtMost(cAsVar, w);
- Contract.Assert(antecedent != null);
- res = Gen.AndSimp(res,
- Gen.Forall(w,
- Gen.Trigger(true, antecedent),
- Gen.Implies(antecedent, minAncestors)));
-
- // Constraints for unique child-parent edges
- foreach (ConstantParent p in c.Parents) {
- Contract.Assert(p != null);
- if (p.Unique)
- res =
- Gen.AndSimp(res,
- GenUniqueParentConstraint(c, cce.NonNull((Constant)p.Parent.Decl)));
- }
-
- return res;
- }
-
- // Generate axioms that state that all direct children of c are
- // specified; this is the dual of the axiom stating that all direct
- // ancestors of a constant are known
- private VCExpr GenCompleteChildrenConstraints(Constant c) {
- Contract.Requires(c != null);
- Contract.Requires(c.ChildrenComplete);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
-
- VCExprVar cAsVar = Translator.LookupVariable(c);
- VCExprVar w = Gen.Variable("w", c.TypedIdent.Type);
-
- VCExpr maxDescendants = Gen.Eq(cAsVar, w);
- foreach (Constant d in Constants) {
- Contract.Assert(d != null);
- if (d.Parents != null && d.Parents.Any(p => c.Equals(p.Parent.Decl)))
- maxDescendants = Gen.Or(maxDescendants,
- Gen.AtMost(w, Translator.LookupVariable(d)));
- }
-
- VCExpr antecedent = Gen.AtMost(w, cAsVar);
- Contract.Assert(antecedent != null);
- return Gen.Forall(w,
- Gen.Trigger(true, antecedent),
- Gen.Implies(antecedent, maxDescendants));
- }
-
- private void CloseChildrenCompleteConstants() {
- foreach (Constant c in CompleteConstantsOpen) {
- Contract.Assert(c != null);
- AddAxiom(GenCompleteChildrenConstraints(c));
- }
- CompleteConstantsOpen.Clear();
- }
-
- // Generate the axiom ensuring that the sub-dags underneath unique
- // child-parent edges are all disjoint
- private VCExpr GenUniqueParentConstraint(Constant child, Constant parent) {
- Contract.Requires(child != null);
- Contract.Requires(parent != null);
- Contract.Requires(child.TypedIdent.Type.Equals(parent.TypedIdent.Type));
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
-
-
- VCExprVar w = Gen.Variable("w", child.TypedIdent.Type);
- Contract.Assert(w != null);
- VCExpr antecedent =
- Gen.AtMost(w, Translator.LookupVariable(child));
- Contract.Assert(antecedent != null);
- VCExpr succedent =
- Gen.Eq(Gen.Function(OneStepFunFor(child.TypedIdent.Type),
- Translator.LookupVariable(parent), w),
- Translator.LookupVariable(child));
- Contract.Assert(succedent != null);
-
- return Gen.Forall(w,
- Gen.Trigger(true, antecedent),
- Gen.Implies(antecedent, succedent));
- }
-
- }
-
-}
+//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Collections.Generic; +using System.IO; +using System.Text; +using System.Linq; +using System.Diagnostics.Contracts; +using Microsoft.Boogie.VCExprAST; + +// Class for constructing and collecting the axioms of the partial +// order <:. The class also manages "unique" attributes of constants +// and generated the necessary assumptions for the theorem prover. + +// TODO: there should be an interface so that different ways to handle +// ordering relations can be accessed uniformly + +namespace Microsoft.Boogie { + + public class OrderingAxiomBuilder { + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Gen != null); + Contract.Invariant(Translator != null); + Contract.Invariant(cce.NonNullDictionaryAndValues(OneStepFuns)); + Contract.Invariant(cce.NonNullElements(Constants)); + Contract.Invariant(cce.NonNullElements(CompleteConstantsOpen)); + Contract.Invariant(cce.NonNullElements(AllAxioms)); + Contract.Invariant(cce.NonNullElements(IncAxioms)); + } + + + private readonly VCExpressionGenerator Gen; + private readonly Boogie2VCExprTranslator Translator; + private readonly IDictionary<Type, Function> OneStepFuns; + private readonly List<Constant> Constants = new List<Constant>(); + + // A list to handle constants whose direct children are fully + // specified (the "complete" keyword). Constants are removed from + // the list as soon as the corresponding axiom has been generated, + // which means that from this point on no further children can be + // added + private readonly List<Constant> CompleteConstantsOpen = new List<Constant>(); + + // list in which all axioms are collected + private readonly List<VCExpr> AllAxioms = new List<VCExpr>(); + + // list in which axioms are incrementally collected + private readonly List<VCExpr> IncAxioms = new List<VCExpr>(); + + + public OrderingAxiomBuilder(VCExpressionGenerator gen, + Boogie2VCExprTranslator translator) { + Contract.Requires(gen != null); + Contract.Requires(translator != null); + this.Gen = gen; + this.Translator = translator; + OneStepFuns = new Dictionary<Type, Function>(); + Constants = new List<Constant>(); + CompleteConstantsOpen = new List<Constant>(); + AllAxioms = new List<VCExpr>(); + IncAxioms = new List<VCExpr>(); + } + + public OrderingAxiomBuilder(VCExpressionGenerator gen, + Boogie2VCExprTranslator translator, + OrderingAxiomBuilder builder) { + Contract.Requires(gen != null); + Contract.Requires(translator != null); + Contract.Requires(builder != null); + this.Gen = gen; + this.Translator = translator; + OneStepFuns = new Dictionary<Type, Function>(builder.OneStepFuns); + Constants = new List<Constant>(builder.Constants); + CompleteConstantsOpen = new List<Constant>(builder.CompleteConstantsOpen); + AllAxioms = new List<VCExpr>(builder.AllAxioms); + IncAxioms = new List<VCExpr>(builder.IncAxioms); + } + + //////////////////////////////////////////////////////////////////////////// + + // Used to axiomatise the disjoint-sub-dag specs that are + // described by parents with the "unique" flag + + + private Function OneStepFunFor(Type t) { + Contract.Requires(t != null); + Contract.Ensures(Contract.Result<Function>() != null); + + Function res; + if (!OneStepFuns.TryGetValue(t, out res)) { + List<Variable> args = new List<Variable>(); + args.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "arg0", t), true)); + args.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "arg1", t), true)); + Formal result = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "res", t), false); + res = new Function(Token.NoToken, "oneStep", new List<TypeVariable>(), args, result); + OneStepFuns.Add(t, res); + } + return cce.NonNull(res); + } + + //////////////////////////////////////////////////////////////////////////// + + + private void AddAxiom(VCExpr axiom) { + Contract.Requires(axiom != null); + if (axiom.Equals(VCExpressionGenerator.True)) + return; + AllAxioms.Add(axiom); + IncAxioms.Add(axiom); + } + + // Return all axioms that were added since the last time NewAxioms + // was called + public VCExpr GetNewAxioms() { + Contract.Ensures(Contract.Result<VCExpr>() != null); + + CloseChildrenCompleteConstants(); + VCExpr res = Gen.NAry(VCExpressionGenerator.AndOp, IncAxioms); + IncAxioms.Clear(); + return res; + } + + // return all axioms + public VCExpr Axioms { + get { + Contract.Ensures(Contract.Result<VCExpr>() != null); + + CloseChildrenCompleteConstants(); + return Gen.NAry(VCExpressionGenerator.AndOp, AllAxioms); + } + } + + //////////////////////////////////////////////////////////////////////////// + + // Generate the normal axioms for a partial order relation + public void Setup() { + TypeVariable alpha = new TypeVariable(Token.NoToken, "alpha"); + Contract.Assert(alpha != null); + List<TypeVariable> typeParams = new List<TypeVariable>(); + typeParams.Add(alpha); + + List<VCTrigger> triggers = new List<VCTrigger>(); + + VCExprVar x = Gen.Variable("x", alpha); + Contract.Assert(x != null); + VCExprVar y = Gen.Variable("y", alpha); + Contract.Assert(y != null); + VCExprVar z = Gen.Variable("z", alpha); + Contract.Assert(z != null); + + List<VCExprVar> boundVars = new List<VCExprVar>(); + + // reflexivity + boundVars.Add(x); + AddAxiom(Gen.Forall(typeParams, boundVars, triggers, + new VCQuantifierInfos("bg:subtype-refl", -1, false, null), + Gen.AtMost(x, x))); + + // transitivity + boundVars = new List<VCExprVar>(); + boundVars.Add(x); + boundVars.Add(y); + boundVars.Add(z); + triggers = new List<VCTrigger>(); + triggers.Add(Gen.Trigger(true, Gen.AtMost(x, y), Gen.AtMost(y, z))); + VCExpr body = Gen.Implies(Gen.And(Gen.AtMost(x, y), Gen.AtMost(y, z)), + Gen.AtMost(x, z)); + Contract.Assert(body != null); + AddAxiom(Gen.Forall(typeParams, boundVars, triggers, + new VCQuantifierInfos("bg:subtype-trans", -1, false, null), + body)); + + // anti-symmetry + boundVars = new List<VCExprVar>(); + boundVars.Add(x); + boundVars.Add(y); + triggers = new List<VCTrigger>(); + triggers.Add(Gen.Trigger(true, Gen.AtMost(x, y), Gen.AtMost(y, x))); + body = Gen.Implies(Gen.And(Gen.AtMost(x, y), Gen.AtMost(y, x)), + Gen.Eq(x, y)); + AddAxiom(Gen.Forall(typeParams, boundVars, triggers, + new VCQuantifierInfos("bg:subtype-antisymm", -1, false, null), + body)); + } + + //////////////////////////////////////////////////////////////////////////// + + public void AddConstant(Constant c) { + Contract.Requires(c != null); + AddAxiom(GenParentConstraints(c)); + Constants.Add(c); + if (c.ChildrenComplete) + CompleteConstantsOpen.Add(c); + + // ensure that no further children are added to closed + // children-complete constants + Contract.Assert(!(c.Parents != null && Contract.Exists(c.Parents, p => cce.NonNull((Constant)p.Parent.Decl).ChildrenComplete && !CompleteConstantsOpen.Contains((Constant)p.Parent.Decl)))); + } + + // Generate the constraints telling that parents of a constant are + // strictly greater than the constant itself, and are the minimal + // elements with this property + private VCExpr GenParentConstraints(Constant c) { + Contract.Requires(c != null); + Contract.Ensures(Contract.Result<VCExpr>() != null); + + VCExpr res = VCExpressionGenerator.True; + + if (c.Parents == null) + return res; + + VCExprVar cAsVar = Translator.LookupVariable(c); + VCExprVar w = Gen.Variable("w", c.TypedIdent.Type); + + // Parents of c are proper ancestors of c + foreach (ConstantParent p in c.Parents) { + Contract.Assert(p != null); + VCExprVar par = Translator.LookupVariable(cce.NonNull(p.Parent.Decl)); + res = Gen.AndSimp(res, Gen.Neq(cAsVar, par)); + res = Gen.AndSimp(res, Gen.AtMost(cAsVar, par)); + } + + // Parents are direct ancestors of c (no other elements are in + // between c and a parent) + foreach (ConstantParent p in c.Parents) { + Contract.Assert(p != null); + VCExprVar par = Translator.LookupVariable(cce.NonNull(p.Parent.Decl)); + Contract.Assert(par != null); + VCExpr antecedent1 = Gen.AtMost(cAsVar, w); + Contract.Assert(antecedent1 != null); + VCExpr antecedent2 = Gen.AtMost(w, par); + Contract.Assert(antecedent2 != null); + VCExpr body = Gen.Implies(Gen.And(antecedent1, antecedent2), + Gen.Or(Gen.Eq(cAsVar, w), Gen.Eq(par, w))); + Contract.Assert(body != null); + res = Gen.AndSimp(res, + Gen.Forall(w, + Gen.Trigger(true, antecedent1, antecedent2), + body)); + } + + // Ancestors of c are only c itself and the ancestors of the + // parents of c + VCExpr minAncestors = Gen.Eq(cAsVar, w); + Contract.Assert(minAncestors != null); + foreach (ConstantParent p in c.Parents) { + Contract.Assert(p != null); + minAncestors = + Gen.Or(minAncestors, + Gen.AtMost(Translator.LookupVariable(cce.NonNull(p.Parent.Decl)), w)); + } + VCExpr antecedent = Gen.AtMost(cAsVar, w); + Contract.Assert(antecedent != null); + res = Gen.AndSimp(res, + Gen.Forall(w, + Gen.Trigger(true, antecedent), + Gen.Implies(antecedent, minAncestors))); + + // Constraints for unique child-parent edges + foreach (ConstantParent p in c.Parents) { + Contract.Assert(p != null); + if (p.Unique) + res = + Gen.AndSimp(res, + GenUniqueParentConstraint(c, cce.NonNull((Constant)p.Parent.Decl))); + } + + return res; + } + + // Generate axioms that state that all direct children of c are + // specified; this is the dual of the axiom stating that all direct + // ancestors of a constant are known + private VCExpr GenCompleteChildrenConstraints(Constant c) { + Contract.Requires(c != null); + Contract.Requires(c.ChildrenComplete); + Contract.Ensures(Contract.Result<VCExpr>() != null); + + + VCExprVar cAsVar = Translator.LookupVariable(c); + VCExprVar w = Gen.Variable("w", c.TypedIdent.Type); + + VCExpr maxDescendants = Gen.Eq(cAsVar, w); + foreach (Constant d in Constants) { + Contract.Assert(d != null); + if (d.Parents != null && d.Parents.Any(p => c.Equals(p.Parent.Decl))) + maxDescendants = Gen.Or(maxDescendants, + Gen.AtMost(w, Translator.LookupVariable(d))); + } + + VCExpr antecedent = Gen.AtMost(w, cAsVar); + Contract.Assert(antecedent != null); + return Gen.Forall(w, + Gen.Trigger(true, antecedent), + Gen.Implies(antecedent, maxDescendants)); + } + + private void CloseChildrenCompleteConstants() { + foreach (Constant c in CompleteConstantsOpen) { + Contract.Assert(c != null); + AddAxiom(GenCompleteChildrenConstraints(c)); + } + CompleteConstantsOpen.Clear(); + } + + // Generate the axiom ensuring that the sub-dags underneath unique + // child-parent edges are all disjoint + private VCExpr GenUniqueParentConstraint(Constant child, Constant parent) { + Contract.Requires(child != null); + Contract.Requires(parent != null); + Contract.Requires(child.TypedIdent.Type.Equals(parent.TypedIdent.Type)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + + + + VCExprVar w = Gen.Variable("w", child.TypedIdent.Type); + Contract.Assert(w != null); + VCExpr antecedent = + Gen.AtMost(w, Translator.LookupVariable(child)); + Contract.Assert(antecedent != null); + VCExpr succedent = + Gen.Eq(Gen.Function(OneStepFunFor(child.TypedIdent.Type), + Translator.LookupVariable(parent), w), + Translator.LookupVariable(child)); + Contract.Assert(succedent != null); + + return Gen.Forall(w, + Gen.Trigger(true, antecedent), + Gen.Implies(antecedent, succedent)); + } + + } + +} |