module Satchmo.Solver.Funsat

( solve
)

where

import qualified Satchmo.Data
import qualified Satchmo.Solve


import qualified Language.CNF.Parse.ParseDIMACS as ParseCNF
import qualified Funsat.Solver
import Funsat.Types

import Data.String
import Data.Array.Unboxed
import qualified Data.Map as M
import qualified Data.Set as S

solve = Satchmo.Solve.solve funsat

funsat :: Satchmo.Solve.Implementation
funsat cs = do
    let Right cnf = ParseCNF.parseByteString "satchmo"
                  $ fromString cs
        result @ ( sol, stats, mtrace ) = Funsat.Solver.solve1 $ asCNF cnf
    case result of
        ( Funsat.Solver.Sat a, _, _ ) -> 
            return $ Just $ M.fromList $ do
                l <- litAssignment a
                return ( Satchmo.Data.literal $ abs $ unLit l, litSign l )
        _ -> return Nothing

-- | Convert parsed CNF to internal representation.
-- this code snippet is stolen from funsat-0.5.2/Main.hs
asCNF :: ParseCNF.CNF -> CNF
asCNF (ParseCNF.CNF v c is) =
    CNF { numVars    = v
        , numClauses = c
        , clauses    = S.fromList . map (map fromIntegral . elems) $ is 
        }