//-----------------------------------------------------------------------------
//
// 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;

// A translator from the Boogie AST to the VCExpr AST.
// This was previously realised in the methods AbsyExpr.VCView

namespace Microsoft.Boogie.VCExprAST {
  using Microsoft.Boogie;

  // TODO: in future we might use that for defining symbols for Boogie's conditional compilation 
  public class VCGenerationOptions {
    private readonly List<string/*!*/>/*!*/ SupportedProverCommands;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(cce.NonNullElements(SupportedProverCommands));
    }


    public bool IsProverCommandSupported(string kind) {
      Contract.Requires(kind != null);
      return SupportedProverCommands.Contains(kind);
    }

    public bool IsAnyProverCommandSupported(string kinds) {
      Contract.Requires(kinds != null);
      if (kinds.IndexOf(',') < 0) {
        return IsProverCommandSupported(kinds);
      } else {
        return kinds.Split(',', ' ').Any(k => IsProverCommandSupported(k));
      }
    }

    public VCGenerationOptions(List<string/*!*/>/*!*/ supportedProverCommands) {
      Contract.Requires(cce.NonNullElements(supportedProverCommands));
      this.SupportedProverCommands = supportedProverCommands;
    }
  }

  public delegate VCExpr/*!*/ CodeExprConverter(CodeExpr/*!*/ codeExpr, Hashtable/*<Block, VCExprVar!>*//*!*/ blockVariables, List<VCExprLetBinding> bindings, bool isPositiveContext);

  public class Boogie2VCExprTranslator : ReadOnlyVisitor, ICloneable {
    // Stack on which the various Visit-methods put the result of the translation
    private readonly Stack<VCExpr/*!*/>/*!*/ SubExpressions = new Stack<VCExpr>();
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(cce.NonNullElements(SubExpressions));
      Contract.Invariant(Gen != null);
    }


    private void Push(VCExpr expr) {
      Contract.Requires(expr != null);
      SubExpressions.Push(expr);
    }

    private VCExpr Pop() {
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return SubExpressions.Pop();
    }

    public VCExpr Translate(Expr expr) {
      Contract.Requires(expr != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      this.Visit(expr);
      return Pop();
    }

    public List<VCExpr/*!*/>/*!*/ Translate(IList<Expr> exprs) {
      Contract.Requires(exprs != null);
      Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
      List<VCExpr/*!*/>/*!*/ res = new List<VCExpr/*!*/>();
      foreach (Expr e in exprs)
        res.Add(Translate(cce.NonNull(e)));
      return res;
    }

    ///////////////////////////////////////////////////////////////////////////////

    internal readonly VCExpressionGenerator/*!*/ Gen;

    public Boogie2VCExprTranslator(VCExpressionGenerator gen,
                                   VCGenerationOptions genOptions) {
      Contract.Requires(gen != null);
      Contract.Requires(genOptions != null);
      this.Gen = gen;
      this.GenerationOptions = genOptions;
      UnboundVariables = new VariableMapping<Variable>();
      BoundVariables = new VariableMapping<BoundVariable>();
      Formals = new VariableMapping<Formal>();
    }

    private Boogie2VCExprTranslator(Boogie2VCExprTranslator tl) {
      Contract.Requires(tl != null);
      this.Gen = tl.Gen;
      this.GenerationOptions = tl.GenerationOptions;
      UnboundVariables =
        (VariableMapping<Variable>)tl.UnboundVariables.Clone();
      BoundVariables = new VariableMapping<BoundVariable>();
      Formals = new VariableMapping<Formal>();
    }

    public object Clone() {
      Contract.Ensures(Contract.Result<object>() != null);
      return new Boogie2VCExprTranslator(this);
    }

    private IAppliableTranslator IAppTranslatorAttr = null;
    private IAppliableTranslator IAppTranslator {
      get {
        Contract.Ensures(Contract.Result<IAppliableTranslator>() != null);

        if (IAppTranslatorAttr == null)
          IAppTranslatorAttr = new IAppliableTranslator(this);
        return IAppTranslatorAttr;
      }
    }

    ///////////////////////////////////////////////////////////////////////////////
    // Class for handling occurring variables

    private class VariableMapping<VarKind> : ICloneable {
      private readonly List<Dictionary<VarKind/*!*/, VCExprVar/*!*/>/*!*/>/*!*/ Mapping;
      [ContractInvariantMethod]
      void ObjectInvariant() {
        Contract.Invariant(Mapping != null && Contract.ForAll(Mapping, i => cce.NonNullDictionaryAndValues(i)));
      }


      public VariableMapping() {
        List<Dictionary<VarKind/*!*/, VCExprVar/*!*/>/*!*/>/*!*/ mapping =
          new List<Dictionary<VarKind/*!*/, VCExprVar/*!*/>/*!*/>();
        mapping.Add(new Dictionary<VarKind/*!*/, VCExprVar/*!*/>());
        this.Mapping = mapping;
      }

      private VariableMapping(VariableMapping<VarKind> vm) {
        Contract.Requires(vm != null);
        List<Dictionary<VarKind/*!*/, VCExprVar/*!*/>/*!*/>/*!*/ mapping =
          new List<Dictionary<VarKind/*!*/, VCExprVar/*!*/>/*!*/>();
        foreach (Dictionary<VarKind/*!*/, VCExprVar/*!*/>/*!*/ d in vm.Mapping) {
          Contract.Assert(cce.NonNullDictionaryAndValues(d));
          mapping.Add(new Dictionary<VarKind/*!*/, VCExprVar/*!*/>(d));
        }
        this.Mapping = mapping;
      }

      public object Clone() {
        Contract.Ensures(Contract.Result<object>() != null);
        return new VariableMapping<VarKind>(this);
      }

      public void PushScope() {
        Mapping.Add(new Dictionary<VarKind/*!*/, VCExprVar/*!*/>());
      }

      public void PopScope() {
        Contract.Assume(Mapping.Count > 0);
        Mapping.RemoveAt(Mapping.Count - 1);
      }

      public void Bind(VarKind boogieVar, VCExprVar/*!*/ vcExprVar) {
        Contract.Requires(vcExprVar != null);
        Contract.Requires(boogieVar != null);
        Contract.Requires(!Contains(boogieVar));
        Mapping[Mapping.Count - 1].Add(boogieVar, vcExprVar);
      }

      public VCExprVar Lookup(VarKind boogieVar) {
        Contract.Requires(boogieVar != null);
        Contract.Ensures(Contract.Result<VCExprVar>() != null);
        VCExprVar res = LookupHelp(boogieVar);
        Contract.Assume(res != null);
        return res;
      }

      [Pure]
      public bool Contains(VarKind boogieVar) {
        Contract.Requires(boogieVar != null);
        return LookupHelp(boogieVar) != null;
      }

      public bool TryGetValue(VarKind boogieVar, out VCExprVar res) {
        Contract.Requires(boogieVar != null);
        res = LookupHelp(boogieVar);
        return res != null;
      }

      [Pure]
      private VCExprVar LookupHelp(VarKind boogieVar) {
        Contract.Requires(boogieVar != null);
        VCExprVar res;
        foreach (Dictionary<VarKind/*!*/, VCExprVar/*!*/>/*!*/ d in Mapping) {
          //Contract.Assert(cce.NonNullElements(d));
          if (d.TryGetValue(boogieVar, out res)) {
            Contract.Assert(res != null);
            return res;
          }
        }
        return null;
      }
    }

    //////////////////////////////////////////////////////////////////////////////////

    private readonly VariableMapping<Variable>/*!*/ UnboundVariables;
    private readonly VariableMapping<BoundVariable>/*!*/ BoundVariables;
    // used when translating the bodies of function expansions
    private readonly VariableMapping<Formal>/*!*/ Formals;
    [ContractInvariantMethod]
    void ObjectInvairant() {
      Contract.Invariant(UnboundVariables != null);
      Contract.Invariant(BoundVariables != null);
      Contract.Invariant(Formals != null);
    }


    internal void PushBoundVariableScope() {
      BoundVariables.PushScope();
    }
    internal void PopBoundVariableScope() {
      BoundVariables.PopScope();
    }

    internal void PushFormalsScope() {
      Formals.PushScope();
    }
    internal void PopFormalsScope() {
      Formals.PopScope();
    }

    public VCExprVar BindVariable(Variable boogieVar) {
      Contract.Requires(boogieVar != null);
      Contract.Ensures(Contract.Result<VCExprVar>() != null);
      if (boogieVar is BoundVariable) {
        VCExprVar/*!*/ newVar = Gen.Variable(boogieVar.Name, boogieVar.TypedIdent.Type);
        BoundVariables.Bind((BoundVariable)boogieVar, newVar);
        return newVar;
      } else if (boogieVar is Formal) {
        VCExprVar/*!*/ newVar = Gen.Variable(boogieVar.Name, boogieVar.TypedIdent.Type);
        Formals.Bind((Formal)boogieVar, newVar);
        return newVar;
      } else {
        // only bound variables and formals are declared explicitly
        Contract.Assert(false);
        throw new cce.UnreachableException();
      }
    }

    public VCExprVar LookupVariable(Variable boogieVar) {
      Contract.Requires(boogieVar != null);
      Contract.Ensures(Contract.Result<VCExprVar>() != null);

      BoundVariable bv = boogieVar as BoundVariable;
      if (bv != null) {
        return BoundVariables.Lookup(bv);
      }
      VCExprVar res;
      Formal fml = boogieVar as Formal;
      if (fml != null && Formals.TryGetValue(fml, out res))
        return cce.NonNull(res);

      // global variables, local variables, incarnations, etc. are
      // bound the first time they occur
      if (!UnboundVariables.TryGetValue(boogieVar, out res)) {
        if (boogieVar is Constant)
          res = new VCExprConstant(boogieVar.Name, boogieVar.TypedIdent.Type);
        else 
          res = new VCExprVar(boogieVar.Name, boogieVar.TypedIdent.Type);
        UnboundVariables.Bind(boogieVar, res);
      }
      return cce.NonNull(res);
    }

    /// <summary>
    /// Unlike LookupVariable, this method does not create a new variable mapping if none is
    /// found.  Instead, this method returns null in such cases.  Also, this method does not
    /// look for bound variables.
    /// </summary>
    /// <param name="boogieVar"></param>
    /// <returns></returns>
    public VCExprVar TryLookupVariable(Variable boogieVar) {
      Contract.Requires(boogieVar != null);

      VCExprVar res;
      Formal fml = boogieVar as Formal;
      if (fml != null && Formals.TryGetValue(fml, out res))
        return cce.NonNull(res);

      if (UnboundVariables.TryGetValue(boogieVar, out res)) {
        return cce.NonNull(res);
      }

      return null;  // not present
    }

    ///////////////////////////////////////////////////////////////////////////////////

    internal readonly VCGenerationOptions/*!*/ GenerationOptions;
    [ContractInvariantMethod]
    void ObjectInvarian() {
      Contract.Invariant(GenerationOptions != null);
    }

    ///////////////////////////////////////////////////////////////////////////////////

    public override Expr VisitLiteralExpr(LiteralExpr node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Expr>() != null);
      Push(TranslateLiteralExpr(node));
      return node;
    }
    private VCExpr TranslateLiteralExpr(LiteralExpr node) {
      Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      if (node.Val is bool) {
        bool b = (bool)node.Val;
        if (b) {
          return VCExpressionGenerator.True;
        } else {
          return VCExpressionGenerator.False;
        }
      } else if (node.Val is BigNum) {
        return Gen.Integer(node.asBigNum);
      } else if (node.Val is BigDec) {
        return Gen.Real(node.asBigDec);
      } else if (node.Val is BvConst) {
        return Gen.Bitvector((BvConst)node.Val);
      } else {
        System.Diagnostics.Debug.Assert(false, "unknown kind of literal " + node.tok.ToString());
        Contract.Assert(false);
        throw new cce.UnreachableException();
      }
    }

    ///////////////////////////////////////////////////////////////////////////////////

    public override Expr VisitIdentifierExpr(IdentifierExpr node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Expr>() != null);
      Contract.Assume(node.Decl != null);   // the expression has to be resolved
      Push(LookupVariable(node.Decl));
      return node;
    }

    ///////////////////////////////////////////////////////////////////////////////////

    // Because of our scheme for numbering incarnations of variables, the pre-state
    // value of a variable x is always just "x". (The first update to it in a method
    // causes it to become "x0". So we just remove old expressions with a visitor
    // before transforming it into a VCExpr.
    public override Expr VisitOldExpr(OldExpr node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Expr>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }

    ///////////////////////////////////////////////////////////////////////////////////

    public override Expr VisitNAryExpr(NAryExpr node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Expr>() != null);
      Push(TranslateNAryExpr(node));
      return node;
    }

    public bool isPositiveContext = true;
    private VCExpr TranslateNAryExpr(NAryExpr node) {
      Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
     
      bool flipContextForArg0 = false;
      if (node.Fun is UnaryOperator)
      {
          UnaryOperator oper = (UnaryOperator)node.Fun;
          if (oper.Op == UnaryOperator.Opcode.Not)
              flipContextForArg0 = true;
      }
      else if (node.Fun is BinaryOperator)
      {
          BinaryOperator oper = (BinaryOperator)node.Fun;
          if (oper.Op == BinaryOperator.Opcode.Imp)
              flipContextForArg0 = true;
          else if (oper.Op == BinaryOperator.Opcode.Iff) {
              Expr one = new NAryExpr(node.tok, new BinaryOperator(node.tok, BinaryOperator.Opcode.Imp), new List<Expr> { node.Args[0], node.Args[1] });
              Expr two = new NAryExpr(node.tok, new BinaryOperator(node.tok, BinaryOperator.Opcode.Imp), new List<Expr> { node.Args[1], node.Args[0] });
              NAryExpr cmpd = new NAryExpr(node.tok, new BinaryOperator(node.tok, BinaryOperator.Opcode.And), new List<Expr> { one, two });
              TypecheckingContext tc = new TypecheckingContext(null);
              cmpd.Typecheck(tc);
              return TranslateNAryExpr(cmpd);
          }
      }

      int n = node.Args.Count;
      List<VCExpr/*!*/>/*!*/ vcs = new List<VCExpr/*!*/>(n);
        
      for (int i = 0; i < n; i++) {
        if (i == 0 && flipContextForArg0)
            isPositiveContext = !isPositiveContext;
        vcs.Add(Translate(cce.NonNull(node.Args)[i]));
        if (i == 0 && flipContextForArg0)
            isPositiveContext = !isPositiveContext;
      }

      if (node.Type == null) {
        System.Console.WriteLine("*** type is null for {0}", node);
        Contract.Assert(false);
        throw new cce.UnreachableException();
      }

      return IAppTranslator.Translate(node.Fun, node.Type, vcs,
                                      ToList(cce.NonNull(node.TypeParameters)));
    }


    private static List<Type/*!*/>/*!*/ EMPTY_TYPE_LIST = new List<Type/*!*/>();
    [ContractInvariantMethod]
    void ObjectInvirant() {
      Contract.Invariant(EMPTY_TYPE_LIST != null);
    }


    private List<Type/*!*/>/*!*/ ToList(TypeParamInstantiation insts) {
      Contract.Requires(insts != null);
      Contract.Ensures(cce.NonNullElements(Contract.Result<List<Type>>()));
      if (insts.FormalTypeParams.Count == 0)
        return EMPTY_TYPE_LIST;

      List<Type/*!*/>/*!*/ typeArgs = new List<Type/*!*/>();
      foreach (TypeVariable/*!*/ var in insts.FormalTypeParams) {
        Contract.Assert(var != null);
        typeArgs.Add(insts[var]);
      }
      return typeArgs;
    }

    ///////////////////////////////////////////////////////////////////////////////////

    public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<QuantifierExpr>() != null);
      Push(TranslateQuantifierExpr(node));
      return node;
    }

    public override Expr VisitExistsExpr(ExistsExpr node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Expr>() != null);
      node = (ExistsExpr)this.VisitQuantifierExpr(node);
      return node;
    }

    public override Expr VisitForallExpr(ForallExpr node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Expr>() != null);
      node = (ForallExpr)this.VisitQuantifierExpr(node);
      return node;
    }

    private VCExpr TranslateQuantifierExpr(QuantifierExpr node) {
      Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      List<TypeVariable/*!*/>/*!*/ typeParams = new List<TypeVariable/*!*/>();
      foreach (TypeVariable/*!*/ v in node.TypeParameters) {
        Contract.Assert(v != null);
        typeParams.Add(v);
      }

      PushBoundVariableScope();

      List<VCExprVar/*!*/>/*!*/ boundVars = new List<VCExprVar/*!*/>();
      foreach (Variable/*!*/ v in node.Dummies)
        boundVars.Add(BindVariable(v));

      try {
        List<VCTrigger/*!*/>/*!*/ triggers = TranslateTriggers(node.Triggers);
        VCExpr/*!*/ body = Translate(node.Body);
        VCQuantifierInfos/*!*/ infos = GenerateQuantifierInfos(node);

        Quantifier quan;
        if (node is ForallExpr)
          quan = Quantifier.ALL;
        else if (node is ExistsExpr)
          quan = Quantifier.EX;
        else {
          Contract.Assert(false);
          throw new cce.UnreachableException();
        }

        return Gen.Quantify(quan, typeParams, boundVars, triggers, infos, body);
      } finally {
        PopBoundVariableScope();
      }
    }

    private List<VCTrigger/*!*/>/*!*/ TranslateTriggers(Trigger node) {
      Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCTrigger>>()));
      List<VCTrigger/*!*/>/*!*/ res = new List<VCTrigger/*!*/>();
      Trigger curTrigger = node;
      while (curTrigger != null) {
        res.Add(Gen.Trigger(curTrigger.Pos, Translate(curTrigger.Tr)));
        curTrigger = curTrigger.Next;
      }
      return res;
    }

    private VCQuantifierInfos GenerateQuantifierInfos(QuantifierExpr node) {
      Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<VCQuantifierInfos>() != null);
      string qid = getQidNameFromQKeyValue(node.Dummies, node.Attributes);
      return new VCQuantifierInfos(qid, node.SkolemId, false, node.Attributes);
    }

    private string getQidNameFromQKeyValue(List<Variable> vars, QKeyValue attributes) {
      Contract.Requires(vars != null);
      // Check for a 'qid, name' pair in keyvalues
      string qid = QKeyValue.FindStringAttribute(attributes, "qid");
      if (qid == null && vars.Count != 0) {
        // generate default name (line:column position in .bpl file)
        Variable v = vars[0];
        Contract.Assert(v != null); // Rustan's claim!
        // Include the first 8 characters of the filename in QID (helpful in case we use /concat)
        // We limit it to 8, so the SX file doesn't grow too big, and who on earth would need
        // more than 8 characters in a filename anyways.
        int max = 8;
        StringBuilder buf = new StringBuilder(max + 20);
        string filename = v.tok.filename;
        if (filename == null)
          filename = "unknown";
        for (int i = 0; i < filename.Length; ++i) {
          if (filename[i] == '/' || filename[i] == '\\')
            buf.Length = 0;
          if (buf.Length < max && char.IsLetterOrDigit(filename[i])) {
            if (buf.Length == 0 && char.IsDigit(filename[i])) {
              // Z3 does not like QID's to start with a digit, so we prepend another character
              buf.Append('_');
            }
            buf.Append(filename[i]);
          }
        }
        buf.Append('.').Append(v.Line).Append(':').Append(v.Col);
        qid = buf.ToString();
      }
      return qid;
    }

    ///////////////////////////////////////////////////////////////////////////////////

    public override Expr VisitBvExtractExpr(BvExtractExpr node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Expr>() != null);
      Push(TranslateBvExtractExpr(node));
      return node;
    }

    private VCExpr TranslateBvExtractExpr(BvExtractExpr node) {
      Contract.Requires(node != null);
      Contract.Requires((node.Start <= node.End));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      VCExpr/*!*/ bv = Translate(node.Bitvector);
      return Gen.BvExtract(bv, cce.NonNull(node.Bitvector.Type).BvBits, node.Start, node.End);
    }

    ///////////////////////////////////////////////////////////////////////////////////

    public override Expr VisitBvConcatExpr(BvConcatExpr node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Expr>() != null);
      Push(TranslateBvConcatExpr(node));
      return node;
    }

    private VCExpr TranslateBvConcatExpr(BvConcatExpr node) {
      Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      VCExpr/*!*/ bv0 = Translate(node.E0);
      VCExpr/*!*/ bv1 = Translate(node.E1);
      return Gen.BvConcat(bv0, bv1);
    }

    ///////////////////////////////////////////////////////////////////////////////////
    // all the other cases should never happen

    public override Cmd VisitAssertCmd(AssertCmd node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Cmd>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Cmd VisitAssignCmd(AssignCmd node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Cmd>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Cmd VisitAssumeCmd(AssumeCmd node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Cmd>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override AtomicRE VisitAtomicRE(AtomicRE node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<AtomicRE>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Axiom VisitAxiom(Axiom node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Axiom>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Type VisitBasicType(BasicType node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Type>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Type VisitBvType(BvType node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Type>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Block VisitBlock(Block node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Block>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public CodeExprConverter codeExprConverter = null;
    public void SetCodeExprConverter(CodeExprConverter f) {
      this.codeExprConverter = f;
    }
    public override Expr/*!*/ VisitCodeExpr(CodeExpr/*!*/ codeExpr) {
      //Contract.Requires(codeExpr != null);
      Contract.Ensures(Contract.Result<Expr>() != null);
      Contract.Assume(codeExprConverter != null);

      Hashtable/*<Block, LetVariable!>*/ blockVariables = new Hashtable/*<Block, LetVariable!!>*/();
      List<VCExprLetBinding/*!*/> bindings = new List<VCExprLetBinding/*!*/>();
      VCExpr e = codeExprConverter(codeExpr, blockVariables, bindings, isPositiveContext);
      Push(e);
      return codeExpr;
    }
    public override List<Block> VisitBlockSeq(List<Block> blockSeq) {
      //Contract.Requires(blockSeq != null);
      Contract.Ensures(Contract.Result<List<Block>>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override List<Block/*!*/>/*!*/ VisitBlockList(List<Block/*!*/>/*!*/ blocks) {
      //Contract.Requires(cce.NonNullElements(blocks));
      Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override BoundVariable VisitBoundVariable(BoundVariable node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<BoundVariable>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Cmd VisitCallCmd(CallCmd node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Cmd>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Cmd VisitParCallCmd(ParCallCmd node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Cmd>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq) {
      //Contract.Requires(cmdSeq != null);
      Contract.Ensures(Contract.Result<List<Cmd>>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Choice VisitChoice(Choice node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Choice>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Cmd VisitCommentCmd(CommentCmd node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Cmd>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Constant VisitConstant(Constant node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Constant>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override CtorType VisitCtorType(CtorType node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<CtorType>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Declaration VisitDeclaration(Declaration node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Declaration>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override List<Declaration/*!*/>/*!*/ VisitDeclarationList(List<Declaration/*!*/>/*!*/ declarationList) {
      //Contract.Requires(cce.NonNullElements(declarationList));
      Contract.Ensures(cce.NonNullElements(Contract.Result<List<Declaration>>()));
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override DeclWithFormals VisitDeclWithFormals(DeclWithFormals node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<DeclWithFormals>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Requires VisitRequires(Requires @requires) {
      //Contract.Requires(@requires != null);
      Contract.Ensures(Contract.Result<Requires>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override List<Requires> VisitRequiresSeq(List<Requires> requiresSeq) {
      //Contract.Requires(requiresSeq != null);
      Contract.Ensures(Contract.Result<List<Requires>>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Ensures VisitEnsures(Ensures @ensures) {
      //Contract.Requires(@ensures != null);
      Contract.Ensures(Contract.Result<Ensures>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override List<Ensures> VisitEnsuresSeq(List<Ensures> ensuresSeq) {
      //Contract.Requires(ensuresSeq != null);
      Contract.Ensures(Contract.Result<List<Ensures>>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Formal VisitFormal(Formal node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Formal>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Function VisitFunction(Function node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Function>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override GlobalVariable VisitGlobalVariable(GlobalVariable node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<GlobalVariable>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override GotoCmd VisitGotoCmd(GotoCmd node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<GotoCmd>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Cmd VisitHavocCmd(HavocCmd node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Cmd>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Implementation VisitImplementation(Implementation node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Implementation>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override LocalVariable VisitLocalVariable(LocalVariable node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<LocalVariable>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override AssignLhs VisitMapAssignLhs(MapAssignLhs node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<AssignLhs>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override MapType VisitMapType(MapType node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<MapType>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Procedure VisitProcedure(Procedure node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Procedure>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Program VisitProgram(Program node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Program>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Cmd VisitRE(RE node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Cmd>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override List<RE> VisitRESeq(List<RE> reSeq) {
      //Contract.Requires(reSeq != null);
      Contract.Ensures(Contract.Result<List<RE>>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override ReturnCmd VisitReturnCmd(ReturnCmd node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<ReturnCmd>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override ReturnExprCmd VisitReturnExprCmd(ReturnExprCmd node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<ReturnExprCmd>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Sequential VisitSequential(Sequential node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Sequential>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<AssignLhs>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Cmd VisitStateCmd(StateCmd node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Cmd>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override TransferCmd VisitTransferCmd(TransferCmd node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<TransferCmd>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Trigger VisitTrigger(Trigger node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Trigger>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Type VisitType(Type node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Type>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override TypedIdent VisitTypedIdent(TypedIdent node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<TypedIdent>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Type VisitTypeSynonymAnnotation(TypeSynonymAnnotation node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Type>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Type VisitTypeVariable(TypeVariable node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Type>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Variable VisitVariable(Variable node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Variable>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override List<Variable> VisitVariableSeq(List<Variable> variableSeq) {
      //Contract.Requires(variableSeq != null);
      Contract.Ensures(Contract.Result<List<Variable>>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Cmd>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }
    public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) {
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<Cmd>() != null);
      Contract.Assert(false);
      throw new cce.UnreachableException();
    }

  }


  /////////////////////////////////////////////////////////////////////////////////

  public class IAppliableTranslator : IAppliableVisitor<VCExpr/*!*/> {

    private readonly Boogie2VCExprTranslator/*!*/ BaseTranslator;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(BaseTranslator != null);
    }


    private VCExpressionGenerator/*!*/ Gen {
      get {
        Contract.Ensures(Contract.Result<VCExpressionGenerator>() != null);

        return BaseTranslator.Gen;
      }
    }
    private VCGenerationOptions GenerationOptions {
      get {
        Contract.Ensures(Contract.Result<VCGenerationOptions>() != null);

        return BaseTranslator.GenerationOptions;
      }
    }

    public IAppliableTranslator(Boogie2VCExprTranslator baseTranslator) {
      Contract.Requires(baseTranslator != null);
      this.BaseTranslator = baseTranslator;
    }

    ///////////////////////////////////////////////////////////////////////////////

    private List<VCExpr/*!*/>/*!*/ args = new List<VCExpr/*!*/>();
    private List<Type/*!*/>/*!*/ typeArgs = new List<Type/*!*/>();
    [ContractInvariantMethod]
    void ObjectInvarianet() {
      Contract.Invariant(args != null);
      Contract.Invariant(typeArgs != null);
    }


    public VCExpr Translate(IAppliable app, Type ty, List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs) {
      Contract.Requires(ty != null);
      Contract.Requires(app != null);
      Contract.Requires(cce.NonNullElements(typeArgs));
      Contract.Requires(cce.NonNullElements(args));
      Contract.Ensures(Contract.Result<VCExpr>() != null);

      List<VCExpr/*!*/>/*!*/ oldArgs = this.args;
      List<Type/*!*/>/*!*/ oldTypeArgs = this.typeArgs;
      this.args = args;
      this.typeArgs = typeArgs;
      VCExpr/*!*/ result = app.Dispatch<VCExpr/*!*/>(this);
      this.args = oldArgs;
      this.typeArgs = oldTypeArgs;
      return result;
    }

    ///////////////////////////////////////////////////////////////////////////////



    public VCExpr Visit(UnaryOperator unaryOperator) {
      //Contract.Requires(unaryOperator != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      Contract.Assert(unaryOperator.Op == UnaryOperator.Opcode.Neg || unaryOperator.Op == UnaryOperator.Opcode.Not);
      Contract.Assert(this.args.Count == 1);
      if (unaryOperator.Op == UnaryOperator.Opcode.Neg) {
        VCExpr e = cce.NonNull(this.args[0]);
        if (cce.NonNull(e.Type).IsInt) {
          return Gen.Function(VCExpressionGenerator.SubIOp, Gen.Integer(BigNum.ZERO), e);
        }
        else {
          return Gen.Function(VCExpressionGenerator.SubROp, Gen.Real(BigDec.ZERO), e);
        }
      }
      else {
        return Gen.Not(this.args);
      }
    }

    public VCExpr Visit(BinaryOperator binaryOperator) {
      //Contract.Requires(binaryOperator != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return TranslateBinaryOperator(binaryOperator, this.args);
    }

    public VCExpr Visit(FunctionCall functionCall) {
      //Contract.Requires(functionCall != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return TranslateFunctionCall(functionCall, this.args, this.typeArgs);
    }

    public VCExpr Visit(MapSelect mapSelect) {
      //Contract.Requires(mapSelect != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Gen.Select(this.args, this.typeArgs);
    }

    public VCExpr Visit(MapStore mapStore) {
      //Contract.Requires(mapStore != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Gen.Store(this.args, this.typeArgs);
    }

    public VCExpr Visit(TypeCoercion typeCoercion) {
      //Contract.Requires(typeCoercion != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      Contract.Assert(this.args.Count == 1);
      return this.args[0];
    }

    public VCExpr Visit(ArithmeticCoercion arithCoercion) {
      //Contract.Requires(arithCoercion != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      Contract.Assert(this.args.Count == 1);
      switch (arithCoercion.Coercion) {
        case ArithmeticCoercion.CoercionType.ToInt:
          return Gen.Function(VCExpressionGenerator.ToIntOp, this.args);
        case ArithmeticCoercion.CoercionType.ToReal:
          return Gen.Function(VCExpressionGenerator.ToRealOp, this.args);
        default:
          Contract.Assert(false);
          return null;
      }
    }

    public VCExpr Visit(IfThenElse ite) {
      //Contract.Requires(ite != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Gen.Function(VCExpressionGenerator.IfThenElseOp, this.args);
    }

    ///////////////////////////////////////////////////////////////////////////////

    private VCExpr TranslateBinaryOperator(BinaryOperator app, List<VCExpr/*!*/>/*!*/ args) {
      Contract.Requires(app != null);
      Contract.Requires(cce.NonNullElements(args));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      Contract.Assert(args.Count == 2);

      switch (app.Op) {
        case BinaryOperator.Opcode.Add:
          if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {
            return Gen.Function(VCExpressionGenerator.AddIOp, args);
          }
          else {
            return Gen.Function(VCExpressionGenerator.AddROp, args);
          }
        case BinaryOperator.Opcode.Sub:
          if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {
            return Gen.Function(VCExpressionGenerator.SubIOp, args);
          }
          else {
            return Gen.Function(VCExpressionGenerator.SubROp, args);
          }
        case BinaryOperator.Opcode.Mul:
          if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {
            return Gen.Function(VCExpressionGenerator.MulIOp, args);
          }
          else {
            return Gen.Function(VCExpressionGenerator.MulROp, args);
          }
        case BinaryOperator.Opcode.Div:
          return Gen.Function(VCExpressionGenerator.DivIOp, args);
        case BinaryOperator.Opcode.Mod:
          return Gen.Function(VCExpressionGenerator.ModOp, args);
        case BinaryOperator.Opcode.RealDiv:
          VCExpr arg0 = cce.NonNull(args[0]);
          VCExpr arg1 = cce.NonNull(args[1]);
          if (cce.NonNull(arg0.Type).IsInt) {
            arg0 = Gen.Function(VCExpressionGenerator.ToRealOp, arg0);
          }
          if (cce.NonNull(arg1.Type).IsInt) {
            arg1 = Gen.Function(VCExpressionGenerator.ToRealOp, arg1);
          }
          return Gen.Function(VCExpressionGenerator.DivROp, arg0, arg1);
        case BinaryOperator.Opcode.Pow:
          return Gen.Function(VCExpressionGenerator.PowOp, args);
        case BinaryOperator.Opcode.Eq:
        case BinaryOperator.Opcode.Iff:
          // we don't distinguish between equality and equivalence at this point
          return Gen.Function(VCExpressionGenerator.EqOp, args);
        case BinaryOperator.Opcode.Neq:
          return Gen.Function(VCExpressionGenerator.NeqOp, args);
        case BinaryOperator.Opcode.Lt:
          return Gen.Function(VCExpressionGenerator.LtOp, args);
        case BinaryOperator.Opcode.Le:
          return Gen.Function(VCExpressionGenerator.LeOp, args);
        case BinaryOperator.Opcode.Ge:
          return Gen.Function(VCExpressionGenerator.GeOp, args);
        case BinaryOperator.Opcode.Gt:
          return Gen.Function(VCExpressionGenerator.GtOp, args);
        case BinaryOperator.Opcode.Imp:
          return Gen.Function(VCExpressionGenerator.ImpliesOp, args);
        case BinaryOperator.Opcode.And:
          return Gen.Function(VCExpressionGenerator.AndOp, args);
        case BinaryOperator.Opcode.Or:
          return Gen.Function(VCExpressionGenerator.OrOp, args);
        case BinaryOperator.Opcode.Subtype:
          return Gen.Function(VCExpressionGenerator.SubtypeOp, args);
        default:
          Contract.Assert(false);
          throw new cce.UnreachableException();  // unexpected binary operator
      }
    }

    ///////////////////////////////////////////////////////////////////////////////

    private VCExpr/*!*/ TranslateFunctionCall(FunctionCall app, List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs) {
      Contract.Requires(cce.NonNullElements(args));
      Contract.Requires(cce.NonNullElements(typeArgs));
      Contract.Requires(app != null);
      Contract.Requires((app.Func != null));
      Contract.Ensures(Contract.Result<VCExpr>() != null);    // resolution must have happened

      VCExpr res = ApplyExpansion(app, args, typeArgs);
      if (res != null)
        return res;

      VCExprOp/*!*/ functionOp = Gen.BoogieFunctionOp(app.Func);
      return Gen.Function(functionOp, args, typeArgs);
    }

    private VCExpr ApplyExpansion(FunctionCall app, List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs) {
      Contract.Requires(app != null);
      Contract.Requires(cce.NonNullElements(args));
      Contract.Requires(cce.NonNullElements(typeArgs));
      Contract.Assert(app.Func != null);    // resolution must have happened

      lock (app.Func)
      {
        if (app.Func.doingExpansion)
        {
          System.Console.WriteLine("*** detected expansion loop on {0}", app.Func);
          return null;
        }

        var exp = app.Func.Body;
        if (exp == null)
          return null;

        VCExpr/*!*/ translatedBody;
        VCExprSubstitution/*!*/ subst = new VCExprSubstitution();
        try
        {
          BaseTranslator.PushFormalsScope();
          BaseTranslator.PushBoundVariableScope();
          app.Func.doingExpansion = true;

          // first bind the formals to VCExpr variables, which are later
          // substituted with the actual parameters
          var inParams = app.Func.InParams;
          for (int i = 0; i < inParams.Count; ++i)
            subst[BaseTranslator.BindVariable(inParams[i])] = args[i];

          // recursively translate the body of the expansion
          translatedBody = BaseTranslator.Translate(exp);
        }
        finally
        {
          BaseTranslator.PopFormalsScope();
          BaseTranslator.PopBoundVariableScope();
          app.Func.doingExpansion = false;
        }

        // substitute the formals with the actual parameters in the body
        var tparms = app.Func.TypeParameters;
        Contract.Assert(typeArgs.Count == tparms.Count);
        for (int i = 0; i < typeArgs.Count; ++i)
          subst[tparms[i]] = typeArgs[i];
        SubstitutingVCExprVisitor/*!*/ substituter = new SubstitutingVCExprVisitor(Gen);
        return substituter.Mutate(translatedBody, subst);
      }
    }
  }
}