//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.IO;
using System.Diagnostics;
using System.Collections;
using System.Collections.Generic;
using System.Text;
using util;
using Microsoft.Contracts;
using Microsoft.Boogie;
using Microsoft.Boogie.Simplify;
using Microsoft.Basetypes;

// Simplified interface to an external prover like Simplify or the z3 process, taken from Bird.
namespace Microsoft.Boogie.Z3
{
  internal class Z3ProverProcess : ProverProcess {
    [Peer] private Z3InstanceOptions! opts;
    [Peer] private readonly Inspector? inspector;
    private readonly bool expectingModel = false;

    private string! cmdLineArgs = "";
    class OptionValue {
      public readonly string! Option;
      public readonly string! Value;
      public OptionValue(string! option, string! value) { Option = option; Value = value; }
    }
    static void AddOption(List<OptionValue!>! parms, string! option, string! value)
      modifies parms.*;
    {
      OptionValue ov = new OptionValue(option, value);
      Owner.AssignSame(ov, Owner.ElementProxy(parms));
      parms.Add(ov);
    }
    private List<OptionValue!>! parameterSettings;

    // [NotDelayed]
    [Captured]
    public Z3ProverProcess(Z3InstanceOptions! opts, Inspector? inspector)
      requires inspector != null ==> Owner.Same(opts, inspector);
    { // throws ProverException
      string! z3args = OptionChar() + "si";
      List<OptionValue!> parms = new List<OptionValue!>();

      if (opts.V2) {
        AddOption(parms, "MODEL_PARTIAL", "true");
        AddOption(parms, "MODEL_VALUE_COMPLETION", "false");
        AddOption(parms, "MODEL_HIDE_UNUSED_PARTITIONS", "false");
        AddOption(parms, "MODEL_V1", "true");
        AddOption(parms, "ASYNC_COMMANDS", "false");
      } else {
        AddOption(parms, "PARTIAL_MODELS", "true");
        AddOption(parms, "MODEL_VALUE_COMPLETION", "false");
        AddOption(parms, "HIDE_UNUSED_PARTITIONS", "false");
      }

      if (opts.V2) {
        // Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.
        // The restart parameters change the restart behavior to match Z3 v1, which also seems to be good.
        AddOption(parms, "PHASE_SELECTION", "0");
        AddOption(parms, "RESTART_STRATEGY", "0");
        AddOption(parms, "RESTART_FACTOR", "|1.5|");

        // This is used by VCC, but could be also useful for others, if sk_hack(foo(x)) is included as trigger,
        // the foo(x0) will be activated for e-matching when x is skolemized to x0.
        AddOption(parms, "NNF_SK_HACK", "true");

        // More or less like MAM=0.
        AddOption(parms, "QI_EAGER_THRESHOLD", "100");
        // Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more.

        // Make the integer model more diverse by default, speeds up some benchmarks a lot.
        AddOption(parms, "ARITH_RANDOM_INITIAL_VALUE", "true");

        // The left-to-right structural case-splitting strategy.
        AddOption(parms, "SORT_AND_OR", "false");
        AddOption(parms, "CASE_SPLIT", "3");

        // In addition delay adding unit conflicts.
        AddOption(parms, "DELAY_UNITS", "true");
        AddOption(parms, "DELAY_UNITS_THRESHOLD", "16");

        if (opts.Inspector != null) {
          AddOption(parms, "PROGRESS_SAMPLING_FREQ", "100");
        }
      } else {
        z3args += " " + OptionChar() + "mam:" + CommandLineOptions.Clo.Z3mam;
      }
      
      if (CommandLineOptions.Clo.z3AtFlag) {
		z3args += " " + OptionChar() + "@ ";
	  }
      if (0 <= CommandLineOptions.Clo.ProverCCLimit) {
        z3args += " " + OptionChar() + "cex:" + CommandLineOptions.Clo.ProverCCLimit;
      }
      if (0 <= opts.Timeout) {
        z3args += " " + OptionChar() + "t:" + opts.Timeout;
      }
      if (opts.Typed) {
        AddOption(parms, "TYPE_CHECK", "true");
        if (opts.BitVectors == CommandLineOptions.BvHandling.Z3Native) {
          if (opts.V2) {
            AddOption(parms, "BV_REFLECT", "true");
          } else {
            AddOption(parms, "REFLECT_BV_OPS", "true");
          }
        }
      }
      if (CommandLineOptions.Clo.PrintErrorModel >= 1 || 
          CommandLineOptions.Clo.EnhancedErrorMessages == 1 || 
          CommandLineOptions.Clo.ContractInfer ||
          CommandLineOptions.Clo.LazyInlining) {
        z3args += " " + OptionChar() + "m";
        expectingModel = true;
      }
      // Z3 version 1.3 does not support SETPARAMETER in the input, so we tack on the OPTION=value pairs to z3args
      if (opts.V1) {
        foreach (OptionValue opt in parms) {
          z3args += string.Format(" \"{0}={1}\"", opt.Option, opt.Value);
        }
      }
      
      foreach (string! opt in CommandLineOptions.Clo.Z3Options) {
        int eq = opt.IndexOf("=");
        // we add them both to command line and the input file:
        //    - allow for overriding default options
        //    - some options (like TRACE) work only from command line
        // Also options with spaces do not work with (SETPARAMETER ...)
        if (eq > 0 && opt.IndexOf(" ") < 0 && 'A' <= opt[0] && opt[0] <= 'Z') {
          AddOption(parms, opt.Substring(0, eq), opt.Substring(eq + 1));
        }
        z3args += " \"" + opt + "\"";
      }

      
      cmdLineArgs = z3args;
      parameterSettings = parms;
      
      ProcessStartInfo! psi = new ProcessStartInfo(opts.ExeName, z3args);
      psi.CreateNoWindow = true;
      psi.UseShellExecute = false;
      psi.RedirectStandardInput = true;
      psi.RedirectStandardOutput = true;
      psi.RedirectStandardError = true;
      
      base(psi, opts.ExeName);

      Owner.AssignSame(this, opts);
      this.opts = opts;
      this.inspector = inspector;
    }
    
