-- 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 :: [[Lit Int]] -> [[Maybe Bool]]
m_solve [[Lit Int]]
clauses = SolverState [[Maybe Bool]] -> [[Maybe Bool]]
forall a. SolverState a -> a
m_run (SolverState [[Maybe Bool]] -> [[Maybe Bool]])
-> SolverState [[Maybe Bool]] -> [[Maybe Bool]]
forall a b. (a -> b) -> a -> b
$ do
  Bool
r <- [[Lit Int]] -> SolverState Bool
m_solver_addclauses [[Lit Int]]
clauses
  if Bool
r Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
False then do
    [[Maybe Bool]] -> SolverState [[Maybe Bool]]
forall a. a -> StateT Solver Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    else do
    SolverState ()
m_solver_solve_start
    [[Maybe Bool]]
sols <- SolverState [[Maybe Bool]]
m_solver_next_solutions
    [[Maybe Bool]] -> SolverState [[Maybe Bool]]
forall a. a -> StateT Solver Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return [[Maybe Bool]]
sols