using System.Console
using Nemerle.Collections
using Nemerle.Utility
using Nemerle.Logging
using Nemerle.Imperative
using Nemerle.Profiling

set namespace Fx7

public class Driver
  internal mutable static PrintResult : bool
  internal mutable static TimeLimit : int
  internal mutable static Verbose : bool
  internal mutable static Mechanical : bool
  internal mutable static NoStats : bool
  internal mutable static NoProgress : bool
  internal mutable static LogAfter : int
  internal mutable static LoggingEnabled : bool = true
  internal mutable static SimplifySyntax : bool
  internal mutable static ExpectAllValid : bool
  internal mutable static ExpectAllInvalid : bool
  internal mutable static PrettyPrint : bool
  internal mutable static Translate : bool
  internal mutable static SmtStartNo : int
  internal mutable static CsvName = "fx7_stats.csv"
  internal mutable static Strategies : list [int] // = [3]
  internal mutable static DoubleCheck : int = 0
  internal mutable static PrunerFile : string
  internal mutable static EnablePruner : bool


  // general flags
  [Option] EnableTcTheory = true
  [Option ("Display profile information")] \
  Profile = true
  [Option ("Dump statistics for quantifier instantiations")] \
  DumpQuantStats = false
  [Option ("Display additional quantifier information")] \
  VerboseQuant = false
  [Option] SelfChecks = false
  [Option] LogConflicts = ""
  [Option] ProofLogging = false
  [Option] CoqProofs = false
  [Option] ExpandProofs = false
  [Option] SkolProofs = true
  [Option] RunChecker = false

  [Option] InstProofs = true
  [Option] ResolutionProofs = true
  [Option] AndProofs = true
  [Option] OrProofs = true
  [Option] PrintDoneForProofs = false
  [Option] ProofFile = "proof.rw"

  // trigger generation flags
  [Option] LoopTest = true

  // matcher flags
  [Option] FlatMatching = true
  [Option] SimplifyMatching = false
  [Option] IncrementalSimplifyMatching = false
  [Option] FnLastMerge = false // cannot be set to true currently!

  // general search flags
  [Option (Depth)] MatchingDepth = 5
  [Option (CFC)] CheapFullCheck = true
  [Option (NLE)] NewLiteralExplanation = true // not implemented yet

  // literal ranking flags
  [Option] PosLitScore = 1.0
  [Option] NegLitScore = 1.0
  [Option] ScoreMult = 1.02
  [Option] DepthBonus = 5.0
  [Option (DCM)] DeepConflictMult = 1.0
  [Option (ALS)] AlternatingLiteralSelection = 0

  // promotion/important quantifiers flags
  [Option] HighRankingPromotion = 10
  [Option] MinHighRankingQA = 3
  [Option] MaxHighRankingQA = 5
  [Option (FIE)] FullInstantiationEvery = 4
  [Option] PromoteBackLog = 5

  // conflict handling
  [Option] MixConflicts = false
  [Option (LCE)] LeakConflictExpansions = false
  [Option (CP)] ConflictPromotion = false

  // restart flags
  [Option (SBR)] SpeedBasedRestarts = true
  [Option] SBR_Sample = 3
  [Option] SBR_Threshold = 2
  [Option] SBR_Flattening = 3
  [Option] SBR_Fadeout = 3

  [Option] FirstRestart = 0 //300
  [Option] NextRestartIn = 150
  [Option ("in %")] RestartHorizonMult = 150
 
  // Grinder flags
  [Option] EqProp = false
  [Option] GrindForall = false
  [Option] RealCNFThreshold = 5

  // Pruner flags
  [Option (DG)] DisableGrinder = false

  // SMT translation
  [Option] SmtComment = ""

  [Option] IgnoreTriggers = false

  internal mutable static Instance : Driver

  mutable static axiom_files : list [string] = []
  internal mutable static file_name : string = "stdin"
  mutable static cmd_line_options : string

  class TimeoutException : System.Exception {}

  start_time : int
  end_time : int

  // ForParser and Run
  mutable core : Core

  mutable result : string = ""
  mutable status : string = ""

  #region stats
  internal mutable clause_count : int
  internal mutable last_stat_at_tick : int = System.Environment.TickCount
  internal mutable last_stat_at_iter : int
  problem_name : string

  internal sizes : array [long] = array (4)
  total_sizes : array [long] = array (4)

  [AutoStats] num_case_splits : int
  [AutoStats] num_conflicts : int
  [AutoStats] instance_count : int
  [AutoStats] num_inst_rounds : int
  [AutoStats] num_empty_inst_rounds : int

  [AutoStats] num_asserts : int
  [AutoStats] num_matchings : int
  [AutoStats] num_noskips : int

  [AutoStats] conflicts_attempted : int
  [AutoStats] conflicts_added : int

  [AutoStats] subtrigger_flats : int
  [AutoStats] subtrigger_hits : int
  [AutoStats] subtrigger_misses : int
  [AutoStats] subtrigger_sub_hits : int
  [AutoStats] subtrigger_sub_misses : int
  [AutoStats] subtrigger_anything : int
  [AutoStats] subtrigger_nothing : int

  [AutoStats] num_merges : int
  [AutoStats] num_non_unit_merges : int
  [AutoStats] num_merge_hits : int
  [AutoStats] num_merge_misses : int

  // both filled by the AutoStats macro
  [AutoStats] internal GetStats () : list [string * string]
    {}
  internal class StatsRec
  {
  }

  [ProfDump] static DumpProf () : void
    {}

  #region prover option book-keeping
  static RegisterOptions () : void
    {
      // filled by [Options] macros
    }

  static Parse (s : string, o : ref bool) : void
    match (s)
      | "1" | "t" | "true" | "True" => o = true
      | "0" | "f" | "false" | "False" => o = false
      | _ => throw FatalError ($"invalid format for boolean option: `$s'")

  static Parse (s : string, o : ref int) : void
    o = int.Parse (s)

  static Parse (s : string, o : ref double) : void
    o = double.Parse (s)

  static Parse (s : string, o : ref string) : void
    o = s

  static TypeName (_ : ref double) : string
    "double"

  static TypeName (_ : ref bool) : string
    "bool"

  static TypeName (_ : ref int) : string
    "int"

  static TypeName (_ : ref string) : string
    "string"

  [Record] \
  class TheOption
    public Name : string
    public Aliases : list [string]
    public Description : string
    public Setter : string -> void

  static options : Hashtable [string, TheOption] = Hashtable ()
  static mutable option_list : list [TheOption] = []
  static AddOption (opt : TheOption) : void
    foreach (name in opt.Name :: opt.Aliases)
      options [name.ToLower ().Replace ("_", "")]  = opt
    option_list ::= opt

  static DescribeOptions () : string
    def res = System.Text.StringBuilder ()
    foreach (opt in option_list.Rev ())
      _ = res.AppendFormat ("          {0,-25} {1}\n", opt.Name, opt.Description)
    res.ToString ()

  static SetOptions (s : string) : void
    foreach (o in s.Split (','))
      def spl = o.Split ('=')
      if (spl.Length != 2)
        throw FatalError ($"invalid option format: `$o'")
      else
        def name = spl [0].ToLower ().Replace ("_", "")
        if (options.Contains (name))
          options [name].Setter (spl [1])
        else
          throw FatalError ($"unknown option name: `$(spl[0])'")

  static this ()
    RegisterOptions ()
  #endregion

  
  mutable usersys_time = 0
  mutable peak_memory = 0

  ReadProcStats () : void
    when (System.IO.File.Exists ("/proc/self/stat") && 
        System.IO.File.Exists ("/proc/self/status"))
      def lines = System.IO.File.ReadAllLines ("/proc/self/stat")
      def words = lines [0].Substring (lines [0].LastIndexOf (") ") + 2).Split (' ')
      def user = int.Parse (words [11])
      def sys = int.Parse (words [12])
      mutable vmpk = 0
      foreach (l in System.IO.File.ReadAllLines ("/proc/self/status"))
        when (l.StartsWith ("VmPeak:"))
          vmpk = int.Parse (l.Substring (8).Replace ("kB", ""))
      usersys_time = (user + sys) * 10
      peak_memory = vmpk


  DumpStats () : void
    unless (NoStats)
      def running_time = System.Environment.TickCount - start_time
      def running_time = if (running_time == 0) 1 else running_time
      def time (t)
        string.Format ("{0:0.00}s", t / 1000.0)
      def csv_time (t)
        string.Format ("{0:0.00}", t / 1000.0)

      ReadProcStats ()
      def cpu_usage = usersys_time * 100 / running_time
      WriteLine ("*** STATS ***")
      WriteLine ($ "running time [$problem_name]: $(time(running_time)) / $(time(usersys_time)) $(cpu_usage)% CPU $(peak_memory) kB")
      def totals = GetStats ()
      foreach ((n, v) in totals)
        WriteLine ("{0,40} : {1}", n, v)
      WriteLine ($ "clause count: $clause_count")
      def line = CSV.Line (
        file_name, 
        problem_name, 
        csv_time (running_time),
        csv_time (usersys_time),
        cpu_usage,
        status,
        result,
        cmd_line_options);
      def line = line + $[v | (_, v) in totals]
      when (!System.IO.File.Exists (CsvName))
        CSV.WriteFile (CsvName, [["File name", "Problem", "Time", "user/sys time", "% CPU", 
                                   "Status", "Result", "Cmd line"] + 
                                   $[ n | (n, _) in totals ]], append = true)
      CSV.WriteFile (CsvName, [line], append = true)
      WriteLine (ReportSizes (num_case_splits, total_sizes))
      when (Profile)
        DumpProf ()
      when (DumpQuantStats)
        core.TermPool.DumpStats ()

  static public mutable LogPrefix : string = ""
  static public DoLog (msg : string) : void
    System.Console.WriteLine (LogPrefix + msg)

  ReportSizes (every : int, sz : array [long]) : string
    def nz (n : long)
      if (n == 0) -1L else n
    def every = nz (every)
    mutable s = ""
    for (mutable i = 0; i < sz.Length; ++i)
      s += string.Format ("{0,5} ", sz [i] / every)
                          
    s
  #endregion

  internal CheckTimeout () : void
    when (end_time != 0 && System.Environment.TickCount > end_time)
      result = "TIMEOUT"
      log (WARN, "TIMEOUT")
      throw TimeoutException ()

  public this (name = "")
    problem_name = name
    when (TimeLimit != 0)
      end_time = TimeLimit * 1000 + System.Environment.TickCount
    start_time = System.Environment.TickCount
    core = Core (this)

  internal ProgressCallback () : void
    CheckTimeout ()
    LoggingEnabled = num_case_splits >= LogAfter
    num_case_splits++
    when (!Verbose)
      StatLine ()

  internal StatLine () : void
    when (System.Environment.TickCount - last_stat_at_tick > 500)
      def every = num_case_splits - last_stat_at_iter
      last_stat_at_tick = System.Environment.TickCount
      last_stat_at_iter = num_case_splits
      when (!NoStats && !NoProgress)
        def s = string.Format ("\ri: {0,-4}+{1,-4}/{2,-4} t:{3,7:0.00}s ",
                               num_conflicts, num_case_splits, 
                               instance_count,
                               (System.Environment.TickCount - start_time) / 1000.0)
        Write (s + ReportSizes (every, sizes) + "  \r")
      for (mutable i = 0; i < sizes.Length; ++i)
        total_sizes [i] += sizes [i]
        sizes [i] = 0


  [Profile] \
  public Run (formula : Term) : bool
    def d = SimpleSolver (core, this)
    d.Search (formula)


  static mutable error_cnt = 0
  
  static ForParser (parser : Parser) : void
    when (SmtStartNo > 0)
      SmtStartNo = 1
    LoggingEnabled = 0 >= LogAfter
    foreach (ax in axiom_files.Rev ())
      parser.ReadAxioms (ax)
    def write (s : string)
      if (Mechanical)
        log (INFO, s)
      else
        Write (s)

    mutable cnt = 0
    def run (cmd, mkform, expect_sat, expect_unsat)
      ++cnt
      def d = Driver (cmd.name)
      Instance = d
      d.core.PlainPredicates = parser.PlainPredicates
      def formula = mkform (d.core)
      def end = if (NoStats) "" else "\n"
      if (formula == null)
        when (Driver.EnablePruner)
          d.DumpStats ()
        return
      else if (expect_sat)
        write ($ "ExpectSAT [$(cmd.name)]...\n")
        d.status = "SAT"
      else if (expect_unsat)
        write ($ "ExpectUnSAT [$(cmd.name)]...\n")
        d.status = "UNSAT"
      else
        write ($ "CheckSAT [$(cmd.name)]...\n")
        d.status = "unknown"
      try
        def sat = d.Run (formula)
        if ((expect_sat && !sat) || (expect_unsat && sat))
          error_cnt++
          if (Mechanical)
            log (ERR, "wrong answer")
          else
            write ("\n\x1b[31;1mwrong answer\x1b[0m\n\n")
          when (d.result == null)
            d.result = "wrong answer"
        else if (expect_sat || expect_unsat)
          if (Mechanical)
            log (INFO, "correct answer")
          else
            write (end + $ "\x1b[32;1mOK\x1b[0m, SAT=$sat (i=$(d.instance_count))\n")
          d.result = $"OK:SAT=$sat"
        else
          unless (Mechanical)
            write ($"\nok, SAT=$sat\n")
          d.result = $"OK:SAT=$sat"
        d.DumpStats ()
      catch
        | _ is TimeoutException =>
          d.DumpStats ()
          System.Environment.Exit (3)
        
    foreach (c in parser.Run ())
      | CheckSAT (f) => run (c, f, false, false)
      | ExpectSAT (f) => run (c, f, true, false)
      | ExpectUnSAT (f) => run (c, f, false, true)

  public static mutable alloc_block : string

  public static Main () : int
    mutable help_opts = []
    def print_help ()
      WriteLine (Getopt.Usage (help_opts))
      WriteLine ("Exit codes:\n"
                 "0 - OK\n"
                 "1 - wrong answer\n"
                 "2 - FatalError exception\n"
                 "3 - timeout\n"
                 "4 - other exception\n"
                 "5 - non-UTVPI/non-linear\n"
                 )
      System.Environment.Exit (0)

    mutable files = []

    cmd_line_options = System.Environment.CommandLine
        
    def opts =
      [
        Getopt.CliOption.Flag (name = "-verbose",
                                 aliases = ["-v"],
                                 help = "Be noisy",
                                 handler = fun () { Verbose = true }),
        Getopt.CliOption.Flag (name = "-verbose-quant",
                                 aliases = ["-vq"],
                                 help = "Be noisy about quantifiers",
                                 handler = fun () { VerboseQuant = true }),
        Getopt.CliOption.Flag (name = "-smt",
                                 aliases = [],
                                 help = "Translate input to SMT-LIB format",
                                 handler = fun () { Translate = true }),
        Getopt.CliOption.Int (name = "-smt-no",
                                 aliases = [],
                                 help = "Start numerating SMT-LIB dumps with INT",
                                 handler = fun (n) { Translate = true; SmtStartNo = n }),
        Getopt.CliOption.Flag (name = "-print-result",
                                 aliases = ["-p"],
                                 help = "Print the final assignment",
                                 handler = fun () { PrintResult = true }),
        Getopt.CliOption.Int (name = "-time-limit",
                                 aliases = ["-t"],
                                 help = "Time limit in seconds",
                                 handler = fun (i) { TimeLimit = i }),
        Getopt.CliOption.Int (name = "-log-after",
                                 aliases = [],
                                 help = "Enable logging only during and after iteration INT",
                                 handler = fun (i) { LogAfter = i }),
        Getopt.CliOption.Flag (name = "-no-stats",
                                 aliases = ["-n"],
                                 help = "Disable stats",
                                 handler = fun () { NoStats = true }),
        Getopt.CliOption.Flag (name = "-no-progress",
                                 aliases = ["-npb"],
                                 help = "Disable progress display",
                                 handler = fun () { NoProgress = true }),
        Getopt.CliOption.Flag (name = "-simplify-syntax",
                                 aliases = ["-s"],
                                 help = "Use Simplify's syntax.",
                                 handler = fun () { SimplifySyntax = true }),
        Getopt.CliOption.String (name = "-axioms",
                                 aliases = ["-ax"],
                                 help = "Read axioms from specified file.",
                                 handler = fun (s) { axiom_files ::= s }),
        Getopt.CliOption.Flag (name = "-expect-all-valid",
                                 aliases = ["-valid"],
                                 help = "Expect all formulas to be valid.",
                                 handler = fun () { ExpectAllValid = true }),
        Getopt.CliOption.Flag (name = "-expect-all-invalid",
                                 aliases = ["-invalid"],
                                 help = "Expect all formulas to be invalid.",
                                 handler = fun () { ExpectAllInvalid = true }),
        Getopt.CliOption.Flag (name = "-mechanical",
                                 aliases = ["-M"],
                                 help = "Use machine-readable output, supress stats.",
                                 handler = fun () { NoStats = true; NoProgress = true; 
                                        Mechanical = true }),

        Getopt.CliOption.String (name = "-options",
                                 aliases = ["-o", "-opt"],
                                 help = "Set search options, possible options are:\n" + DescribeOptions (),
                                 handler = SetOptions),

        Getopt.CliOption.Flag (name = "-no-profile",
                                 aliases = ["-np"],
                                 help = "Don't display profile data",
                                 handler = fun () { Profile = false }),
        Getopt.CliOption.Int (name = "-doublecheck",
                                 aliases = ["-dc"],
                                 help = "Check theory conflict clauses again (INT times)",
                                 handler = fun (x) { DoubleCheck = x }),
        Getopt.CliOption.Flag (name = "-pretty-print",
                                 aliases = ["-pp"],
                                 help = "Display the first formula pretty printed, using Unicode",
                                 handler = fun () { PrettyPrint = true }),

        Getopt.CliOption.Int (name = "-alloc",
                                 aliases = [],
                                 help = "Voodoo",
                                 handler = fun (x) { alloc_block = string ('x', x) }),

        Getopt.CliOption.String (name = "-csv-name",
                                 aliases = [],
                                 help = "Set the name of the CSV stats file",
                                 handler = fun (x) { CsvName = x }),

        Getopt.CliOption.String (name = "-pruner",
                                 aliases = ["-pr"],
                                 help = "Set the name of the previously unsat file for the pruner",
                                 handler = fun (x) { EnablePruner = true; PrunerFile = x }),

        Getopt.CliOption.String (name = "-strategies",
                                 aliases = ["-st"],
                                 help = "List of strategy numbers to try, like 1,2",
                                 handler = fun (x) { 
                                   Strategies = 
                                        $[int.Parse (k) | k in x.Split (',', ';', ' ', ':')]
                                 }),

        Getopt.CliOption.Flag (name = "-help",
                     aliases = ["-h"],
                     help = "Display this usage message and exit",
                     handler = print_help),
        Getopt.CliOption.NonOption (name = "",
                          help = "Specify file to check (omit to use stdin)",
                          handler = fun (s) { files ::= s })
      ]

    try
      help_opts = opts
      Getopt.Parse (opts)
      
      match (files)
        | [] => ForParser (Parser ())
        | xs =>
          foreach (x in xs.Rev ())
            file_name = x
            ForParser (Parser (x))

      if (error_cnt == 0)
        log (INFO, "All tests passed.")
        0
      else
        log (INFO, $ "$error_cnt tests failed.")
        1
        
    catch
      | e is FatalError =>
        def msg = e.Message
        log (ERR, $ "Fatal error: $msg")
        
        if (msg.IndexOf ("not UTVPI") != -1 || msg.IndexOf ("non-linear subterm") != -1)
          5
        else
          2
      | e =>
        log (ERR, $ "Internal Prover Error:\n$e")
        4