Boogie: Renaming VCExpr sources in preparation for port commit

1 files changed, 626 insertions, 0 deletions

diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs
new file mode 100644
index 00000000..ec03d2e8
--- /dev/null
+++ b/Source/VCExpr/TypeErasureArguments.cs
@@ -0,0 +1,626 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+using System;

+using System.Text;

+using System.IO;

+using System.Collections;

+using System.Collections.Generic;

+using Microsoft.Contracts;

+using Microsoft.Basetypes;

+using Microsoft.Boogie.VCExprAST;

+

+// Erasure of types using explicit type parameters for functions

+

+namespace Microsoft.Boogie.TypeErasure

+{

+  using Microsoft.Boogie.VCExprAST;

+  using HFNS = Microsoft.Boogie.VCExprAST.HelperFuns;

+

+  public class TypeAxiomBuilderArguments : TypeAxiomBuilderIntBoolU {

+

+    public TypeAxiomBuilderArguments(VCExpressionGenerator! gen) {

+      base(gen);

+      Typed2UntypedFunctions = new Dictionary<Function!, Function!> ();

+    }    

+

+    // constructor to allow cloning

+    [NotDelayed]

+    internal TypeAxiomBuilderArguments(TypeAxiomBuilderArguments! builder) {

+      Typed2UntypedFunctions =

+        new Dictionary<Function!, Function!> (builder.Typed2UntypedFunctions);

+      base(builder);

+

+      MapTypeAbstracterAttr =

+        builder.MapTypeAbstracterAttr == null ?

+        null : new MapTypeAbstractionBuilderArguments(this, builder.Gen,

+                                                      builder.MapTypeAbstracterAttr);

+    }

+

+    public override Object! Clone() {

+      return new TypeAxiomBuilderArguments(this);

+    }

+

+    ///////////////////////////////////////////////////////////////////////////////    

+

+    // generate axioms of the kind "forall x:U. {Int2U(U2Int(x))} Int2U(U2Int(x))==x"

+    // (this makes use of the assumption that only well-typed terms are generated

+    // by the SMT-solver, i.e., that U2Int is only applied to terms that actually

+    // are of type int)

+    protected override VCExpr! GenReverseCastAxiom(Function! castToU,

+                                                   Function! castFromU) {

+      List<VCTrigger!>! triggers;

+      VCExprVar! var;

+      VCExpr! eq = GenReverseCastEq(castToU, castFromU, out var, out triggers);

+      return Gen.Forall(HelperFuns.ToList(var), triggers, "cast:" + castFromU.Name, eq);

+    }

+

+    protected override VCExpr! GenCastTypeAxioms(Function! castToU,

+                                                 Function! castFromU) {

+      // nothing

+      return VCExpressionGenerator.True;

+    }

+

+    private MapTypeAbstractionBuilderArguments MapTypeAbstracterAttr = null;

+

+    internal override MapTypeAbstractionBuilder! MapTypeAbstracter { get {

+      if (MapTypeAbstracterAttr == null)

+        MapTypeAbstracterAttr = new MapTypeAbstractionBuilderArguments (this, Gen);

+      return MapTypeAbstracterAttr;

+    } }

+

+    protected override void AddVarTypeAxiom(VCExprVar! var, Type! originalType) {

+      // no axioms are needed for variable or function types

+    }

+

+    ////////////////////////////////////////////////////////////////////////////

+    // Symbols for representing functions

+

+    // Globally defined functions

+    private readonly IDictionary<Function!, Function!>! Typed2UntypedFunctions;

+

+    public Function! Typed2Untyped(Function! fun) {

+      Function res;

+      if (!Typed2UntypedFunctions.TryGetValue(fun, out res)) {

+        assert fun.OutParams.Length == 1;

+

+        // if all of the parameters are int or bool, the function does

+        // not have to be changed

+        if (forall{Formal f in fun.InParams; UnchangedType(((!)f).TypedIdent.Type)} &&

+            UnchangedType(((!)fun.OutParams[0]).TypedIdent.Type)) {

+          res = fun;

+        } else {

+          Type[]! types = new Type [fun.TypeParameters.Length + fun.InParams.Length + 1];

+

+          int i = 0;

+          // the first arguments are the explicit type parameters

+          for (int j = 0; j < fun.TypeParameters.Length; ++j) {

+            types[i] = T;

+            i = i + 1;

+          }

+          // followed by the actual parameters

+          foreach (Variable! x in fun.InParams) {

+            types[i] = TypeAfterErasure(x.TypedIdent.Type);

+            i = i + 1;

+          }

+

+          types[types.Length - 1] = TypeAfterErasure(((!)fun.OutParams[0]).TypedIdent.Type);

+

+          res = HelperFuns.BoogieFunction(fun.Name, types);

+          res.Attributes = fun.Attributes;

+        }

+

+        Typed2UntypedFunctions.Add(fun, res);

+      }

+      return (!)res;

+    }

+

+  }

+

+  //////////////////////////////////////////////////////////////////////////////

+

+  internal class MapTypeAbstractionBuilderArguments : MapTypeAbstractionBuilder {

+

+    private readonly TypeAxiomBuilderArguments! AxBuilderArguments;

+

+    internal MapTypeAbstractionBuilderArguments(TypeAxiomBuilderArguments! axBuilder,

+                                                VCExpressionGenerator! gen) {

+      base(axBuilder, gen);

+      this.AxBuilderArguments = axBuilder;

+    }

+

+    // constructor for cloning

+    internal MapTypeAbstractionBuilderArguments(TypeAxiomBuilderArguments! axBuilder,

+                                                VCExpressionGenerator! gen,

+                                                MapTypeAbstractionBuilderArguments! builder) {

+      base(axBuilder, gen, builder);

+      this.AxBuilderArguments = axBuilder;

+    }

+

+    ////////////////////////////////////////////////////////////////////////////

+

+    protected override void GenSelectStoreFunctions(MapType! abstractedType,

+                                                    TypeCtorDecl! synonym,

+                                                    out Function! select,

+                                                    out Function! store) {

+      string! baseName = synonym.Name;

+      int typeParamNum = abstractedType.FreeVariables.Length +

+                         abstractedType.TypeParameters.Length;

+      

+      int arity = typeParamNum + abstractedType.Arguments.Length;

+

+      Type![]! selectTypes = new Type! [arity + 2];

+      Type![]! storeTypes = new Type! [arity + 3];

+      

+      int i = 0;

+      // Fill in the free variables and type parameters

+      for (; i < typeParamNum; i++) {

+        selectTypes[i] = AxBuilder.T;

+        storeTypes[i] = AxBuilder.T;

+      }

+      // Fill in the map type

+      if (CommandLineOptions.Clo.UseArrayTheory) {

+        selectTypes[i] = abstractedType;

+        storeTypes[i] = abstractedType;

+      } else {

+        selectTypes[i] = AxBuilder.U;

+        storeTypes[i] = AxBuilder.U;

+      }

+      i++;

+      // Fill in the index types

+      foreach (Type! type in abstractedType.Arguments)

+      {

+        if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(type)) {

+          selectTypes[i] = type;

+          storeTypes[i] = type;

+        } else {

+          selectTypes[i] = AxBuilder.U;

+          storeTypes[i] = AxBuilder.U;

+        }

+        i++;

+      }

+      // Fill in the output type for select function which also happens 

+      // to be the type of the last argument to the store function

+      if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(abstractedType.Result)) {

+        selectTypes[i] = abstractedType.Result;

+        storeTypes[i] = abstractedType.Result;

+      } else {

+        selectTypes[i] = AxBuilder.U;

+        storeTypes[i] = AxBuilder.U;

+      }

+      i++;

+      // Fill in the map type which is the output of the store function

+      if (CommandLineOptions.Clo.UseArrayTheory) 

+        storeTypes[i] = abstractedType;

+      else

+        storeTypes[i] = AxBuilder.U;

+      NonNullType.AssertInitialized(selectTypes);

+      NonNullType.AssertInitialized(storeTypes);

+      

+      select = HelperFuns.BoogieFunction(baseName + "Select", selectTypes);
+      store = HelperFuns.BoogieFunction(baseName + "Store", storeTypes);

+      

+      if (CommandLineOptions.Clo.UseArrayTheory) {

+        select.AddAttribute("builtin", "select");

+        store.AddAttribute("builtin", "store");

+      } else {

+        AxBuilder.AddTypeAxiom(GenMapAxiom0(select, store, 

+                 abstractedType.TypeParameters.Length, abstractedType.FreeVariables.Length));

+        AxBuilder.AddTypeAxiom(GenMapAxiom1(select, store, 

+                 abstractedType.TypeParameters.Length, abstractedType.FreeVariables.Length));

+      }

+    }

