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

using MiniSatCS

set namespace Fx7

public class QuantDPLLSolver : DPLLSolver
  qloop : QuantLoop
  top_trail : list [Literal]

  mutable start_num_quant_iters : int
  mutable start_instance_count : int
  mutable start_num_inst_rounds : int

  public this (parent : DPLLSolver)
    base (parent.core, parent.driver, parent.cnf_converter, parent.Level + 1)

    conflicts_log = parent.conflicts_log

    start_num_quant_iters = core.TheDriver.num_quant_iters
    start_instance_count = core.TheDriver.instance_count
    start_num_inst_rounds = core.TheDriver.num_inst_rounds

    top_trail = parent.Trail ()
    qloop = QuantLoop (this, top_trail)
    match (parent)
      | p is QuantDPLLSolver =>
        qloop.CopyFrom (p.qloop)
      | _ => {}
    //qloop.Prepare (skip_important = Level > 1)
    qloop.Prepare ()
    foreach (l in top_trail)
      parent_asserted_literals [l] = l

  QCleanState () : void
    ClearState ()

  [Profile] \
  SpawnNextLevel () : bool
    log (QDPLL, $ "starting new, at lev=$Level ")
    def next = QuantDPLLSolver (this) 
    !next.Run ()

  [Profile] \
  public Run () : bool
    inside_search = true
    
    //log (TEMP, $"start small sat")
    if (SearchNoRestarts ())
      QCleanState ()
      true
    else
      QCleanState ()

      cnf_converter.FindUnsatCore (conflicts_log)

      def time = System.Environment.TickCount - start_time
      when (time > Driver.HardMonomeLimit * 1000) // put a proper limit here
        log (TEMP, $"time: $time ms, "
                    "$(core.TheDriver.num_quant_iters - start_num_quant_iters) iters, "
                    "$(core.TheDriver.instance_count - start_instance_count) instances, "
                    "$(core.TheDriver.num_inst_rounds - start_num_inst_rounds) inst.rounds, "
                    "confl: $(core.LastUnsatCore.Map (~_)) trail: top_trail")

      //log (TEMP, $"end small sat")
      log (QDPLL, $ "generated small sat conflict")
      false

  mutable forced_instantiation_countdown : int = Driver.InstantatiateEvery

  [Profile] \
  protected override ModelFoundCallback () : bool
    if (driver.QuantCallback ())
      when (Driver.Verbose)
        System.Console.WriteLine ($"failing top-trail: $(top_trail)")
      false
    else
      def force_inst = 
        forced_instantiation_countdown--
        forced_instantiation_countdown == 0

      if (!force_inst && base.ModelFoundCallback ()) true
      else if (qloop.NumFullIters > 0 && Level + 1 < Driver.SatLevels)
        SpawnNextLevel ()
      else
        foreach (i in $[0 .. trail.size() - 1])
          def l = cnf_converter.ToLiteral (index(trail[i]))
          when (l != null && !l.bg_asserted && !parent_asserted_literals.Contains (l) && 
                !l.atom.IsQuantified)
            core.TheDriver.total_quant_monome_size++

        instance_bump *= Driver.InstanceBumpMult
        //log (TEMP, $"$forced_instantiation_countdown")
        forced_instantiation_countdown = Driver.InstantatiateEvery

        //log (TEMP, "start case split")
        foreach (term in core.PossibleSplitLiterals)
          def lit = cnf_converter.MakeLiteral (term)
          //log (TEMP, $"will case split on: $lit")
          QueueCaseSplit (lit)
        //log (TEMP, "stop case split")

        if (qloop.GenerateFacts () || !(core.PossibleSplitLiterals is []))
          // ok, found some instantiations
          log (QDPLL, $ "generated something")
          true
        else if (force_inst)
          true // we still might have case splits available
        else
          when (Driver.Verbose)
            System.Console.WriteLine ($"failing trail: $(Trail())")
          false