using Nemerle.Collections
using Nemerle.Utility
using Nemerle.Logging

set namespace Fx7

public class Clause
  public Lits : array [Literal]
  public mutable Score : double
  public mutable Promoted : int
  public mutable Usefulness : int

  public Proof : Rule

  public this (l : array [Literal], proof : Rule)
    Lits = l
    assert (!Driver.ProofLogging || proof != null)
    Proof = proof

  public override ToString () : string
    $ "$Score: $($[l | l in Lits])"

  public MakeProof () : Proof
    Lits.FoldLeft (Proof.True (), (l, p) => Proof.Rule2 ("clause-to-proof", Proof.Leaf (~l), p))