+

+    ///////////////////////////////////////////////////////////////////////////

+    // The normal axioms of the theory of arrays (right now without extensionality)

+

+    private VCExpr! Select(Function! select, List<VCExprVar!>! types,

+                           VCExpr! map, List<VCExprVar!>! indexes) {

+      List<VCExpr!>! selectArgs = new List<VCExpr!> ();

+      selectArgs.AddRange(HelperFuns.ToVCExprList(types));

+      selectArgs.Add(map);

+      selectArgs.AddRange(HelperFuns.ToVCExprList(indexes));

+      return Gen.Function(select, selectArgs);

+    }

+

+    private VCExpr! Store(Function! store, List<VCExprVar!>! types,

+                          VCExpr! map, List<VCExprVar!>! indexes, VCExpr! val) {

+      List<VCExpr!>! storeArgs = new List<VCExpr!> ();

+      storeArgs.AddRange(HelperFuns.ToVCExprList(types));

+      storeArgs.Add(map);

+      storeArgs.AddRange(HelperFuns.ToVCExprList(indexes));

+      storeArgs.Add(val);

+      return Gen.Function(store, storeArgs);

+    }

+

+    private VCExpr! GenMapAxiom0(Function! select, Function! store,

+                                 // bound type variables in the map type

+                                 int mapTypeParamNum,

+                                 // free type variables in the map

+                                 // type (abstraction)

+                                 int mapAbstractionVarNum) {

+      int arity = select.InParams.Length - 1 - mapTypeParamNum - mapAbstractionVarNum;

+      List<VCExprVar!>! types =

+        HelperFuns.VarVector("t", mapTypeParamNum + mapAbstractionVarNum,

+                             AxBuilder.T, Gen);

+                             

+      List<Type!> indexTypes = new List<Type!>();

+      for (int i = mapTypeParamNum + mapAbstractionVarNum + 1; i < select.InParams.Length; i++)

+      {

+        indexTypes.Add(((!)select.InParams[i]).TypedIdent.Type);

+      }

+      assert arity == indexTypes.Count;

+      

+      List<VCExprVar!>! indexes = HelperFuns.VarVector("x", indexTypes, Gen);

+

+      VCExprVar! m = Gen.Variable("m", AxBuilder.U);

+      VCExprVar! val = Gen.Variable("val", ((!)select.OutParams[0]).TypedIdent.Type);

+

+      VCExpr! storeExpr = Store(store, types, m, indexes, val);

+      VCExpr! selectExpr = Select(select, types, storeExpr, indexes);

+

+      List<VCExprVar!>! quantifiedVars = new List<VCExprVar!> ();

+      quantifiedVars.AddRange(types);

+      quantifiedVars.Add(val);

+      quantifiedVars.Add(m);

+      quantifiedVars.AddRange(indexes);

+

+      VCExpr! eq = Gen.Eq(selectExpr, val);

+      return Gen.Forall(quantifiedVars, new List<VCTrigger!> (),

+                        "mapAx0:" + select.Name, eq);

+    }    

