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

set namespace Fx7

public class InternalCNF : ToCNF
  dpll : DPLLSolver

  public this (c : Core, p : ToCNF, dpll : DPLLSolver)
    base (c, p)
    this.dpll = dpll
    Init ()

  protected override AddClauseImpl (kind : ClauseKind, c : array [SatSolver.Lit]) : void
    dpll.AddClause (kind, c)

  protected override NewLitImpl (no : int) : void
    while (dpll.nVars () <= no)
      _ = dpll.newVar ()
    dpll.CreateVar (no)

  public override GetQMonome () : list [Literal]
    dpll.GetQMonome ()