{-# OPTIONS_GHC -Wall #-}
--------------------------------------------------------------------
-- |
-- Copyright :  © Masahiro Sakai 2014
-- License   :  BSD3
-- Maintainer:  Masahiro Sakai <masahiro.sakai@gmail.com>
-- Stability :  experimental
-- Portability: portable
--
--------------------------------------------------------------------
module Ersatz.Solver.Toysat where

import Control.Monad
import Control.Monad.IO.Class
import Data.Array.IArray
import qualified Data.Foldable as F
import qualified Data.IntSet as IntSet
import qualified Data.IntMap as IntMap
import Ersatz
import qualified ToySolver.SAT as ToySAT

toysat :: MonadIO m => Solver SAT m
toysat problem = liftIO $ do
  solver <- ToySAT.newSolver
  let nv = dimacsNumVariables problem
  ToySAT.newVars_ solver nv
  F.forM_ (dimacsClauses problem) $ \clause -> do
    ToySAT.addClause solver (IntSet.toList clause)
  ret <- ToySAT.solve solver
  if ret then do
    model <- ToySAT.getModel solver
    return (Satisfied, IntMap.fromList (assocs model))
  else
    return (Unsatisfied, IntMap.empty)