+

+    private VCExpr! GenMapAxiom1(Function! select, Function! store, 

+                                 // bound type variables in the map

+                                 // type

+                                 int mapTypeParamNum,

+                                 // free type variables in the map

+                                 // type (abstraction)

+                                 int mapAbstractionVarNum) {

+      int arity = select.InParams.Length - 1 - mapTypeParamNum - mapAbstractionVarNum;

+

+      List<VCExprVar!>! freeTypeVars =

+        HelperFuns.VarVector("u", mapAbstractionVarNum, AxBuilder.T, Gen);

+      List<VCExprVar!>! boundTypeVars0 =

+        HelperFuns.VarVector("s", mapTypeParamNum, AxBuilder.T, Gen);

+      List<VCExprVar!>! boundTypeVars1 =

+        HelperFuns.VarVector("t", mapTypeParamNum, AxBuilder.T, Gen);

+

+      List<VCExprVar!>! types0 = new List<VCExprVar!> (boundTypeVars0);

+      types0.AddRange(freeTypeVars);

+

+      List<VCExprVar!>! types1 = new List<VCExprVar!> (boundTypeVars1);

+      types1.AddRange(freeTypeVars);

+

+      List<Type!> indexTypes = new List<Type!>();

+      for (int i = mapTypeParamNum + mapAbstractionVarNum + 1; i < select.InParams.Length; i++)

+      {

+        indexTypes.Add(((!)select.InParams[i]).TypedIdent.Type);

+      }

+      assert arity == indexTypes.Count;

+      

+      List<VCExprVar!>! indexes0 = HelperFuns.VarVector("x", indexTypes, Gen);

+      List<VCExprVar!>! indexes1 = HelperFuns.VarVector("y", indexTypes, Gen);

+

+      VCExprVar! m = Gen.Variable("m", AxBuilder.U);

+      VCExprVar! val = Gen.Variable("val", ((!)select.OutParams[0]).TypedIdent.Type);

+

+      VCExpr! storeExpr = Store(store, types0, m, indexes0, val);

+      VCExpr! selectWithoutStoreExpr = Select(select, types1, m, indexes1);

+      VCExpr! selectExpr = Select(select, types1, storeExpr, indexes1);

+

+      VCExpr! selectEq = Gen.Eq(selectExpr, selectWithoutStoreExpr);

+

+      List<VCExprVar!>! quantifiedVars = new List<VCExprVar!> ();

+      quantifiedVars.AddRange(freeTypeVars);

+      quantifiedVars.AddRange(boundTypeVars0);

+      quantifiedVars.AddRange(boundTypeVars1);

+      quantifiedVars.Add(val);

+      quantifiedVars.Add(m);

+      quantifiedVars.AddRange(indexes0);

+      quantifiedVars.AddRange(indexes1);

+

+      List<VCTrigger!>! triggers = new List<VCTrigger!> ();

+

+      // different value arguments or different type arguments are sufficient

+      // to conclude that that value of the map at some point (after an update)

+      // has not changed

+

+      List<VCExpr!>! indexEqs = new List<VCExpr!> ();

+      for (int i = 0; i < mapTypeParamNum; ++i)

+        indexEqs.Add(Gen.Eq(boundTypeVars0[i], boundTypeVars1[i]));

+      for (int i = 0; i < arity; ++i)

+        indexEqs.Add(Gen.Eq(indexes0[i], indexes1[i]));

+

+      VCExpr! axiom = VCExpressionGenerator.True;

+      int n = 0;

+      foreach (VCExpr! indexesEq in indexEqs) {

+        VCExpr! matrix = Gen.Or(indexesEq, selectEq);

+        VCExpr! conjunct = Gen.Forall(quantifiedVars, triggers,

+                                      "mapAx1:" + select.Name + ":" + n, matrix);

+        axiom = Gen.AndSimp(axiom, conjunct);

+        n = n + 1;

+      }

+

+      return axiom;

+    }

