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

set namespace Fx7

public class ExternalCNF : ToCNF
  [Accessor] solver : SatSolver

  public this (c : Core, p : ToCNF)
    base (c, p)
    solver = SatSolver (c)
    Init ()

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

  /// First positive, then negative
  [Profile] \
  public GetMonome (skip_asserted = false) : list [Literal]
    def need_case_splits = parent != null && Driver.DumpQuantStats
    def model = solver.Model
    when (need_case_splits)
      CheckForSplits (model)
    ToLiterals (model, skip_asserted)
    
  public Solve () : bool
    solver.Solve ()

  public override GetQMonome () : list [Literal]
    GetMonome ()