{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Store.CNF
-- Copyright   :  (c) Masahiro Sakai 2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.SAT.Store.CNF
  ( CNFStore
  , newCNFStore
  , getCNFFormula
  ) where

import Control.Monad.Primitive
import qualified Data.Foldable as F
import Data.Primitive.MutVar
import Data.Sequence (Seq, (|>))
import qualified Data.Sequence as Seq
import qualified ToySolver.FileFormat.CNF as CNF
import qualified ToySolver.SAT.Types as SAT

data CNFStore m = CNFStore (MutVar (PrimState m) Int) (MutVar (PrimState m) (Seq SAT.PackedClause))

instance PrimMonad m => SAT.NewVar m (CNFStore m) where
  newVar :: CNFStore m -> m Var
newVar (CNFStore MutVar (PrimState m) Var
ref MutVar (PrimState m) (Seq PackedClause)
_) = do
    forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar' MutVar (PrimState m) Var
ref (forall a. Num a => a -> a -> a
+Var
1)
    forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) Var
ref

instance PrimMonad m => SAT.AddClause m (CNFStore m) where
  addClause :: CNFStore m -> [Var] -> m ()
addClause (CNFStore MutVar (PrimState m) Var
_ MutVar (PrimState m) (Seq PackedClause)
ref) [Var]
clause =
    case [Var] -> Maybe [Var]
SAT.normalizeClause [Var]
clause of
      Just [Var]
clause' -> do
        let clause'' :: PackedClause
clause'' = [Var] -> PackedClause
SAT.packClause [Var]
clause'
        seq :: forall a b. a -> b -> b
seq PackedClause
clause'' forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar' MutVar (PrimState m) (Seq PackedClause)
ref (forall a. Seq a -> a -> Seq a
|> PackedClause
clause'')
      Maybe [Var]
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

newCNFStore :: PrimMonad m => m (CNFStore m)
newCNFStore :: forall (m :: * -> *). PrimMonad m => m (CNFStore m)
newCNFStore = do
  MutVar (PrimState m) Var
ref1 <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Var
0
  MutVar (PrimState m) (Seq PackedClause)
ref2 <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall a. Seq a
Seq.empty
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall (m :: * -> *).
MutVar (PrimState m) Var
-> MutVar (PrimState m) (Seq PackedClause) -> CNFStore m
CNFStore MutVar (PrimState m) Var
ref1 MutVar (PrimState m) (Seq PackedClause)
ref2)

getCNFFormula :: PrimMonad m => CNFStore m -> m CNF.CNF
getCNFFormula :: forall (m :: * -> *). PrimMonad m => CNFStore m -> m CNF
getCNFFormula (CNFStore MutVar (PrimState m) Var
ref1 MutVar (PrimState m) (Seq PackedClause)
ref2) = do
  Var
nv <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) Var
ref1
  Seq PackedClause
cs <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) (Seq PackedClause)
ref2
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
     CNF.CNF
     { cnfNumVars :: Var
CNF.cnfNumVars = Var
nv
     , cnfNumClauses :: Var
CNF.cnfNumClauses = forall a. Seq a -> Var
Seq.length Seq PackedClause
cs
     , cnfClauses :: [PackedClause]
CNF.cnfClauses = forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq PackedClause
cs
     }