+  }

+

+  //////////////////////////////////////////////////////////////////////////////

+

+  public class TypeEraserArguments : TypeEraser {

+

+    private readonly TypeAxiomBuilderArguments! AxBuilderArguments;

+

+    private OpTypeEraser OpEraserAttr = null;

+    protected override OpTypeEraser! OpEraser { get {

+      if (OpEraserAttr == null)

+        OpEraserAttr = new OpTypeEraserArguments(this, AxBuilderArguments, Gen);

+      return OpEraserAttr;

+    } }

+

+    public TypeEraserArguments(TypeAxiomBuilderArguments! axBuilder,

+                               VCExpressionGenerator! gen) {

+      base(axBuilder, gen);

+      this.AxBuilderArguments = axBuilder;

+    }

+

+    ////////////////////////////////////////////////////////////////////////////

+

+    public override VCExpr! Visit(VCExprQuantifier! node,

+                                  VariableBindings! oldBindings) {

+      VariableBindings! bindings = oldBindings.Clone();

+      

+      // bound term variables are replaced with bound term variables

+      // typed in a simpler way

+      List<VCExprVar!>! newBoundVars =

+        BoundVarsAfterErasure(node.BoundVars, bindings);

+

+      // type variables are replaced with ordinary quantified variables

+      GenBoundVarsForTypeParams(node.TypeParameters, newBoundVars, bindings);

+      VCExpr! newNode = HandleQuantifier(node, newBoundVars, bindings);

+

+      if (!(newNode is VCExprQuantifier) || !IsUniversalQuantifier(node))

+        return newNode;

+

+      VariableBindings! bindings2;

+      if (!RedoQuantifier(node, (VCExprQuantifier)newNode, node.BoundVars, oldBindings,

+                          out bindings2, out newBoundVars))

+        return newNode;

+

+      GenBoundVarsForTypeParams(node.TypeParameters, newBoundVars, bindings2);

+      return HandleQuantifier(node, newBoundVars, bindings2);

+    }

+

+    private void GenBoundVarsForTypeParams(List<TypeVariable!>! typeParams,

+                                           List<VCExprVar!>! newBoundVars,

+                                           VariableBindings! bindings) {

+      foreach (TypeVariable! tvar in typeParams) {

+        VCExprVar! var = Gen.Variable(tvar.Name, AxBuilder.T);

+        newBoundVars.Add(var);

+        bindings.TypeVariableBindings.Add(tvar, var);

+      }

+    }

+

+    private VCExpr! HandleQuantifier(VCExprQuantifier! node,

+                                     List<VCExprVar!>! newBoundVars,

+                                     VariableBindings! bindings) {

+      List<VCTrigger!>! newTriggers = MutateTriggers(node.Triggers, bindings);

+      VCExpr! newBody = Mutate(node.Body, bindings);

+      newBody = AxBuilder.Cast(newBody, Type.Bool);

+

+      if (newBoundVars.Count == 0)  // might happen that no bound variables are left

+        return newBody;

+      return Gen.Quantify(node.Quan, new List<TypeVariable!> (), newBoundVars,

+                          newTriggers, node.Infos, newBody);

+    }

+  }

