content: {-# OPTIONS_GHC -Wall #-}
  {-# OPTIONS_HADDOCK show-extensions #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE TypeFamilies #-}
  -----------------------------------------------------------------------------
  -- |
  -- Module      :  ToySolver.Converter.SAT2KSAT
  -- Copyright   :  (c) Masahiro Sakai 2016
  -- License     :  BSD-style
  --
  -- Maintainer  :  masahiro.sakai@gmail.com
  -- Stability   :  experimental
  -- Portability :  non-portable
  --
  -----------------------------------------------------------------------------
  module ToySolver.Converter.SAT2KSAT
    ( sat2ksat
    , SAT2KSATInfo
    ) where
  
  import Control.Monad
  import Control.Monad.ST
  import Data.Foldable (toList)
  import qualified Data.IntMap.Lazy as IntMap
  import Data.Sequence ((<|), (|>))
  import qualified Data.Sequence as Seq
  import Data.STRef
  
  import ToySolver.Converter.Tseitin
  import qualified ToySolver.FileFormat.CNF as CNF
  import ToySolver.SAT.Formula
  import qualified ToySolver.SAT.Types as SAT
  import ToySolver.SAT.Store.CNF
  
  
  sat2ksat :: Int -> CNF.CNF -> (CNF.CNF, SAT2KSATInfo)
  sat2ksat k _ | k < 3 = error "ToySolver.Converter.SAT2KSAT.sat2ksat: k must be >=3"
  sat2ksat k cnf = runST $ do
    let nv1 = CNF.cnfNumVars cnf
    db <- newCNFStore
    defsRef <- newSTRef IntMap.empty
    SAT.newVars_ db nv1
    forM_ (CNF.cnfClauses cnf) $ \clause -> do
      let loop lits = do
            if Seq.length lits <= k then
              SAT.addClause db (toList lits)
            else do
              v <- SAT.newVar db
              case Seq.splitAt (k-1) lits of
                (lits1, lits2) -> do
                  SAT.addClause db (toList (lits1 |> (-v)))
                  modifySTRef' defsRef (IntMap.insert v (toList lits1))
                  loop (v <| lits2)
      loop $ Seq.fromList $ SAT.unpackClause clause
    cnf2 <- getCNFFormula db
    defs <- readSTRef defsRef
    return (cnf2, TseitinInfo nv1 (CNF.cnfNumVars cnf2) (fmap (\clause -> Or [atom lit | lit <- clause]) defs))
    where
      atom l
        | l < 0 = Not (Atom (- l))
        | otherwise = Atom l
  
  
  type SAT2KSATInfo = TseitinInfo
  
  -- -----------------------------------------------------------------------------
  