{-# 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 :: Int -> CNF -> (CNF, SAT2KSATInfo)
sat2ksat Int
k CNF
_ | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
3 = [Char] -> (CNF, SAT2KSATInfo)
forall a. HasCallStack => [Char] -> a
error [Char]
"ToySolver.Converter.SAT2KSAT.sat2ksat: k must be >=3"
sat2ksat Int
k CNF
cnf = (forall s. ST s (CNF, SAT2KSATInfo)) -> (CNF, SAT2KSATInfo)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (CNF, SAT2KSATInfo)) -> (CNF, SAT2KSATInfo))
-> (forall s. ST s (CNF, SAT2KSATInfo)) -> (CNF, SAT2KSATInfo)
forall a b. (a -> b) -> a -> b
$ do
  let nv1 :: Int
nv1 = CNF -> Int
CNF.cnfNumVars CNF
cnf
  CNFStore (ST s)
db <- ST s (CNFStore (ST s))
forall (m :: * -> *). PrimMonad m => m (CNFStore m)
newCNFStore
  STRef s (IntMap [Int])
defsRef <- IntMap [Int] -> ST s (STRef s (IntMap [Int]))
forall a s. a -> ST s (STRef s a)
newSTRef IntMap [Int]
forall a. IntMap a
IntMap.empty
  CNFStore (ST s) -> Int -> ST s ()
forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ CNFStore (ST s)
db Int
nv1
  [PackedClause] -> (PackedClause -> ST s ()) -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf) ((PackedClause -> ST s ()) -> ST s ())
-> (PackedClause -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \PackedClause
clause -> do
    let loop :: Seq Int -> ST s ()
loop Seq Int
lits = do
          if Seq Int -> Int
forall a. Seq a -> Int
Seq.length Seq Int
lits Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
k then
            CNFStore (ST s) -> [Int] -> ST s ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause CNFStore (ST s)
db (Seq Int -> [Int]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq Int
lits)
          else do
            Int
v <- CNFStore (ST s) -> ST s Int
forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar CNFStore (ST s)
db
            case Int -> Seq Int -> (Seq Int, Seq Int)
forall a. Int -> Seq a -> (Seq a, Seq a)
Seq.splitAt (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Seq Int
lits of
              (Seq Int
lits1, Seq Int
lits2) -> do
                CNFStore (ST s) -> [Int] -> ST s ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause CNFStore (ST s)
db (Seq Int -> [Int]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Seq Int
lits1 Seq Int -> Int -> Seq Int
forall a. Seq a -> a -> Seq a
|> (-Int
v)))
                STRef s (IntMap [Int]) -> (IntMap [Int] -> IntMap [Int]) -> ST s ()
forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef' STRef s (IntMap [Int])
defsRef (Int -> [Int] -> IntMap [Int] -> IntMap [Int]
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
v (Seq Int -> [Int]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq Int
lits1))
                Seq Int -> ST s ()
loop (Int
v Int -> Seq Int -> Seq Int
forall a. a -> Seq a -> Seq a
<| Seq Int
lits2)
    Seq Int -> ST s ()
loop (Seq Int -> ST s ()) -> Seq Int -> ST s ()
forall a b. (a -> b) -> a -> b
$ [Int] -> Seq Int
forall a. [a] -> Seq a
Seq.fromList ([Int] -> Seq Int) -> [Int] -> Seq Int
forall a b. (a -> b) -> a -> b
$ PackedClause -> [Int]
SAT.unpackClause PackedClause
clause
  CNF
cnf2 <- CNFStore (ST s) -> ST s CNF
forall (m :: * -> *). PrimMonad m => CNFStore m -> m CNF
getCNFFormula CNFStore (ST s)
db
  IntMap [Int]
defs <- STRef s (IntMap [Int]) -> ST s (IntMap [Int])
forall s a. STRef s a -> ST s a
readSTRef STRef s (IntMap [Int])
defsRef
  (CNF, SAT2KSATInfo) -> ST s (CNF, SAT2KSATInfo)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (CNF
cnf2, Int -> Int -> VarMap Formula -> SAT2KSATInfo
TseitinInfo Int
nv1 (CNF -> Int
CNF.cnfNumVars CNF
cnf2) (([Int] -> Formula) -> IntMap [Int] -> VarMap Formula
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[Int]
clause -> [Formula] -> Formula
Or [Int -> Formula
atom Int
lit | Int
lit <- [Int]
clause]) IntMap [Int]
defs))
  where
    atom :: Int -> Formula
atom Int
l
      | Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = Formula -> Formula
Not (Int -> Formula
Atom (- Int
l))
      | Bool
otherwise = Int -> Formula
Atom Int
l


type SAT2KSATInfo = TseitinInfo

-- -----------------------------------------------------------------------------