    public override string! OptionComments()
    {
      StringBuilder sb = new StringBuilder();
      sb.AppendFormat("Z3 command line: {0} {1}\nUser supplied Z3 options:",
                      opts.ExeName, cmdLineArgs);
      assume CommandLineOptions.Clo.IsPeerConsistent;
      foreach (string! opt in CommandLineOptions.Clo.Z3Options) {
        sb.Append(" ").Append(opt);
      }
      sb.AppendFormat("\nProver options: {0}\n", opts.ToString());
      return sb.ToString();
    }

    [Pure(false)]
    public override IEnumerable<string!>! ParameterSettings {
      get {
        if (opts.V2) {
          foreach (OptionValue opt in parameterSettings) {
            yield return "(SETPARAMETER " + opt.Option + " " + opt.Value + ")";
          }
        }
      }
    }

    // z3 uses different magic characters for options on linux/unix and on windows
    private static string! OptionChar() {
      assume Environment.OSVersion != null;
      switch (Environment.OSVersion.Platform) {
        case PlatformID.Unix:
          return "-";
        default:
          return "/";
      }
    }

    protected override void DoBeginCheck(string! descriptiveName, string! formula)
    {
      ToWriteLine(formula);
      ToWriteLine(String.Format(";   END OF FORMULA {0} - {1}", NumFormulasChecked.ToString(), descriptiveName));
      ToFlush();
    }

    protected int TimedFromReadChar()
    {
      if (opts.Timeout > 0)
        return FromReadChar((opts.Timeout + 1) * 1000);
      else
        return FromReadChar();
    }

    private void Trace(string! msg)
    { 
      Console.WriteLine("Z3: " + msg);
    }

