using System
using System.Runtime.InteropServices

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

set namespace Fx7

public class SatSolver : IDisposable
  #region datatypes
  [Record] \
  public struct Var
    public id : int
    
    public ToLit () : Lit
      Lit (id + id)
      
    public ToPosLit () : Lit
      Lit (id + id)
      
    public ToNegLit () : Lit
      Lit (id + id + 1)

    public override ToString () : string
      $ "x$id"

    public Id : int
      get { id }

  [Record] \
  [StructLayout (LayoutKind.Sequential, Pack = 4)] \
  public struct Lit
    public val : int
    
    public Neg () : Lit
      Lit (val ^ 1)

    public static @~ (n : Lit) : Lit
      n.Neg ()

    public Var : Var
      get { Var (val >> 1) }
    
    public IsNeg : bool
      get { (val & 1) != 0 }

    public IsPos : bool
      get { (val & 1) == 0 }

    public Abs : Lit
      get
        if (IsNeg) ~this
        else this

    public override ToString () : string
      if (IsNeg)
        $ "-$(this.Var)"
      else
        this.Var.ToString ()

    public Id : int
      get { val }

    public override GetHashCode () : int
      val
    
    [Nemerle.OverrideObjectEquals] \
    public Equlas (other : Lit) : bool
      val == other.val
  #endregion


  #region external interface
  mutable handle : IntPtr

  [DllImport ("minisat.dll")] \
  extern static minisat_new () : IntPtr
  [DllImport ("minisat.dll")] \
  extern static minisat_delete (s : IntPtr) : void
  [DllImport ("minisat.dll")] \
  extern static minisat_solve (s : IntPtr) : int
  [DllImport ("minisat.dll")] \
  extern static minisat_get_model (s : IntPtr, output : array [int]) : int
  [DllImport ("minisat.dll")] \
  extern static minisat_add_clause (s : IntPtr, clause : array [Lit], sz : int) : void

  [DllImport ("minisat.dll")] \
  extern static minisat_solve_with (s : IntPtr, assump : array [Lit], size : int) : int
  [DllImport ("minisat.dll")] \
  extern static minisat_try_solve_with (s : IntPtr, assump : array [Lit], size : int,
                                        model : array [uint], modelsize : int) : int
  [DllImport ("minisat.dll")] \
  extern static minisat_get_conflict (s : IntPtr, confl : array [int]) : void
  
  [DllImport ("minisat.dll")] \
  extern public static minisat_rdtsc () : long
  [DllImport ("minisat.dll")] \
  extern public static minisat_get_usersys_time () : int
  #endregion

  core : Core
  
  public this (c : Core)
    handle = minisat_new ()
    core = c

  public Dispose () : void
    when (handle != IntPtr.Zero)
      minisat_delete (handle)
      handle = IntPtr.Zero

  public AddClause (clause : array [Lit]) : void
    log (SAT, $ "add_clause($(List.FromArray(clause)))")
    unless (core == null) core.TheDriver.clause_count++
    minisat_add_clause (handle, clause, clause.Length)

  /** Return true iff formula is satisfable.
  
      Once we get [false] from here, you will always get [false], there is
      no possibility of backtrack.  */
  [Profile] \
  public Solve () : bool
    minisat_solve (handle) != 0
  
  /** Available only if last call to [Solve] returned [true].  */
  public Model : array [int]
    [Profile] \
    get
      def ar = array (minisat_get_model (handle, null))
      _ = minisat_get_model (handle, ar)
      log (SAT, $"model = $(List.FromArray (ar))")
      ar

  public TrySolveWith (var_cnt : int, assumptions : array [Lit]) : array [uint]
    def model = array (var_cnt / 32 + 3)
    def res = minisat_try_solve_with (handle, assumptions, assumptions.Length, 
                                      model, model.Length)
    if (res == 0) null
    else model

  /** Assume [assumptions], and try to solve. If it returns UNSAT, return
      the set of assumptions that caused the conflict. Otherwise blow up.  */
  public SolveWith (assumptions : array [Lit]) : array [int]
    def size = minisat_solve_with (handle, assumptions, assumptions.Length)
    def conflict = array (size)
    minisat_get_conflict (handle, conflict)
    conflict