{-# 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 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 (Seq (Int, [Int]))
defsRef <- Seq (Int, [Int]) -> ST s (STRef s (Seq (Int, [Int])))
forall a s. a -> ST s (STRef s a)
newSTRef Seq (Int, [Int])
forall a. Seq a
Seq.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 (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 (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 (Seq (Int, [Int]))
-> (Seq (Int, [Int]) -> Seq (Int, [Int])) -> ST s ()
forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef' STRef s (Seq (Int, [Int]))
defsRef (Seq (Int, [Int]) -> (Int, [Int]) -> Seq (Int, [Int])
forall a. Seq a -> a -> Seq a
|> (Int
v, Seq Int -> [Int]
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
  Seq (Int, [Int])
defs <- STRef s (Seq (Int, [Int])) -> ST s (Seq (Int, [Int]))
forall s a. STRef s a -> ST s a
readSTRef STRef s (Seq (Int, [Int]))
defsRef
  (CNF, SAT2KSATInfo) -> ST s (CNF, SAT2KSATInfo)
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
(SAT2KSATInfo -> SAT2KSATInfo -> Bool)
-> (SAT2KSATInfo -> SAT2KSATInfo -> Bool) -> Eq SAT2KSATInfo
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]
(Int -> SAT2KSATInfo -> ShowS)
-> (SAT2KSATInfo -> [Char])
-> ([SAT2KSATInfo] -> ShowS)
-> Show SAT2KSATInfo
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]
(Int -> ReadS SAT2KSATInfo)
-> ReadS [SAT2KSATInfo]
-> ReadPrec SAT2KSATInfo
-> ReadPrec [SAT2KSATInfo]
-> Read 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 s. ST s (STUArray s Int Bool)) -> UArray Int Bool
forall i e. (forall s. ST s (STUArray s i e)) -> UArray i e
runSTUArray ((forall s. ST s (STUArray s Int Bool)) -> UArray Int Bool)
-> (forall s. ST s (STUArray s Int Bool)) -> UArray Int Bool
forall a b. (a -> b) -> a -> b
$ do
    STUArray s Int Bool
m2 <- (Int, Int) -> ST s (STUArray s Int Bool)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Int
1,Int
nv2)
    [Int] -> (Int -> ST s ()) -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int
1..Int
nv1] ((Int -> ST s ()) -> ST s ()) -> (Int -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \Int
v -> do
      STUArray s Int Bool -> Int -> Bool -> ST s ()
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 (UArray Int Bool -> Int -> Bool
forall a. IModel a => a -> Int -> Bool
SAT.evalVar UArray Int Bool
Source SAT2KSATInfo
m Int
v)
    [(Int, [Int])] -> ((Int, [Int]) -> ST s ()) -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Seq (Int, [Int]) -> [(Int, [Int])]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq (Int, [Int])
defs) (((Int, [Int]) -> ST s ()) -> ST s ())
-> ((Int, [Int]) -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \(Int
v, [Int]
clause) -> do
      let f :: Int -> ST s Bool
f Int
lit =
            if Int
lit Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then
              STUArray s Int Bool -> Int -> ST s Bool
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
              (Bool -> Bool) -> ST s Bool -> ST s Bool
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Bool -> Bool
not (STUArray s Int Bool -> Int -> ST s Bool
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 <- ([Bool] -> Bool) -> ST s [Bool] -> ST s Bool
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ((Int -> ST s Bool) -> [Int] -> ST s [Bool]
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)
      STUArray s Int Bool -> Int -> Bool -> ST s ()
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
    STUArray s Int Bool -> ST s (STUArray s Int Bool)
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

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