    public override ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler! handler) 
      throws UnexpectedProverOutputException;
    {
      ProverOutcome outcome;
      bool isInvalid = false;

      if (this.simplify == null) {
        return ProverOutcome.Inconclusive;
      }


      while (true) {
        int ch = TimedFromReadChar();
        if (ch == -1 && this.readTimedOut) {
          handler.OnResourceExceeded("timeout (forced)");
          return ProverOutcome.TimeOut;
        }

        string line = new string((char)ch, 1) + FromReadLine();

        if (line.StartsWith("STATS ")) {
          if (inspector != null) {
            inspector.StatsLine(line);
          }
          continue;
        }

        if (opts.Verbosity > 2) {
          Trace("INPUT: " + line);
        }

		if (line.StartsWith("WARNING: Out of allocated virtual memory.")) {
		  handler.OnResourceExceeded("memory");
		  return ProverOutcome.OutOfMemory;
		}


        if (line.StartsWith("WARNING: ")) {
          string w = line.Substring(9);
          handler.OnProverWarning(w);
          continue;
        }

        if (line.ToUpper().StartsWith("ERROR")) {
          Console.WriteLine("Z3 returns the following error:");
          Console.WriteLine("    " + line);
          return ProverOutcome.Inconclusive;
        }

        int beg = 0;
        while (beg < line.Length && '0' <= line[beg] && line[beg] <= '9')
          invariant beg <= line.Length;
        {
          beg++;
        }

        if (beg > 0 && line.Substring(beg).StartsWith(": ")) {
          string status = line.Substring(beg + 2);

          if (status.StartsWith("Valid")) {
            return ProverOutcome.Valid;
          }

          if (status.StartsWith("Timeout")) {
            handler.OnResourceExceeded("timeout");
            return ProverOutcome.TimeOut;
          }

          if (status.StartsWith("Inconclusive")) {
            return ProverOutcome.Inconclusive;
          }

          if (status.StartsWith("Memout")) {
            handler.OnResourceExceeded("memory");
            return ProverOutcome.OutOfMemory;
          }

          if (status.StartsWith("Invalid")) {
            isInvalid = true;
            continue;
          }
        }

        if (isInvalid && line == ".") {
          return ProverOutcome.NotValid;
        }

        if (isInvalid && line.StartsWith("labels: (")) {
          List<string!>! l = ParseLabels(line);
          Z3ErrorModel errModel = null;
          if (expectingModel) {
            if (opts.Verbosity > 2) {
              Trace("waiting for model");
            }
            line = FromReadLine();
            if (line.StartsWith("partitions:")) {
              line = ParseModel(out errModel);
              if (opts.Verbosity > 2) {
                Trace("model parsed, final line " + line);
              }
              // Z3 always ends the model with END_OF_MODEL, not with labels: or .
              assume line == "END_OF_MODEL";
            } else {
              throw new UnexpectedProverOutputException(string.Format("evil input from z3 (expecting partitions): '{0}'", line));
            }
          }
          handler.OnModel(l, errModel);
          continue;
        }

        throw new UnexpectedProverOutputException(string.Format("evil input from z3: '{0}'", line));
      }
    }
  
    /* ----------------------------------------------------------------------------
    BNF Grammar to parse Z3 output, including the model generated when using the /m /si switch:

    Output  ::= VC*
    VC      ::= number ": " "Valid." | number ": " "Inconclusive" | VCI
    VCI     ::= number ": " "Invalid"
                ("labels: " "(" ID* ")"
                [MODEL] "END_OF_MODEL")+
                "."
    MODEL   ::= MBOOL MFUNC
    MBOOL   ::= "boolean assignment:"
                "partitions:"
                MAPPING*
    MAPPING ::= ZID ["{" ID+"}"] ["->" "(" (number | false | true | BITVECTOR) ")"]
    BITVECTOR ::= ulong ":bv" int
    MFUNC   ::= "function interpretations:"
                F*
    F       ::= Id "->" "{"
                MAPLET*
                "else" "->" ZID
                "}"
    MAPLET  ::= ZID* "->" ZID

    -----------------------------------------------------------------------------*/
    private string! ParseModel(out Z3ErrorModel errModel) 
      modifies this.*;
      ensures result == "." || result.StartsWith("labels: (") || result == "END_OF_MODEL";
      throws UnexpectedProverOutputException;
    {
      //Format in the grammar:
      // ZID ["{" ID+"}"] ["->" "(" (number | false | true) ")"]
      // storing the model:
      // map each ID (a string) to the corresping ZID (an integer) in a dictionary:
      Dictionary<string!, int> identifierToPartition = new Dictionary<string!, int>();
      // map each ZID to the set (in list form) of IDs belonging to it (possibly empty):
      List<List<string!>> partitionToIdentifiers = new List<List<string!>>();
      // map each ZID to the number or boolean given, if any:
      List<Object> partitionToValue = new List<Object>();
      // map each value (number or boolean) to the ZID, reverse map of partitionToValue
      Dictionary<Object, int> valueToPartition = new Dictionary<Object, int>();
      Owner.AssignSame(Owner.ElementProxy(partitionToValue), Owner.ElementProxy(valueToPartition));

      int ch;

      // read the MAPPING
      for (int zID = 0; true; zID++)
      {
        ch = FromReadChar();
        if (ch == 'f') {
          break;
        }
        ParseModelMapping(zID, identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition);
      }// end MAPPING

      // add the fake partition for the 'else -> #undefined' clause
      List<string!> emptyList = new List<string!>();
      Owner.AssignSame(emptyList, Owner.ElementProxy(partitionToIdentifiers));
      partitionToIdentifiers.Add(emptyList);
      partitionToValue.Add(null);

      // continue in ParseModelFunctions, which breaks up this long method and enables its verification
      return ParseModelFunctions(ch, out errModel, identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition);
    }

