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

set namespace Fx7

#define MULTI_REF
//#define DETERMINISTIC

public type Vec ['a] = System.Collections.Generic.List ['a]
public delegate Callback () : void

public class Core
  public TermPool : Term.Pool = Term.Pool (this)
  public TheDriver : Driver

  public mutable Refuted : bool
  public mutable PossibleSplitLiterals : list [Term]
  public mutable RefutationProof : list [Literal]
  public mutable RefutationProofs : list [list [Literal]]
  public mutable MultiRefutation : bool
  public mutable SeenExplicitTriggers : bool // = true
  public mutable CurrentCnfConverter : ToCNF
  public mutable LastUnsatCore : list [Literal]
  public mutable SubtypingSymbol : string = "<:"
  public mutable SubtypingTrue : Term

  internal mutable PlainPredicates : Hashtable [string, string] = Hashtable ()

  internal ImportantLiterals : Hashtable [Literal, float] = Hashtable ()
  internal mutable CurrentStrategy : int = 2
  
  pending : Queue [void -> void] = Queue ()

  internal mutable linear_theory : LinearTheory

  public event OnPush : Callback
  public event OnPop : Callback

  public this (d : Driver)
    TheDriver = d
    def arith ()
      if (Driver.EnableLinearTheory)
        linear_theory = LinearTheory (0, this)
        linear_theory
      else
        UtvpiTheory (0, this)
    mutable thr = [arith () : PlainVarTheory]

    mutable id = 1
    when (Driver.EnableTcTheory)
      thr ::= TcTheory (id, this)
      id++
    when (Driver.EnableArrayTheory)
      thr ::= ArrayTheory (id, this)
      id++
    thr = thr.Rev ()
    var_theories = thr.ToArray ()

    theories = thr.Map (fun (x) { x : Theory }) + [free_fun_th]

  #region Theory dispatch
  free_fun_th : FreeFunTheory = FreeFunTheory (this)
  theories : list [Theory]
  internal var_theories : array [PlainVarTheory]

  public IsSomeTheoryPredicate (name : string) : bool
    when (name == "distinct")
      return (true)
    foreach (t in var_theories)
      when (t.IsMyPredicate (name))
        return (true)
    false

  [Profile] \
  AddVar (thr : int, t : Term) : void
    when (thr == -1)
      return

    log (COREV, $"AddVar($t) root=$(t.Root)")

    def old_t = t.Var [thr]
    assert (old_t : object != t)

    def th = var_theories [thr]
    th.MakeAlien (t, outer = th.IsMyFunction (t.Name))
    t.SetVar (thr, t)
   
    if (old_t != null)
      th.TellEquality (t, old_t, Proof.EqProof (t, old_t))
    else if (t : object != t.Root)
      if (t.Root.Var [thr] != null)
        // whoops, we already had a variable here
        def root_t = t.Root.Var [thr]
        log (COREV, $"AddVar: assert eq $t = $root_t to $th")
        th.TellEquality (t, root_t, Proof.EqProof (t, root_t))
      else
        log (COREV, $"AddVar: copy var $(t.Root) <- $t")
        t.Root.SetVar (thr, t)
    else {}

  // -1 is UIF
  TheoryOf (t : Term) : int
    foreach (i in [0 .. var_theories.Length - 1])
      def th = var_theories [i]
      when (th.IsMyFunction (t.Name))
        return (i)
    -1
    

  // thr:
  // -2 -- don't create top-alien
  // -1 -- do create it
  [Profile] \
  Alienate (thr : int, t : Term) : void
    DoAlienate (thr, t)
  
  DoAlienate (thr : int, t : Term) : void
    log (COREV, $"Alienate($thr, $t) done=$(t.Alienated)")
    def thr' = TheoryOf (t)
    unless (t.Alienated)
      t.WillWrite ()
      t.Alienated = true
      foreach (c in t.Children)
        DoAlienate (thr', c)
    when (thr != thr' && thr != -2)
      when (thr != -1 && t.Var [thr] : object != t)
        AddVar (thr, t)
      when (thr' != -1 && t.Var [thr'] : object != t)
        AddVar (thr', t)
    

  AssertPredicate (neg : bool, t : Term, proof : Proof) : void
    if (t.Name == "distinct")
      if (neg)
        // we probably should check each possibility here, but we won't
        {}
      else
        t.IterChildren (Alienate (-1, _))
        TermPool.AssertDistinct (t.Children, proof)
    else
      foreach (i in [0 .. var_theories.Length - 1])
        def th = var_theories [i]
        when (th.IsMyPredicate (t.Name))
          log (COREV, $ "tell struct-pred $t")
          t.IterChildren (Alienate (i, _))
          th.AssertPredicate (neg, t.Name, t.Children, proof)
 
  // used by TermPool.Merge
  internal TellEquality (t1 : Term, t2 : Term) : void
    log (CORE, $"TellEquality($t1, $t2)")
    
    foreach (i in [0 .. var_theories.Length - 1])
      def r1 = t1.Var [i]
      def r2 = t2.Var [i]
      if (r1 == null)
        if (r2 != null)
          t1.SetVar (i, r2)
        else {}
      else
        if (r2 != null)
          log (CORE, $"will telleq: $t1 $t2")
          pending.Push (fun () {
            log (CORE, $"run telleq: $t1 $t2");
            Alienate (-2, r1);
            Alienate (-2, r2);
            var_theories [i].TellEquality (r1, r2, Proof.EqProof (r1, r2))
          })
        else
          t2.SetVar (i, r1)
      
  TellInequality (t1 : Term, t2 : Term, proof : Proof) : void
    log (COREV, $ "tell struct-ineq $t1 $t2")
    Alienate (-1, t1)
    Alienate (-1, t2)
    free_fun_th.TellInequality (t1, t2, proof)


  TellEquality (t1 : Term, t2 : Term, proof : Proof) : void
    log (COREV, $ "tell struct-eq $t1 $t2")
    // using -2 here is problematic
    Alienate (-1, t1)
    Alienate (-1, t2)
    TermPool.Merge (t1, t2, proof)
  #endregion


  #region push and pop
  mutable state_level = 0
  [Profile] \
  public PushState () : void
    assert (!Refuted)
    log (CORE, "( push")
    state_level++
    OnPush ()
    foreach (th in var_theories)
      th.PushState ()
    free_fun_th.PushState ()

  [Profile] \
  public PopState () : void
    log (CORE, "pop )")
    state_level--
    free_fun_th.PopState ()
    foreach (th in var_theories)
      th.PopState ()
    OnPop ()
    Reset ()
 
  internal Reset () : void
    log (CORE, "reset")
    pending.Clear ()
    Refuted = false
    RefutationProof = null
    RefutationProofs = []
    MultiRefutation = false
    PossibleSplitLiterals = []
  #endregion

  #region Utils
  // we don't want true randomness here
  // http://crypto.mat.sbg.ac.at/results/karl/server/node4.html
  mutable rand_seed : uint = 1
  public Rand () : uint
    unchecked
      rand_seed *= 3039177861
    rand_seed

  public Rand (max : int) : int
    unchecked
      (Rand () % (max :> uint)) :> int

  public Refute (proof : Proof) : void
    log (CORE, $"Refute, lits=$(proof.GetLiterals())")
    if (MultiRefutation)
      RefutationProofs ::= proof.GetLiterals ()
      when (RefutationProofs.Length > Driver.MaxMultiRefutations)
        Refuted = true
    else
      unless (Refuted)
        Refuted = true
        RefutationProof = proof.GetLiterals ()

  public AddSplitLiteral (l : Term) : void
    log (CORE, $"add case split on $l")
    PossibleSplitLiterals ::= l

  [Profile] \
  public RandomizeList ['a] (l : list ['a]) : list ['a]
    def a = l.ToArray ()
    def len = a.Length
    repeat (len)
      a [Rand (len)] <-> a [Rand (len)]
    List.FromArray (a)
  #endregion

  [Profile] \
  Assert (lit : Literal) : void
    TheDriver.num_asserts++
    log (CORE, $"assert $lit")
    unless (Refuted)
      AssertOnly (lit, Proof.Leaf (lit))
      while (!Refuted && !pending.IsEmpty)
        pending.Take () ()
  
  [Profile] \
  AssertOnly (lit : Literal, proof : Proof) : void
    unless (Refuted)
      def (t1, t2) = lit.atom
      if (lit.atom.IsQuantified) {}
      else if (t2 == null)
        AssertPredicate (lit.IsNeg, t1, proof)
      else
        if (lit.IsNeg)
          TellInequality (t1, t2, proof)
        else
          TellEquality (t1, t2, proof)

  FinalTheoryCheck () : void
    PossibleSplitLiterals = []
    theories.Iter (_.FinalCheck ())

  public ClearTheories () : void
    theories.Iter (_.Clear ())

  public SetActive (lits : list [Literal]) : void
    foreach (l in lits)
      unless (l.atom.IsQuantified)
        l.atom.term1.MakeActive ()
        when (l.atom.term2 != null)
          l.atom.term2.MakeActive ()

  public FullFinalCheck () : void
    while (true)
      while (!pending.IsEmpty)
        pending.Take () ()
        when (Refuted) break
      FinalTheoryCheck ()
      when (Refuted || pending.IsEmpty) break


  internal AssertLits (lits : list [Literal], do_final_check = true) : void
    log (CORE, $ "AssertLits start, final=$do_final_check")
    SetActive (lits)
    foreach (lit in lits)
      if (lit.atom.IsQuantified || lit.bg_asserted)
        log (CORE, $"skip $lit ($(lit.bg_asserted))")
      else
        Assert (lit)
        when (Refuted) break

    when (do_final_check)
      FullFinalCheck ()

    log (CORE, "AssertLits stop")


  [Profile] \
  OneStepMinimize (lits : list [Literal]) : list [Literal]
    Reset ()
    PushState ()
    try
      def lits = RandomizeList (lits)

      AssertLits (lits)

      log (CORE, $ "minimize: $lits, ref=$Refuted proof=$RefutationProof")
      if (!Refuted) null
      else
        def res = RefutationProof
        log (CORE, $ "minimize: res=$res")
        res
    finally
      PopState ()

  // all_lits only for debug dump
  DoMinimizeConflictClause (all_lits : list [Literal], lits : list [Literal]) : list [Literal]
    def fixpoint (prev, lits, tries = 0)
      // def lits' = OneStepMinimize (OneStepMinimize (lits))
      def lits' = OneStepMinimize (lits)
      assert (lits' != null, $ "failed minimization for, iter=$(this.TheDriver.num_main_iters): $prev -> $lits")
      // the case when lits' > lits occurs, when we have some background
      // assertions
      // I guess this isn't exactly right...
      if (lits'.Length >= lits.Length) 
        if (tries > 0)
          fixpoint (prev, lits, tries - 1)
        else
          lits
      else
        fixpoint (lits, lits', tries)

    def lits = fixpoint (all_lits, lits)
    TheDriver.sizes [2] += lits.Length
    TheDriver.sizes [3]++
    
    when (Driver.Verbose) WriteLine ($ "minimized: $(lits)")

    assert (OneStepMinimize (lits) != null,
            $ "failed post minimization test for $(lits)")

    lits

  mutable all_conflicts : list [list [Literal]] = []
  
  [Profile] \
  MinimizedConflictClause (lits : list [Literal], all_lits : list [Literal]) : list [Literal]
    log (CORE, $"add mincc by $lits")
    TheDriver.sizes [1] += lits.Length

    def lits =
      if (!Driver.MinimizeConflictClause)
        lits
      else
        DoMinimizeConflictClause (all_lits, lits)
      
    when (Driver.Verbose) WriteLine ($ "theory conflict clause, $(lits.Length): $lits")

    when (Driver.DoubleCheck > 0)
      assert (! lits.IsEmpty)
      all_conflicts ::= lits

    //log (TEMP, $ "conflict: $lits")

    $[~l | l in lits]

  [Profile] \
  public GetConflictsMain (lits : list [Literal]) : list [list [Literal]]
    GetConflicts (lits)

  public DoubleCheck () : void
    Write ("\ndouble checking theory conflicts... ")
    while (state_level > 0)
      PopState ()
    mutable sum = 0.0
    foreach (conflict in all_conflicts)
      mutable min = int.MaxValue

      mutable maxp = null
      mutable maxpl = 0

      //Write ($"\n$(conflict.Length): ")
      foreach (_ in [0 .. Driver.DoubleCheck])
        Reset ()
        PushState ()
        //log (TEMP, $"cnfl=$conflict")
        def c = RandomizeList (conflict)
        AssertLits (c)
        when (!Refuted)
          throw System.Exception ($"bad theory conflict: $c")
        def proof = RefutationProof
        def len = proof.Length
        when (len > maxpl)
          maxpl = len
          maxp = c
        when (len < min) min = len
        PopState ()
      sum += min / conflict.Length
      //when (maxpl != min)
      //  WriteLine ($ "$maxpl -> $min, $(conflict.Length): $maxp")
    WriteLine ($"done, avg overhead $(1.0 - sum / all_conflicts.Length)")

  // returns conflicts found in [lits] as minimized conflict clauses
  [Profile] \
  public GetConflicts (lits : list [Literal], leave_open = false) : list [list [Literal]]
    TheDriver.sizes [0] += lits.Length

    Reset ()

    when (Driver.MultiRefutation)
      MultiRefutation = true

    PushState ()

    #if DETERMINISTIC
    AssertLits (lits)
    #else
    AssertLits (RandomizeList (lits))
    #endif

    if (Driver.MultiRefutation && !(RefutationProofs is []))
      PopState ()
      $[MinimizedConflictClause (p, lits) | p in RefutationProofs]
    else if (!Driver.MultiRefutation && Refuted)
      PopState ()
      [MinimizedConflictClause (RefutationProof, lits)]
    else 
      unless (leave_open)
        PopState ()
      []

  [Profile] \
  public GetConflictsDPLL (lits : list [Literal], final_check : bool) : list [list [Literal]]
    if (lits is [] && !final_check)
      []
    else
      TheDriver.sizes [0] += lits.Length

      Reset ()

      when (Driver.MultiRefutation)
        MultiRefutation = true

      #if DETERMINISTIC
      AssertLits (lits, final_check)
      #else
      AssertLits (RandomizeList (lits), final_check)
      #endif

      if (Driver.MultiRefutation && !(RefutationProofs is []))
        $[MinimizedConflictClause (p, lits) | p in RefutationProofs]
      else if (!Driver.MultiRefutation && Refuted)
        [MinimizedConflictClause (RefutationProof, lits)]
      else 
        []