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


namespace Microsoft.Boogie {

  public class ProverOptions
  {
    public class OptionException : Exception {
      public OptionException(string! msg) { base(msg); }
    }

    public string/*?*/ LogFilename = null;
    public bool AppendLogFile = false;
    public bool SeparateLogFiles = false;
    // Say (DBG_WAS_VALID) or (DBG_WAS_INVALID) after query
    public bool ForceLogStatus = false;
    public int TimeLimit = 0;
    public int MemoryLimit = 0;
    public CommandLineOptions.BvHandling BitVectors = CommandLineOptions.BvHandling.None;
    public int Verbosity = 0;

    private string! stringRepr = "";

    [Pure]
    public override string! ToString()
    {
      return stringRepr;
    }

    // The usual thing to override.
    protected virtual bool Parse(string! opt)
    {
      return ParseString(opt, "LOG_FILE", ref LogFilename) ||
             ParseBool(opt, "APPEND_LOG_FILE", ref AppendLogFile) ||
             ParseBool(opt, "FORCE_LOG_STATUS", ref ForceLogStatus) ||
             ParseInt(opt, "MEMORY_LIMIT", ref MemoryLimit) ||
             ParseInt(opt, "VERBOSITY", ref Verbosity) ||
             ParseInt(opt, "TIME_LIMIT", ref TimeLimit);
             // || base.Parse(opt)
    }

    public virtual void Parse(List<string!>! opts)
    {
      StringBuilder! sb = new StringBuilder(stringRepr);
      foreach (string! opt in opts) {
        if (!Parse(opt)) {
          ReportError("Unrecognised prover option: " + opt);
        }
        sb.Append(opt).Append(" ");
      }
      stringRepr = sb.ToString();
      PostParse();
    }

    protected virtual void PostParse()
    {
      if (LogFilename != null && LogFilename.Contains("@PROC@")) {
        SeparateLogFiles = true;
      }
    }

    protected void ReportError(string! msg)
    {
      throw new OptionException(msg);
    }

    protected virtual bool ParseString(string! opt, string! name, ref string field)
    {
      if (opt.Length >= name.Length && opt.StartsWith(name)) {
        if (opt.Length == name.Length) {
          field = "";
          return true;
        } else if (opt[name.Length] == '=') {
          field = opt.Substring(name.Length + 1);
          return true;
        }
      }
      return false;
    }

    protected virtual bool ParseBool(string! opt, string! name, ref bool field)
    {
      string tmp = null;
      if (ParseString(opt, name, ref tmp))
        switch (((!)tmp).ToLower()) {
        case "1":
        case "true":
        case "":
          field = true;
          return true;
        case "0":
        case "false":
          field = false;
          return true;
        default:
          ReportError("Invalid Boolean option \"" + opt + "\"");
          return false;
        }
      return false;
    }

    protected virtual bool ParseInt(string! opt, string! name, ref int field)
    {
      string tmp = null;
      int t2;
      if (ParseString(opt, name, ref tmp)) {
        if (int.TryParse((!)tmp, out t2)) {
          field = t2;
          return true;
        } else {
          ReportError("Invalid integer option \"" + opt + "\"");
        }
      }
      return false;
    }

    static int sequenceNumber = 0;
    public virtual TextWriter? OpenLog(string/*?*/ descName)
    {
      if (LogFilename != null) {
        string! filename = LogFilename;
        if (descName != null)
          filename = Helpers.SubstituteAtPROC(descName, filename);
        return new StreamWriter(filename, AppendLogFile);
      } else {
        return null;
      }
    }
  }

  public abstract class ProverFactory
  {
    // Really returns ProverInterface.
    //public abstract object! SpawnProver(ProverOptions! options, object! ctxt);
    public abstract object SpawnProver(ProverOptions options, object ctxt);

    // Really returns ProverContext
    public abstract object! NewProverContext(ProverOptions! options);

    public virtual ProverOptions! BlankProverOptions()
    {
      return new ProverOptions();
    }

    // return true if the prover supports DAG AST as opposed to LET AST
    public virtual bool SupportsDags
    {
      get { return false; }
    }

    public virtual CommandLineOptions.VCVariety DefaultVCVariety
    {
      get 
        ensures result != CommandLineOptions.VCVariety.Unspecified;
        { return CommandLineOptions.VCVariety.Dag; }
    }

    public virtual void Close()
    {
    }

    public static ProverFactory! Load(string! proverName)
      ensures result.IsNew && Microsoft.Contracts.Owner.New(result);
    {
      string! path;
      if (proverName.IndexOf("/") > 0 || proverName.IndexOf("\\") > 0) {
        path = proverName;
      } else {
        string! codebase = (!) System.IO.Path.GetDirectoryName(
                                 (!)System.Reflection.Assembly.GetExecutingAssembly().Location);
        path = System.IO.Path.Combine(codebase, "Provers." + proverName + ".dll");
      }
      Assembly asm = (!)Assembly.LoadFrom(path);
      string name = (!)asm.GetName().Name;
      System.Type factoryType = (!)asm.GetType("Microsoft.Boogie." + name.Replace("Provers.", "") + ".Factory");
      return (ProverFactory!)Activator.CreateInstance(factoryType);
    }
  }
}