    private void ParseModelMapping(int zID,
        Dictionary<string!, int>! identifierToPartition,
        List<List<string!>>! partitionToIdentifiers,
        List<Object>! partitionToValue,
        Dictionary<Object, int>! valueToPartition)
      requires Owner.Same(Owner.ElementProxy(partitionToValue), Owner.ElementProxy(valueToPartition));
      modifies this.*, identifierToPartition.*, partitionToIdentifiers.*, partitionToValue.*, valueToPartition.*;
    {
      string s = FromReadLine();
      {
        // sanity check
        int pos = s.IndexOf(' ');
        string n = s;
        int k;
        if (pos >= 0) {
          n = s.Substring(0,pos);
        }
        if (! (int.TryParse(n, out k) && zID == k)) {
          System.Console.WriteLine("mismatch: {0}!={1} '{2}'", zID, k, s);
          assume false;
        }
      }
      
      int j = ParseModelZidAndIdentifiers(zID, s, identifierToPartition, partitionToIdentifiers);
      
      j = s.IndexOf(" -> ", j);
      if (0 <= j) {
        j += 4;
      }
      assume j == -1 || j < s.Length;  // if ' -> ' is present, then more should remain of the line
      if (j == -1) {
        // no "-> " found, end of this line, store that there is no value:
        partitionToValue.Add(null);
        int idForNull;
        if (identifierToPartition.TryGetValue("nullObject", out idForNull) && idForNull == zID) {
          assume !valueToPartition.ContainsKey("nullObject");  // a RHS value should occur only once in the Z3 output
          valueToPartition.Add("nullObject", zID);
          // In this case partitionToValue (as the reverse of valueToPartition) should include
          // a map from zID -> "nullObject", but doing that breaks printing out the model as 
          // it is printed out by Z3. Also, that information is not required, valueToPartition
          // works well enough by itself.
        }
        
      } else if (s[j] == 't'/*rue*/) {
        partitionToValue.Add(true);
        object boxedTrue = true;
        assume !valueToPartition.ContainsKey(boxedTrue);  // a RHS value should occur only once in the Z3 output
        valueToPartition.Add(boxedTrue, zID);
      } else if (s[j] == 'f'/*alse*/) {
        object boxedFalse = false;
        Owner.AssignSame(boxedFalse, Owner.ElementProxy(partitionToValue));
        partitionToValue.Add(boxedFalse);
        assume !valueToPartition.ContainsKey(boxedFalse);  // a RHS value should occur only once in the Z3 output
        valueToPartition.Add(boxedFalse, zID);
      } else if (s[j] == 'v') {
        // -> val!..., i.e. no value
        partitionToValue.Add(null);
      } else if (s[j] == '{') {
        // array
        List<List<int>!> arrayModel = new List<List<int>!>();
        string array = s.Substring(j+1);
        int index1, index2;
        string from, to;
        List<int> tuple = new List<int>();
        while (0 <= array.IndexOf(';')) {
          index1 = array.IndexOf('*') + 1;
          index2 = array.IndexOf(' ');
          from = array.Substring(index1, index2-index1);
          tuple.Add(int.Parse(from));
          array = array.Substring(index2);
          index1 = array.IndexOf('*') + 1;
          index2 = array.IndexOf(';');
          to = array.Substring(index1, index2-index1);
          array = array.Substring(index2+2);
          tuple.Add(int.Parse(to));
          arrayModel.Add(tuple);
          tuple = new List<int>();
        }
        assert array.StartsWith("else ->");
        index1 = array.IndexOf('*') + 1;
        index2 = array.IndexOf('}');
        to = array.Substring(index1, index2-index1);
        tuple.Add(int.Parse(to));
        arrayModel.Add(tuple);
        partitionToValue.Add(arrayModel);
      } else {
        string numberOrBv = s.Substring(j);
        // make number an int, then store it:
        BigNum bvVal;
        int bvSize;
        string number, type;

        int l = numberOrBv.IndexOf(':', 0);
        if (0 <= l) {
          number = numberOrBv.Substring(0, l);
          type = numberOrBv.Substring(l + 1);
        } else {
          l = numberOrBv.IndexOf('[', 0);
          if (0 <= l) {
            number = numberOrBv.Substring(2, l-2);
            int closingBracePosition = numberOrBv.IndexOf(']', l);
            if (l < closingBracePosition)
              type = "bv" + numberOrBv.Substring(l + 1, closingBracePosition - l - 1);
            else type = "int";
          } else {
            number = numberOrBv;
            type = "int";
          }
        }

        if (type == "int") {
          object boxedN = BigNum.FromString(number);
          assume Owner.None(boxedN);
          Owner.AssignSame(boxedN, Owner.ElementProxy(partitionToValue));
          partitionToValue.Add(boxedN);
          assume !valueToPartition.ContainsKey(boxedN);  // a RHS value should occur only once in the Z3 output
          valueToPartition.Add(boxedN, zID); 
        } else if (type.StartsWith("bv") && BigNum.TryParse(number, out bvVal) && int.TryParse(type.Substring(2), out bvSize)) {
          BvConst bitV = new BvConst(bvVal, bvSize);
          Owner.AssignSame(bitV, Owner.ElementProxy(partitionToValue));
          partitionToValue.Add(bitV);
          assume !valueToPartition.ContainsKey(bitV);  // a RHS value should occur only once in the Z3 output
          valueToPartition.Add(bitV, zID);
        } else {
          System.Console.WriteLine("cannot parse type: '{0}':'{1}'", number, type);
          assume false;
        }

      }
    }

