{-# 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.Array.MArray
import Data.Array.ST
import Data.Foldable (toList)
import Data.Sequence ((<|), (|>))
import qualified Data.Sequence as Seq
import Data.STRef

import ToySolver.Converter.Base
import qualified ToySolver.FileFormat.CNF as CNF
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 forall a. Ord a => a -> a -> Bool
< Int
3 = forall a. HasCallStack => [Char] -> a
error [Char]
"ToySolver.Converter.SAT2KSAT.sat2ksat: k must be >=3"
sat2ksat Int
k CNF
cnf = forall a. (forall s. ST s a) -> a
runST forall a b. (a -> b) -> a -> b
$ do
  let nv1 :: Int
nv1 = CNF -> Int
CNF.cnfNumVars CNF
cnf
  CNFStore (ST s)
db <- forall (m :: * -> *). PrimMonad m => m (CNFStore m)
newCNFStore
  STRef s (Seq (Int, [Int]))
defsRef <- forall a s. a -> ST s (STRef s a)
newSTRef forall a. Seq a
Seq.empty
  forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ CNFStore (ST s)
db Int
nv1
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf) forall a b. (a -> b) -> a -> b
$ \PackedClause
clause -> do
    let loop :: Seq Int -> ST s ()
loop Seq Int
lits = do
          if forall a. Seq a -> Int
Seq.length Seq Int
lits forall a. Ord a => a -> a -> Bool
<= Int
k then
            forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause CNFStore (ST s)
db (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq Int
lits)
          else do
            Int
v <- forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar CNFStore (ST s)
db
            case forall a. Int -> Seq a -> (Seq a, Seq a)
Seq.splitAt (Int
kforall a. Num a => a -> a -> a
-Int
1) Seq Int
lits of
              (Seq Int
lits1, Seq Int
lits2) -> do
                forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause CNFStore (ST s)
db (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Seq Int
lits1 forall a. Seq a -> a -> Seq a
|> (-Int
v)))
                forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef' STRef s (Seq (Int, [Int]))
defsRef (forall a. Seq a -> a -> Seq a
|> (Int
v, forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq Int
lits1))
                Seq Int -> ST s ()
loop (Int
v forall a. a -> Seq a -> Seq a
<| Seq Int
lits2)
    Seq Int -> ST s ()
loop forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Seq a
Seq.fromList forall a b. (a -> b) -> a -> b
$ PackedClause -> [Int]
SAT.unpackClause PackedClause
clause
  CNF
cnf2 <- forall (m :: * -> *). PrimMonad m => CNFStore m -> m CNF
getCNFFormula CNFStore (ST s)
db
  Seq (Int, [Int])
defs <- forall s a. STRef s a -> ST s a
readSTRef STRef s (Seq (Int, [Int]))
defsRef
  forall (m :: * -> *) a. Monad m => a -> m a
return (CNF
cnf2, Int -> Int -> Seq (Int, [Int]) -> SAT2KSATInfo
SAT2KSATInfo Int
nv1 (CNF -> Int
CNF.cnfNumVars CNF
cnf2) Seq (Int, [Int])
defs)


data SAT2KSATInfo = SAT2KSATInfo !Int !Int (Seq.Seq (SAT.Var, [SAT.Lit]))
  deriving (SAT2KSATInfo -> SAT2KSATInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SAT2KSATInfo -> SAT2KSATInfo -> Bool
$c/= :: SAT2KSATInfo -> SAT2KSATInfo -> Bool
== :: SAT2KSATInfo -> SAT2KSATInfo -> Bool
$c== :: SAT2KSATInfo -> SAT2KSATInfo -> Bool
Eq, Int -> SAT2KSATInfo -> ShowS
[SAT2KSATInfo] -> ShowS
SAT2KSATInfo -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [SAT2KSATInfo] -> ShowS
$cshowList :: [SAT2KSATInfo] -> ShowS
show :: SAT2KSATInfo -> [Char]
$cshow :: SAT2KSATInfo -> [Char]
showsPrec :: Int -> SAT2KSATInfo -> ShowS
$cshowsPrec :: Int -> SAT2KSATInfo -> ShowS
Show, ReadPrec [SAT2KSATInfo]
ReadPrec SAT2KSATInfo
Int -> ReadS SAT2KSATInfo
ReadS [SAT2KSATInfo]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [SAT2KSATInfo]
$creadListPrec :: ReadPrec [SAT2KSATInfo]
readPrec :: ReadPrec SAT2KSATInfo
$creadPrec :: ReadPrec SAT2KSATInfo
readList :: ReadS [SAT2KSATInfo]
$creadList :: ReadS [SAT2KSATInfo]
readsPrec :: Int -> ReadS SAT2KSATInfo
$creadsPrec :: Int -> ReadS SAT2KSATInfo
Read)

instance Transformer SAT2KSATInfo where
  type Source SAT2KSATInfo = SAT.Model
  type Target SAT2KSATInfo = SAT.Model

instance ForwardTransformer SAT2KSATInfo where
  transformForward :: SAT2KSATInfo -> Source SAT2KSATInfo -> Target SAT2KSATInfo
transformForward (SAT2KSATInfo Int
nv1 Int
nv2 Seq (Int, [Int])
defs) Source SAT2KSATInfo
m = forall i e. (forall s. ST s (STUArray s i e)) -> UArray i e
runSTUArray forall a b. (a -> b) -> a -> b
$ do
    STUArray s Int Bool
m2 <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Int
1,Int
nv2)
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int
1..Int
nv1] forall a b. (a -> b) -> a -> b
$ \Int
v -> do
      forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray STUArray s Int Bool
m2 Int
v (forall a. IModel a => a -> Int -> Bool
SAT.evalVar Source SAT2KSATInfo
m Int
v)
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq (Int, [Int])
defs) forall a b. (a -> b) -> a -> b
$ \(Int
v, [Int]
clause) -> do
      let f :: Int -> ST s Bool
f Int
lit =
            if Int
lit forall a. Ord a => a -> a -> Bool
> Int
0 then
              forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray STUArray s Int Bool
m2 Int
lit
            else
              forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Bool -> Bool
not (forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray STUArray s Int Bool
m2 (- Int
lit))
      Bool
val <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (t :: * -> *). Foldable t => t Bool -> Bool
or (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Int -> ST s Bool
f [Int]
clause)
      forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray STUArray s Int Bool
m2 Int
v Bool
val
    forall (m :: * -> *) a. Monad m => a -> m a
return STUArray s Int Bool
m2

instance BackwardTransformer SAT2KSATInfo where
  transformBackward :: SAT2KSATInfo -> Target SAT2KSATInfo -> Source SAT2KSATInfo
transformBackward (SAT2KSATInfo Int
nv1 Int
_nv2 Seq (Int, [Int])
_defs) = Int -> UArray Int Bool -> UArray Int Bool
SAT.restrictModel Int
nv1

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