-- Copyright (C) 2016 Peter Selinger.
--
-- This file is free software and may be distributed under the terms
-- of the MIT license. Please see the file LICENSE for details.

-- | A functional (non-monadic) interface to the functions of
-- "SAT.MiniSat.Monadic". This layer:
--
-- * hides the existence of a solver object by providing a function
--   mapping SAT instances to a lazy list of solutions.

module SAT.MiniSat.Functional where

import SAT.MiniSat.Monadic
import SAT.MiniSat.Literals

-- | Input a CNF and output the a (lazily generated) list of
-- solutions. Variables are represented as integers, which should be
-- consecutive and start from 0.
m_solve :: [[Lit Int]] -> [[Maybe Bool]]
m_solve clauses = m_run $ do
  r <- m_solver_addclauses clauses
  if r == False then do
    return []
    else do
    m_solver_solve_start
    sols <- m_solver_next_solutions
    return sols