    private static int ParseModelZidAndIdentifiers(int zID, string! s,
        Dictionary<string!, int>! identifierToPartition,
        List<List<string!>>! partitionToIdentifiers)
      modifies identifierToPartition.*, partitionToIdentifiers.*;
      ensures 0 <= result && result <= s.Length;
    {
      List<string!> identifiers = new List<string!>();
      int arrowIndex = s.IndexOf('>');
      assert 0 < arrowIndex;
      int j = s.IndexOf('{', 0) + 1;  // skip the '{', if present, and set j to 0 otherwise
      if (1 <= j && j < arrowIndex) {
        // There is a list of ID's.
        assume j < s.Length;  // there should be more characters; the ending '}', for one
        //ID*
        while (true) 
          invariant identifiers.IsPeerConsistent && identifierToPartition.IsPeerConsistent && partitionToIdentifiers.IsPeerConsistent;
          invariant 0 <= j && j < s.Length;
        {
          int k = s.IndexOfAny(new char[]{' ', '}'}, j);
          assume j <= k;
          string id = s.Substring(j, k-j);
          j = k+1;
          assume !identifierToPartition.ContainsKey(id);  // an ID is listed only once in this list, and an ID can only belong to one ZID equivalence class
          identifierToPartition.Add(id, zID);
          identifiers.Add(id);
          if (s[k] == '}') {
            // end of reading ID*
            break;
          }
          assume j < s.Length;  // there should be more characters; the ending '}', for one
        }//end ID*
      } else {
        j = 0;
      }
      Owner.AssignSame(identifiers, Owner.ElementProxy(partitionToIdentifiers));
      partitionToIdentifiers.Add(identifiers);
      return j;
    }
                  
