using Nemerle.Collections
using Nemerle.Logging
using Nemerle.Profiling
using Nemerle.Imperative

/*
The decision problem is NP-hard. Sketch:

A[0]=0
A[1]=1
0!=1

for each prep. var p:
(A[p] := 1)[0] = (A[p'] <- 0)[1]

p=0 -> L=1 -> R=1 -> p'!=0 -> SAT
p!=0 -> L=0 -> R=0 -> p'=0 -> SAT

for each 3-CNF clause [p,-r,q], add:
f(p',r,q') != f(0,0,0)

*/

set namespace Fx7

[CreateMemento] \
public class ArrayTheory : PlainVarTheory
  #region Rollback handling
  internal mutable current_level : int = 0

  public override PushState () : void
    current_level++
    SaveMemento ()
    
  public override PopState () : void
    current_level--
    RestoreMemento ()
  #endregion

  [Copy] mutable handled : IntTree [Term] = IntTree.Empty ()
  mutable possible_case_splits : list [Term * Term]
    
  internal this (i : int, c : Core)
    base (c, i)

  public override IsMyFunction (head : string) : bool
    | "select" | "store" => true
    | _ => false

  public override IsMyPredicate (_head : string) : bool
    false

  TryResolveSelect (select_term : Term) : bool
    log (ARR, $"TryResolveSelect: $select_term")
    def read_idx = select_term.Child_2of2
    mutable did_something = false

    def store_child = select_term.Child_1of2
    mutable stores = []
    store_child.IterEqc (t => when (t.Name == "store") stores ::= t)

    foreach (s in stores)
      match (s.Children)
        | [the_array, write_idx, write_val] =>

          def eq ()
            log (ARR, $"write=$write_val/$(write_val.Root) old=$select_term/$(select_term.Root)")
            when (select_term.Root : object != write_val.Root)
              core.TermPool.Merge (select_term, write_val, 
                                        Proof.Rule2 ("arr-1", Proof.EqProof (s, store_child), 
                                                              Proof.EqProof (write_idx, read_idx)))
              did_something = true

          def neq (proof)
            def new_select = core.TermPool.Get ("select", [the_array, read_idx])
            log (ARR, $"new=$new_select/$(new_select.Root) old=$select_term/$(select_term.Root)")
            when (select_term.Root : object != new_select.Root)
              new_select.MakeActive ()
              core.TermPool.Merge (select_term, new_select,
                                   Proof.Rule2 ("arr-2", proof, Proof.EqProof (s, store_child)))
              _ = TryResolveSelect (new_select)
              did_something = true

          if (write_idx.Root : object == read_idx.Root)
            eq ()
          else 
            def proof = write_idx.CannotMergeProof (read_idx)
            if (proof != null) neq (proof)
            else
              possible_case_splits ::= (read_idx, write_idx)

        | _ => assert (false)

    did_something

  public override MakeAlien (t : Term, outer : bool) : void
    when (outer)
      match (t.Name)
        | "select" =>
          unless (handled.Contains (t.Id))
            handled = handled.Add (t.Id, t)
            _ = TryResolveSelect (t)
            t.IterChildren (t => when (IsMyFunction (t.Name)) MakeAlien (t, true))
        | _ => {}  

  public override FinalCheckImpl (_full : bool) : void
    assert (!core.MultiRefutation)
    mutable go = true
    while (!core.Refuted && go)
      possible_case_splits = []
      go = handled.Fold (false, (_, t, did) => TryResolveSelect (t) || did)
        
    unless (core.Refuted)
      def seen = Hashtable ()
      foreach ((t1, t2) in possible_case_splits)
        def (t1, t2) =
          if (t1.Id < t2.Id) (t1, t2)
          else (t2, t1)
        def t = core.TermPool.Get ("=", [t1, t2])
        unless (seen.Contains (t))
          seen [t] = t
          core.AddSplitLiteral (t)

  public override AssertPredicate (_neg : bool, _head : string, _children : list [Term], _proof : Proof) : void
    assert (false)

  public override TellEquality (_u1 : Term, _u2 : Term, _proof : Proof) : void
    {}