+

+  //////////////////////////////////////////////////////////////////////////////

+

+  public class OpTypeEraserArguments : OpTypeEraser {

+

+    protected readonly TypeAxiomBuilderArguments! AxBuilderArguments;

+

+    public OpTypeEraserArguments(TypeEraserArguments! eraser,

+                                 TypeAxiomBuilderArguments! axBuilder,

+                                 VCExpressionGenerator! gen) {

+      base(eraser, axBuilder, gen);

+      this.AxBuilderArguments = axBuilder;

+    }

+

+    ////////////////////////////////////////////////////////////////////////////

+

+    private VCExpr! AssembleOpExpression(OpTypesPair opTypes,

+                                         IEnumerable<VCExpr!>! oldArgs,

+                                         VariableBindings! bindings) {

+      // UGLY: the code for tracking polarities should be factored out

+      int oldPolarity = Eraser.Polarity;

+      Eraser.Polarity = 0;

+

+      List<VCExpr!>! newArgs = new List<VCExpr!> ();

+      // explicit type parameters

+      foreach (Type! t in opTypes.Types)

+        newArgs.Add(AxBuilder.Type2Term(t, bindings.TypeVariableBindings));

+      

+      // and the actual value parameters

+      Function! newFun = ((VCExprBoogieFunctionOp)opTypes.Op).Func;

+                          // ^ we only allow this operator at this point

+      int i = opTypes.Types.Count;

+      foreach (VCExpr! arg in oldArgs) {

+        newArgs.Add(AxBuilder.Cast(Eraser.Mutate(arg, bindings),

+                                   ((!)newFun.InParams[i]).TypedIdent.Type));

+        i = i + 1;

+      }

+

+      Eraser.Polarity = oldPolarity;

+      return Gen.Function(opTypes.Op, newArgs);

+    }

+

+    // for the time being, we store both the types of the arguments and the explicit

+    // type parameters (for most operators, this is more than actually necessary)

+    private OpTypesPair OriginalOpTypes(VCExprNAry! node) {

+      List<Type!>! originalTypes = new List<Type!> ();

+      foreach (VCExpr! expr in node)

+        originalTypes.Add(expr.Type);

+      originalTypes.AddRange(node.TypeArguments);

+      return new OpTypesPair (node.Op, originalTypes);

+    }

+

+    private VCExpr! EqualTypes(Type! t0, Type! t1, VariableBindings! bindings) {

+      if (t0.Equals(t1))

+        return VCExpressionGenerator.True;

+      VCExpr! t0Expr = AxBuilder.Type2Term(t0, bindings.TypeVariableBindings);

+      VCExpr! t1Expr = AxBuilder.Type2Term(t1, bindings.TypeVariableBindings);

+      return Gen.Eq(t0Expr, t1Expr);

+    }

+

+    ///////////////////////////////////////////////////////////////////////////

+

+    public override VCExpr! VisitEqOp       (VCExprNAry! node, VariableBindings! bindings) {

+      // we also have to state that the types are equal, because the

+      // translation does not contain any information about the

+      // relationship between values and types

+      return Gen.AndSimp(base.VisitEqOp(node, bindings),

+                         EqualTypes(node[0].Type, node[1].Type, bindings));

+    }

+

+    public override VCExpr! VisitNeqOp      (VCExprNAry! node, VariableBindings! bindings) {

+      // we also have to state that the types are (un)equal, because the

+      // translation does not contain any information about the

+      // relationship between values and types

+      return Gen.OrSimp(base.VisitNeqOp(node, bindings),

+                        Gen.Not(EqualTypes(node[0].Type, node[1].Type, bindings)));

+    }

+

+    public override VCExpr! VisitSubtypeOp  (VCExprNAry! node, VariableBindings! bindings) {

+      // UGLY: the code for tracking polarities should be factored out

+      int oldPolarity = Eraser.Polarity;

+      Eraser.Polarity = 0;

+

+      VCExpr! res =

+        Gen.Function(VCExpressionGenerator.Subtype3Op,

+                     AxBuilder.Type2Term(node[0].Type,

+                                         bindings.TypeVariableBindings),

+                     AxBuilder.Cast(Eraser.Mutate(node[0], bindings),

+                                    AxBuilder.U),

+                     AxBuilder.Cast(Eraser.Mutate(node[1], bindings),

+                                    AxBuilder.U));

+

+      Eraser.Polarity = oldPolarity;

+      return res;

+    }

+    

+    public override VCExpr! VisitSelectOp   (VCExprNAry! node, VariableBindings! bindings) {

+      OpTypesPair originalOpTypes = OriginalOpTypes(node);

+      OpTypesPair newOpTypes;

+

+      if (!NewOpCache.TryGetValue(originalOpTypes, out newOpTypes)) {

+        MapType! rawType = node[0].Type.AsMap;

+        TypeSeq! abstractionInstantiation;

+        Function! select =

+          AxBuilder.MapTypeAbstracter.Select(rawType, out abstractionInstantiation);

+

+        newOpTypes = TypesPairForSelectStore(node, select, abstractionInstantiation);

+        NewOpCache.Add(originalOpTypes, newOpTypes);

+      }

+

+      return AssembleOpExpression(newOpTypes, node, bindings);

+    }

+

+    public override VCExpr! VisitStoreOp    (VCExprNAry! node, VariableBindings! bindings) {

+      OpTypesPair originalOpTypes = OriginalOpTypes(node);

+      OpTypesPair newOpTypes;

+

+      if (!NewOpCache.TryGetValue(originalOpTypes, out newOpTypes)) {

+        MapType! rawType = node[0].Type.AsMap;

+        TypeSeq! abstractionInstantiation;

+        Function! store =

+          AxBuilder.MapTypeAbstracter.Store(rawType, out abstractionInstantiation);

+

+        newOpTypes = TypesPairForSelectStore(node, store, abstractionInstantiation);

+        NewOpCache.Add(originalOpTypes, newOpTypes);

+      }

+

+      return AssembleOpExpression(newOpTypes, node, bindings);

+    }

+

+    private OpTypesPair TypesPairForSelectStore(VCExprNAry! node, Function! untypedOp,

+                                                // instantiation of the abstract map type parameters

+                                                TypeSeq! abstractionInstantiation) {

+      List<Type!>! inferredTypeArgs = new List<Type!> ();

+      foreach (Type! t in node.TypeArguments)

+//        inferredTypeArgs.Add(AxBuilder.MapTypeAbstracter.AbstractMapTypeRecursively(t));

+        inferredTypeArgs.Add(t);

+      foreach (Type! t in abstractionInstantiation)

+        inferredTypeArgs.Add(t);

+

+      assert untypedOp.InParams.Length == inferredTypeArgs.Count + node.Arity;

+      return new OpTypesPair (Gen.BoogieFunctionOp(untypedOp), inferredTypeArgs);

+    }

+

+    ///////////////////////////////////////////////////////////////////////////

+

+    public override VCExpr! VisitBoogieFunctionOp (VCExprNAry! node, VariableBindings! bindings) {

+      OpTypesPair originalOpTypes = OriginalOpTypes(node);

+      OpTypesPair newOpTypes;

+

+      if (!NewOpCache.TryGetValue(originalOpTypes, out newOpTypes)) {

+        Function! oriFun = ((VCExprBoogieFunctionOp)node.Op).Func;

+

+        List<Type!>! inferredTypeArgs = new List<Type!> ();

+        foreach (Type! t in node.TypeArguments)

+//          inferredTypeArgs.Add(AxBuilder.MapTypeAbstracter.AbstractMapTypeRecursively(t));

+          inferredTypeArgs.Add(t);

+

+        VCExprOp! newOp = Gen.BoogieFunctionOp(AxBuilderArguments.Typed2Untyped(oriFun));

+        newOpTypes = new OpTypesPair (newOp, inferredTypeArgs);

+

+        NewOpCache.Add(originalOpTypes, newOpTypes);

+      }

+

+      return AssembleOpExpression(newOpTypes, node, bindings);

+    }

+

+    ///////////////////////////////////////////////////////////////////////////

+

+    // cache from the typed operators to the untyped operators with

+    // explicit type arguments. the keys are pairs of the typed

+    // operator and the actual types of the argument expressions, the

+    // values are pairs of the new operators and the types that have

+    // to be given as explicit type arguments

+    private readonly IDictionary<OpTypesPair, OpTypesPair>! NewOpCache =

+      new Dictionary<OpTypesPair, OpTypesPair>();

+

+    private struct OpTypesPair {

+      public readonly VCExprOp! Op;

+      public readonly List<Type!>! Types;

+

+      public OpTypesPair(VCExprOp! op, List<Type!>! types) {

+        this.Op = op;

+        this.Types = types;

+        this.HashCode = HFNS.PolyHash(op.GetHashCode(), 17, types);

+      }

+

+      [Pure][Reads(ReadsAttribute.Reads.Nothing)]

+      public override bool Equals(object that) {

+        if (that is OpTypesPair) {

+          OpTypesPair thatPair = (OpTypesPair)that;

+          return this.Op.Equals(thatPair.Op) &&

+            HFNS.SameElements(this.Types, thatPair.Types);

+        }

+        return false;

+      }

+

+      private readonly int HashCode;

+

+      [Pure]

+      public override int GetHashCode() {

+        return HashCode;

+      }

+    }

+  }

+

+}