    private string! ParseModelFunctions(int ch, out Z3ErrorModel errModel,
      Dictionary<string!, int>! identifierToPartition,
      List<List<string!>>! partitionToIdentifiers,
      List<Object>! partitionToValue,
      Dictionary<Object, int>! valueToPartition
    ) 
      modifies this.*;
      ensures result == "." || result.StartsWith("labels: (") || result == "END_OF_MODEL";
      throws UnexpectedProverOutputException;
    {
      // read the function F
      Expect(ch, "function interpretations:");
      FromReadLine();
      
      // mapping of function names to function definitions
      Dictionary<string!, List<List<int>>!> definedFunctions = new Dictionary<string!, List<List<int>>!>();
      // function definition given as list of 'pointwise definitions' in the form of the arguments and result
      // the last element here will always be a list with just one entry which corresponds to the else case
      List<List<int>> functionDefinition = new List<List<int>>();
      // list of arguments, followed by the result, the last element of this list is always the result
      List<int> argumentsAndResult = new List<int>();
      
      // read F
      while (true) 
      {
        functionDefinition = new List<List<int>>();
        string s = FromReadLine();
        // end of F, "END_OF_MODEL" ends model, '.' ends whole VC, 'l' starts a new set of labels and model
        //           whenever there is a model this will end with "END_OF_MODEL", the other cases can only
        //           happen when there is no model printed!
        if (s == "." || s.StartsWith("labels: (") || s == "END_OF_MODEL") {
          errModel = new Z3ErrorModel(identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition, definedFunctions);
          return s;
        }
        int j = s.IndexOf(' ', 0);
        assume 0 <= j;
        string id = s.Substring(0, j);
        // id is stored into definedFunctions once the function definition for it has 
        // been completely parsed, 
        
        // just ignore the "-> {" by dropping string s
        string zIDstring;
        
        // MAPLET
        while (true) 
        {
          argumentsAndResult = new List<int>();
          // remove the 2 spaces that are here
          FromReadChar();
          FromReadChar();
          s = FromReadLine();
          if (s.StartsWith("else ->")) break;
          j = 0;
          
          //ZID*
          while(true) 
            invariant 0 <= j && j <= s.Length;
          {
            j = s.IndexOfAny(new Char[]{'*', '-'}, j);
            // true because this always ends with a "->":
            assume 0 <= j;
            
            // reading -> means end of ZID*
            if (s[j] == '-'/*>*/) break;
            
            // start reading the ZID* with the number, not the *
            j = j + 1;
            // by input string format:
            assume j < s.Length;
            int k = s.IndexOf(' ', j);
            // by input string format:
            assume j <= k;
            zIDstring = s.Substring(j, k-j);
            // add the arguments
            argumentsAndResult.Add(int.Parse(zIDstring));
            j = k;
          }// end ZID*
          
          // j is the beginning of "-> *", we want the first character after this
          j = j + 4;
          // by input string format:
          assume j <= s.Length;
          zIDstring = s.Substring(j);
          // add the result
          argumentsAndResult.Add(int.Parse(zIDstring));
          // add the input line as another 'pointwise defined' element to the functions definition
          functionDefinition.Add(argumentsAndResult);
        }// end MAPLET

        // this is the 'else -> #unspecified' case
        // by input string format:
        assume s.IndexOf("#unspec") >= 0;
        // this stores the else line as another argumentsAndResult list
        argumentsAndResult = new List<int>();
        argumentsAndResult.Add(partitionToIdentifiers.Count - 1); // use the fake partition we have created before
        // which is then added to the function definition, which is now complete
        Owner.AssignSame(argumentsAndResult, Owner.ElementProxy(functionDefinition));
        functionDefinition.Add(argumentsAndResult);

    /*
        // this is the 'else -> *' case, that string is already in s
        j = s.IndexOf('*', 0) + 1;
        // by input string format:
        assume 0 < j && j < s.Length;
        zIDstring = s.Substring(j);
        // this stores the else line as another argumentsAndResult list
        argumentsAndResult = new List<int>();
        argumentsAndResult.Add(int.Parse(zIDstring));
        // which is then added to the function definition, which is now complete
        functionDefinition.Add(argumentsAndResult); */

        // and therefore added to the map of defined functions, together with the name 'id'
        // which had been extracted before
        assume !definedFunctions.ContainsKey(id);  // each function name in the model is listed only once
        definedFunctions.Add(id, functionDefinition);
        
        // read the line with "}"
        ch = FromReadChar();
        Expect(ch, "}");
        FromReadLine();
      }// end F
    }

  }


  public class Z3ErrorModel : ErrorModel 
  {
    public Z3ErrorModel(Dictionary<string!, int>! identifierToPartition, List<List<string!>>! partitionToIdentifiers, List<Object>! partitionToValue, Dictionary<object, int>! valueToPartition, Dictionary<string!, List<List<int>>!>! definedFunctions)
      : base(identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition, definedFunctions)
    {
      this.partitionNames = new string?[partitionToIdentifiers.Count];
      this.prevPartitionNames = new string?[partitionToIdentifiers.Count];
    }

    private string?[]! partitionNames;
    private string?[]! prevPartitionNames;

    private void SetNames()
    {
      int len = partitionToIdentifiers.Count;
      for (int i = 0; i < 3; ++i) { // let the names stabilize a bit
        prevPartitionNames = partitionNames;
        partitionNames = new string?[len];
        for (int pos = 0; pos < len; ++pos)
          GetPartitionName(pos);
      }
    }

    private int NameBadness(string! name)
    {
      int badness = name.Length;
      if (name.StartsWith("call") && name.IndexOf("formal@") > 0)
        badness += 1000;
      if (name.IndexOf ("(") > 0)
        badness += 500;
      return badness;
    }

    private string! GetPartitionName(int pos)
    {
      string name = partitionNames[pos];
      if (name != null) {
        return name;
      }

      object tmp = partitionToValue[pos];
      if (tmp != null) {
        partitionNames[pos] = tmp is BvConst ?  ((BvConst)tmp).ToReadableString() : tmp.ToString();
      } else {
        List<string!>! possible_names = new List<string!>();
        List<string!> pti = partitionToIdentifiers[pos];

        // make sure we're not called recursively
        string prevName = prevPartitionNames[pos];
        if (prevName == null) prevName = "*" + pos;
        partitionNames[pos] = prevName;

        if (pti != null && pti.Count > 0) {
          // add identifiers
          foreach (string! name in pti)
            possible_names.Add(name);
        }

        // Then also look for functions,
        // and then collect possible functional definitions
        foreach (KeyValuePair<string!, List<List<int>>!> kv in definedFunctions) {
          foreach (List<int>! parms in kv.Value) {
            if (parms.Count > 1 && parms[parms.Count - 1] == pos) {
              string! s = kv.Key + "(";
              for (int i = 0; i < parms.Count - 1; ++i) {
                if (i != 0) s += ", ";
                s += GetPartitionName(parms[i]);
              }
              s += ")";
              possible_names.Add(s);
            }
          }
        }

        // choose the shortest possible name
        if (possible_names.Count > 0) {
          string! best = possible_names[0];
          foreach (string! s in possible_names)
            if (NameBadness(s) < NameBadness(best)) best = s;
          if (best.Length < 120)
            partitionNames[pos] = best;
        }
      }

      return (!)partitionNames[pos];
    }
    
    private void PrintReadableModel (TextWriter! writer) {
      writer.WriteLine("Z3 error model: ");
      SetNames();
      writer.WriteLine("partitions:");
      assert partitionToIdentifiers.Count == partitionToValue.Count;
      for (int i = 0; i < partitionToIdentifiers.Count; i++){
        writer.Write("{0,5}: {1}  ", "*"+i, GetPartitionName(i));
        List<string!> pti = partitionToIdentifiers[i];
        if (pti != null && (pti.Count > 1 || (pti.Count == 1 && partitionToValue[i] != null))) {
          writer.Write("{");
          for (int k = 0; k < pti.Count - 1; k ++) {
            writer.Write(pti[k] + " ");
          }
          //extra work to make sure no " " is at the end of the list of identifiers
          if (pti.Count != 0) {
            writer.Write(pti[pti.Count - 1]);
          }
          writer.Write("}");
        }
        writer.WriteLine();
      }

      writer.WriteLine();
      writer.WriteLine("function interpretations:");
      List<string!> funNames = new List<string!>(definedFunctions.Keys);
      funNames.Sort();
      foreach (string! name in funNames) {
        if (definedFunctions[name].Count == 1) continue; // skip functions with only the else-> clause
        foreach (List<int>! parms in definedFunctions[name]) {
          string! s = name + "(";
          if (parms.Count == 1) {
            continue;
            // s += "*";
          } else {
            for (int i = 0; i < parms.Count - 1; ++i) {
              if (i != 0) s += ", ";
              s += GetPartitionName(parms[i]);
            }
          }
          s += ")";
          string! res = GetPartitionName(parms[parms.Count - 1]);
          if (res == s)
            res = "*" + parms[parms.Count - 1] + " (SELF)";
          writer.WriteLine("{0} = {1}", s, res);
        }
        writer.WriteLine();
      }
      writer.WriteLine("The end.");
      writer.WriteLine();
    }

    public override void Print (TextWriter! writer) {
      if (CommandLineOptions.Clo.PrintErrorModel == 4) {
        PrintReadableModel(writer);
        return;
      }

      writer.WriteLine("Z3 error model: ");

      writer.WriteLine("partitions:");
      assert partitionToIdentifiers.Count == partitionToValue.Count;
      for (int i = 0; i < partitionToIdentifiers.Count; i++){
        writer.Write("*"+i);
        List<string!> pti = partitionToIdentifiers[i];
        if (pti != null && pti.Count != 0) {
          writer.Write(" {");
          for (int k = 0; k < pti.Count - 1; k ++) {
            writer.Write(pti[k] + " ");
          }
          //extra work to make sure no " " is at the end of the list of identifiers
          if (pti.Count != 0) {
            writer.Write(pti[pti.Count - 1]);
          }
          writer.Write("}");
        }
        // temp object needed for non-null checking
        object tempPTVI = partitionToValue[i];
        if (tempPTVI != null) {
          if (tempPTVI.ToString() == "True") {
            writer.Write(" -> " + "true" + "");
          } else if (tempPTVI.ToString() == "False") {
            writer.Write(" -> " + "false" + "");
          } else if (tempPTVI is BigNum) {
            writer.Write(" -> " + tempPTVI + ":int");
          } else if (tempPTVI is List<List<int>!>) {
            List<List<int>!> array = tempPTVI as List<List<int>!>;
            assume array != null;
            writer.Write(" -> {");
            foreach(List<int> l in array) {
              if (l.Count == 2) {
                writer.Write("*"+l[0] + " -> " + "*"+l[1] + "; ");
              } else {
                assert (l.Count == 1);
                writer.Write("else -> *"+l[0]+"}");
              } 
            }
          } else {
            writer.Write(" -> " + tempPTVI + "");
          }
        } else {
          writer.Write(" ");
        }
        writer.WriteLine();
      }

      writer.WriteLine("function interpretations:");
      foreach (KeyValuePair<string!, List<List<int>>!> kvp in definedFunctions) {
        writer.WriteLine(kvp.Key + " -> {");
        List<List<int>> kvpValue = kvp.Value;
        if (kvpValue != null) {
          foreach(List<int> l in kvpValue) {
            writer.Write("  ");
            if (l != null) {
              for (int i = 0; i < l.Count - 1; i++) {
                writer.Write("*"+l[i] + " ");
              }
              if (l.Count == 1) {
                writer.WriteLine("else -> #unspecified");
              } else {
                writer.WriteLine("-> "+ "*" + l[l.Count - 1]);
              }
            }
          }
        }
        writer.WriteLine("}");
      }
      writer.WriteLine("END_OF_MODEL");
      writer.WriteLine(".");
      
      if (CommandLineOptions.Clo.PrintErrorModel >= 2) {
        writer.WriteLine("identifierToPartition:");
        foreach (KeyValuePair<string!, int> kvp in identifierToPartition) {
          writer.WriteLine(kvp.Key + " : " + "*" + kvp.Value);  
        }
        
        writer.WriteLine("valueToPartition:");
        foreach (KeyValuePair<object, int> kvp in valueToPartition) {
          writer.WriteLine(kvp.Key + " : " + "*" + kvp.Value);
        }
        writer.WriteLine("End of model.");
      }
    }
  }


}