using Nemerle.Profiling
using Nemerle
using Nemerle.Utility

set namespace Fx7

[Rollbackable] \
public class Literal
  public atom : Atom
  public is_neg : bool

  public pool : SimpleSolver

  public mutable Score : double

  [Accessor] [Copy] mutable is_true : bool
  [Copy] mutable is_expanded : bool
  [Copy] mutable is_expanded_cfl : bool
  //[Copy] mutable current_users : list [Clause] = []

  // the clause that caused this literal to be set to true, if any
  [Accessor] [Copy] mutable reason : Clause
  // also set for after-case-split subsumption
  [Accessor] [Copy] mutable is_case_split : bool

  public IsNeg : bool
    get { is_neg }

  public IsPos : bool
    get { ! is_neg }

  public IsFalse : bool
    get
      (~this).is_true

  public IsPossible : bool
    get
      !IsFalse

  public IsUnset : bool
    get
      !is_true && !(~this).is_true

  public IsExpanded [kind : ClauseKind] : bool
    get
      match (kind)
        | Current => is_expanded
        | Conflict => is_expanded_cfl
        | Pending => true
    set
      WillWrite ()
      assert (value)
      match (kind)
        | Current => is_expanded = true; is_expanded_cfl = true
        | Conflict => is_expanded_cfl = true
        | Pending => assert (false)


  public this (p : SimpleSolver, atom : Atom, is_neg : bool)
    this.pool = p
    this.atom = atom
    this.is_neg = is_neg
    this.is_expanded = !(atom is PAtom)
    this.is_expanded_cfl = this.is_expanded
    assert (atom.GetLiteral (is_neg) == null)

  public MakeTrue (is_case_split : bool, reason : Clause) : void
    WillWrite ()
    assert (!IsFalse)
    is_true = true
    this.reason = reason
    this.is_case_split = is_case_split

  public override ToString () : string
    if (is_neg) $ "(not $atom)"
    else atom.ToString ()

  public ToSimplString () : string
    if (is_neg) $ "(NOT $(atom.ToSimplString()))"
    else atom.ToSimplString ()

  public ToTerm (c : Core = null) : Term
    def c = if (c == null) atom.term1.Core else c
    def a = atom.ToTerm (c)
    if (is_neg) c.TermPool.Get ("not", [a])
    else a

  public static @~ (n : Literal) : Literal
    n.atom.GetLiteral (! n.is_neg)

  public Abs : Literal
    get
      if (is_neg) ~this else this

  public override GetHashCode () : int
    unchecked
      atom.GetHashCode () ^
        if (is_neg) 92873 else 0
    
  [Nemerle.OverrideObjectEquals] \
  public Equals (that : Literal) : bool
    is_neg == that.is_neg && atom.Equals (that.atom)