using Nemerle.Collections
using Nemerle.Imperative
using Nemerle.Logging
using Nemerle.Profiling
using SCG = System.Collections.Generic

set namespace Fx7

public class QuantLoop
  // mutable set
  type MSet [T] = Hashtable [T, T]

  start_monome : list [Literal]
  skolemized : MSet [Term] = Hashtable ()
  core : Core
  tocnf : ToCNF
  pool : Term.Pool
  loop_id : int

  static mutable id_seq = 1

  mutable iters = 0
  mutable important : Hashtable [Literal, bool]
  mutable remaining_important : list [Literal] = []
  mutable important_iter = 0
  mutable instances = 0

  [Profile] \
  public CopyFrom (other : QuantLoop) : void
    foreach (t in other.skolemized.Keys)
      skolemized [t] = t
  
  public this (c : Core, monome : list [Literal], parent : ToCNF)
    loop_id = id_seq
    id_seq++
    start_monome = monome
    core = c
    pool = core.TermPool
    tocnf = ExternalCNF (c, parent)

  public this (dpll : DPLLSolver, monome : list [Literal])
    loop_id = id_seq
    id_seq++
    start_monome = monome
    core = dpll.Core
    pool = core.TermPool
    tocnf = dpll.CnfConverter

  public NumFullIters : int
    get { iters } 

  // return true if succeeded
  [Profile] \
  TrySkolemize (lit : Literal, res : Vec [ToCNF.Fact]) : void
    when (!lit.bg_asserted && 
        lit.is_neg && 
        lit.atom.IsQuantified && 
        !skolemized.Contains (lit.atom.term1))
      def atom = lit.atom :> QAtom
      def sub = atom.Vars.FoldLeft (IntTree.Empty (), fun (t, acc) {
        acc.Add (t.Id, core.TermPool.FreshVar ())
      })
      skolemized [lit.atom.term1] = lit.atom.term1
      atom.GenFact (_.Apply (sub), res, true)
      //log (QUANT, $ "add skol $lit => $t")

  IsImportantNow (lit : Literal) : bool
    if (important == null) true
    else important.Contains (lit)

  Exists (lits : list [Literal], f : Literal * Vec [ToCNF.Fact] -> void) : bool
    def res = Vec (100)
    lits.Iter (f (_, res))
    if (res.Count == 0) false
    else
      core.PushState ()
      foreach (f in res)
        //log (TEMP, $ "add: #$(core.TheDriver.num_inst_rounds).$iters $f")
        log (QUANT, $ "add: $f")
        tocnf.AddInstance (f, add_explanation = true)
      core.PopState ()
      true

  RestartImportant () : void
    def keys = $[k | k in core.ImportantLiterals.Keys]
    remaining_important = keys.Sort (fun (a, b) { 
      match (core.ImportantLiterals [b].CompareTo (core.ImportantLiterals [a])) {
        | 0 => a.GetHashCode ().CompareTo (b.GetHashCode ())
        | x => x
      }
    })
    important_iter = 0
    important = Hashtable ()

  GenerateInstances (lits : list [Literal]) : bool
    if (important_iter >= Driver.ImportantOnlyIters || remaining_important is [])
      important = null
    else
      repeat (Driver.ImportantOnlyStep)
        match (remaining_important)
          | x :: xs =>
            important [x] = true
            remaining_important = xs
          | [] => {}
      important_iter++
    
    when (important == null)
      iters++

    Term.Matcher.Start (pool, important != null)

    def instances = Vec (100)

    def matchers =
      lits.FoldLeft ([], (lit, acc) =>
        if (!lit.is_neg && lit.atom.IsQuantified && IsImportantNow (lit)) {
          def atom = lit.atom :> QAtom;
          atom.term1.Stats.InLoop (loop_id);
          Term.Matcher (atom, instances) :: acc
        } else acc)

    foreach (m in matchers) m.Prepare ()
    foreach (m in matchers) m.Run ()

    Term.Matcher.Stop (pool)

    if (instances.Count == 0)
      if (important != null)
        GenerateInstances (lits)
      else false
    else
      def cnt = instances.Count
      this.instances += cnt
      core.TheDriver.instance_count += cnt
      core.PushState ()
      when (this.instances > core.TheDriver.max_instances_per_round)
        core.TheDriver.max_instances_per_round = this.instances
      foreach (f in instances)
        //log (TEMP, $ "add: #$(core.TheDriver.num_inst_rounds).$iters $f")
        log (QUANT, $ "add: $f")
        tocnf.AddInstance (f, add_explanation = true)
      core.PopState ()
      when (important == null && !Driver.ImportantOnce)
        RestartImportant ()
      true


  public Restart () : void
    {}


  public GenerateFacts () : bool
    def lits = tocnf.GetQMonome ()

    if (core.TheDriver.CheckMir (iters))
      false
    else if (Exists (lits, TrySkolemize))
      true
    else
      GenerateInstances (lits)


  public Prepare (skip_important = false) : void
    core.TheDriver.num_quant_loops++
    unless (skip_important)
      RestartImportant ()
    //log (TEMP, $[core.ImportantLiterals[x]|x in remaining_important].ToString())
    //log (TEMP, $[x.GetHashCode()|x in remaining_important].ToString())
    core.TheDriver.StartQuantLoop ()
    tocnf.AssertMonome (start_monome)

  public MarkBgAsserted () : void
    _ = Exists (start_monome, TrySkolemize)
    foreach (l in start_monome)
      l.bg_asserted = true

  public ClearBgAsserted () : void
    //log (TEMP, $"only=$importance_limit size=$(core.ImportantLiterals.Count) max=$(core.ImportantLiteralsMax) iters=$iters inst=$instances")
    foreach (l in start_monome)
      l.bg_asserted = false

  // return a conflict clause or null if not available
  [Profile] \
  public Run () : bool
    def tocnf = tocnf :> ExternalCNF

    def loop ()
      log (QUANT, "*** loop ***")
      if (core.TheDriver.QuantCallback ())
        false
      else if (! tocnf.Solve ())
        log (QUANT, "Look for unsat core")
        tocnf.FindUnsatCore ()
        true
      else
        def lits = tocnf.GetMonome (skip_asserted = true)
        log (QUANT, $"quant lits: " + lits.ToString ("\n"))
        match (core.GetConflicts (lits, leave_open = true))
          | [] =>
            core.TheDriver.total_quant_monome_size += lits.Length
            if (GenerateFacts ())
              core.PopState ()
              loop ()
            else
              false // SAT!

          | lst =>
            log (QUANT, $ "add conflicts: $lst")
            tocnf.AddConflicts (lst)
            loop ()
    
    Prepare ()

    assert (!core.Refuted)

    MarkBgAsserted ()
    try
      loop ()
    finally
      core.PopState ()
      ClearBgAsserted ()