{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE TypeFamilies #-}
module ToySolver.Converter.SAT2MIS
  (
  -- * SAT to independent set problem conversion
    satToIS
  , SAT2ISInfo

  -- * 3-SAT to independent set problem conversion
  , sat3ToIS
  , SAT3ToISInfo

  -- * Maximum independent problem to MaxSAT/PB problem conversion
  , is2pb
  , mis2MaxSAT
  , IS2SATInfo
  ) where

import Control.Monad
import Control.Monad.ST
import Data.Array.IArray
import Data.Array.ST
import Data.Array.Unboxed
import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import Data.IntSet (IntSet)
import Data.Maybe
import Data.STRef

import qualified Data.PseudoBoolean as PBFile

import ToySolver.Converter.Base
import ToySolver.Converter.SAT2KSAT
import qualified ToySolver.FileFormat.CNF as CNF
import ToySolver.Graph.Base
import ToySolver.SAT.Store.CNF
import ToySolver.SAT.Store.PB
import qualified ToySolver.SAT.Types as SAT

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

satToIS :: CNF.CNF -> ((Graph, Int), SAT2ISInfo)
satToIS :: CNF -> ((Graph, Int), SAT2ISInfo)
satToIS CNF
x = ((Graph, Int)
x2, (SAT2KSATInfo -> SAT3ToISInfo -> SAT2ISInfo
forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer SAT2KSATInfo
info1 SAT3ToISInfo
info2))
  where
    (CNF
x1, SAT2KSATInfo
info1) = Int -> CNF -> (CNF, SAT2KSATInfo)
sat2ksat Int
3 CNF
x
    ((Graph, Int)
x2, SAT3ToISInfo
info2) = CNF -> ((Graph, Int), SAT3ToISInfo)
sat3ToIS CNF
x1

type SAT2ISInfo = ComposedTransformer SAT2KSATInfo SAT3ToISInfo

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

sat3ToIS :: CNF.CNF -> ((Graph, Int), SAT3ToISInfo)
sat3ToIS :: CNF -> ((Graph, Int), SAT3ToISInfo)
sat3ToIS CNF
cnf = (forall s. ST s ((Graph, Int), SAT3ToISInfo))
-> ((Graph, Int), SAT3ToISInfo)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s ((Graph, Int), SAT3ToISInfo))
 -> ((Graph, Int), SAT3ToISInfo))
-> (forall s. ST s ((Graph, Int), SAT3ToISInfo))
-> ((Graph, Int), SAT3ToISInfo)
forall a b. (a -> b) -> a -> b
$ do
  STRef s Int
nRef <- Int -> ST s (STRef s Int)
forall a s. a -> ST s (STRef s a)
newSTRef Int
0
  STRef s (IntMap [Int])
litToNodesRef <- 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
  STRef s [Int]
nodeToLitRef <- [Int] -> ST s (STRef s [Int])
forall a s. a -> ST s (STRef s a)
newSTRef []
  let newNode :: Int -> ST s Int
newNode Int
lit = do
        Int
n <- STRef s Int -> ST s Int
forall s a. STRef s a -> ST s a
readSTRef STRef s Int
nRef
        STRef s Int -> Int -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s Int
nRef (Int -> ST s ()) -> Int -> ST s ()
forall a b. (a -> b) -> a -> b
$! Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
        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])
litToNodesRef ((Maybe [Int] -> Maybe [Int]) -> Int -> IntMap [Int] -> IntMap [Int]
forall a. (Maybe a -> Maybe a) -> Int -> IntMap a -> IntMap a
IntMap.alter ([Int] -> Maybe [Int]
forall a. a -> Maybe a
Just ([Int] -> Maybe [Int])
-> (Maybe [Int] -> [Int]) -> Maybe [Int] -> Maybe [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int
n Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:) ([Int] -> [Int]) -> (Maybe [Int] -> [Int]) -> Maybe [Int] -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> Maybe [Int] -> [Int]
forall a. a -> Maybe a -> a
fromMaybe []) Int
lit)
        STRef s [Int] -> ([Int] -> [Int]) -> ST s ()
forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef STRef s [Int]
nodeToLitRef (Int
lit Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:)
        Int -> ST s Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n

  [[Int]]
clusters <- [PackedClause] -> (PackedClause -> ST s [Int]) -> ST s [[Int]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf) ((PackedClause -> ST s [Int]) -> ST s [[Int]])
-> (PackedClause -> ST s [Int]) -> ST s [[Int]]
forall a b. (a -> b) -> a -> b
$ \PackedClause
clause -> do
    (Int -> ST s Int) -> [Int] -> ST s [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Int -> ST s Int
newNode (PackedClause -> [Int]
SAT.unpackClause PackedClause
clause)

  IntMap [Int]
litToNodes <- STRef s (IntMap [Int]) -> ST s (IntMap [Int])
forall s a. STRef s a -> ST s a
readSTRef STRef s (IntMap [Int])
litToNodesRef
  let es :: [(Int, Int, ())]
es = [[(Int, Int, ())]] -> [(Int, Int, ())]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Int, Int, ())]] -> [(Int, Int, ())])
-> [[(Int, Int, ())]] -> [(Int, Int, ())]
forall a b. (a -> b) -> a -> b
$
        [ [(Int
node1, Int
node2, ()) | (Int
node1, Int
node2) <- [Int] -> [(Int, Int)]
forall a. [a] -> [(a, a)]
pairs [Int]
nodes] | [Int]
nodes <- [[Int]]
clusters ] [[(Int, Int, ())]] -> [[(Int, Int, ())]] -> [[(Int, Int, ())]]
forall a. [a] -> [a] -> [a]
++
        [ [(Int
node1, Int
node2, ()) | Int
node1 <- [Int]
nodes1, Int
node2 <- [Int]
nodes2]
        | (Int
lit, [Int]
nodes1) <- IntMap [Int] -> [(Int, [Int])]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap [Int]
litToNodes
        , let nodes2 :: [Int]
nodes2 = [Int] -> Int -> IntMap [Int] -> [Int]
forall a. a -> Int -> IntMap a -> a
IntMap.findWithDefault [] (- Int
lit) IntMap [Int]
litToNodes
        ]

  Int
n <- STRef s Int -> ST s Int
forall s a. STRef s a -> ST s a
readSTRef STRef s Int
nRef
  let g :: Graph
g = Int -> [(Int, Int, ())] -> Graph
forall a. Int -> [(Int, Int, a)] -> EdgeLabeledGraph a
graphFromUnorderedEdges Int
n [(Int, Int, ())]
es

  [Int]
xs <- STRef s [Int] -> ST s [Int]
forall s a. STRef s a -> ST s a
readSTRef STRef s [Int]
nodeToLitRef
  let nodeToLit :: UArray Int Int
nodeToLit = (forall s. ST s (STUArray s Int Int)) -> UArray Int Int
forall i e. (forall s. ST s (STUArray s i e)) -> UArray i e
runSTUArray ((forall s. ST s (STUArray s Int Int)) -> UArray Int Int)
-> (forall s. ST s (STUArray s Int Int)) -> UArray Int Int
forall a b. (a -> b) -> a -> b
$ do
        STUArray s Int Int
a <- (Int, Int) -> ST s (STUArray s Int Int)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Int
0,Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
        [(Int, Int)] -> ((Int, Int) -> ST s ()) -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1,Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
2..] [Int]
xs) (((Int, Int) -> ST s ()) -> ST s ())
-> ((Int, Int) -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \(Int
i, Int
lit) -> do
          STUArray s Int Int -> Int -> Int -> ST s ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray STUArray s Int Int
a Int
i Int
lit
        STUArray s Int Int -> ST s (STUArray s Int Int)
forall (m :: * -> *) a. Monad m => a -> m a
return STUArray s Int Int
a

  ((Graph, Int), SAT3ToISInfo) -> ST s ((Graph, Int), SAT3ToISInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Graph
g, CNF -> Int
CNF.cnfNumClauses CNF
cnf), Int -> [[Int]] -> UArray Int Int -> SAT3ToISInfo
SAT3ToISInfo (CNF -> Int
CNF.cnfNumVars CNF
cnf) [[Int]]
clusters UArray Int Int
nodeToLit)


data SAT3ToISInfo = SAT3ToISInfo Int [[Int]] (UArray Int SAT.Lit)
  deriving (SAT3ToISInfo -> SAT3ToISInfo -> Bool
(SAT3ToISInfo -> SAT3ToISInfo -> Bool)
-> (SAT3ToISInfo -> SAT3ToISInfo -> Bool) -> Eq SAT3ToISInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SAT3ToISInfo -> SAT3ToISInfo -> Bool
$c/= :: SAT3ToISInfo -> SAT3ToISInfo -> Bool
== :: SAT3ToISInfo -> SAT3ToISInfo -> Bool
$c== :: SAT3ToISInfo -> SAT3ToISInfo -> Bool
Eq, Int -> SAT3ToISInfo -> ShowS
[SAT3ToISInfo] -> ShowS
SAT3ToISInfo -> String
(Int -> SAT3ToISInfo -> ShowS)
-> (SAT3ToISInfo -> String)
-> ([SAT3ToISInfo] -> ShowS)
-> Show SAT3ToISInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SAT3ToISInfo] -> ShowS
$cshowList :: [SAT3ToISInfo] -> ShowS
show :: SAT3ToISInfo -> String
$cshow :: SAT3ToISInfo -> String
showsPrec :: Int -> SAT3ToISInfo -> ShowS
$cshowsPrec :: Int -> SAT3ToISInfo -> ShowS
Show)
-- Note that array <0.5.4.0 did not provided Read instance of UArray

instance Transformer SAT3ToISInfo where
  type Source SAT3ToISInfo = SAT.Model
  type Target SAT3ToISInfo = IntSet

instance ForwardTransformer SAT3ToISInfo where
  transformForward :: SAT3ToISInfo -> Source SAT3ToISInfo -> Target SAT3ToISInfo
transformForward (SAT3ToISInfo Int
_nv [[Int]]
clusters UArray Int Int
nodeToLit) Source SAT3ToISInfo
m = [Int] -> IntSet
IntSet.fromList ([Int] -> IntSet) -> [Int] -> IntSet
forall a b. (a -> b) -> a -> b
$ do
    [Int]
nodes <- [[Int]]
clusters
    let xs :: [Int]
xs = [Int
node | Int
node <- [Int]
nodes, Model -> Int -> Bool
forall m. IModel m => m -> Int -> Bool
SAT.evalLit Model
Source SAT3ToISInfo
m (UArray Int Int
nodeToLit UArray Int Int -> Int -> Int
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int
node)]
    if [Int] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
xs then
      String -> [Int]
forall a. HasCallStack => String -> a
error String
"not a model"
    else
      Int -> [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Int] -> Int
forall a. [a] -> a
head [Int]
xs)

instance BackwardTransformer SAT3ToISInfo where
  transformBackward :: SAT3ToISInfo -> Target SAT3ToISInfo -> Source SAT3ToISInfo
transformBackward (SAT3ToISInfo Int
nv [[Int]]
_clusters UArray Int Int
nodeToLit) Target SAT3ToISInfo
indep_set = (forall s. ST s (STUArray s Int Bool)) -> Model
forall i e. (forall s. ST s (STUArray s i e)) -> UArray i e
runSTUArray ((forall s. ST s (STUArray s Int Bool)) -> Model)
-> (forall s. ST s (STUArray s Int Bool)) -> Model
forall a b. (a -> b) -> a -> b
$ do
    STUArray s Int Bool
a <- (Int, Int) -> Bool -> ST s (STUArray s Int Bool)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> e -> m (a i e)
newArray (Int
1, Int
nv) Bool
False
    [Int] -> (Int -> ST s ()) -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntSet -> [Int]
IntSet.toList IntSet
lits) ((Int -> ST s ()) -> ST s ()) -> (Int -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \Int
lit -> 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
a (Int -> Int
SAT.litVar Int
lit) (Int -> Bool
SAT.litPolarity Int
lit)
    STUArray s Int Bool -> ST s (STUArray s Int Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return STUArray s Int Bool
a
    where
      lits :: IntSet
lits = (Int -> Int) -> IntSet -> IntSet
IntSet.map (UArray Int Int
nodeToLit UArray Int Int -> Int -> Int
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
!) IntSet
Target SAT3ToISInfo
indep_set

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

is2pb :: (Graph, Int) -> (PBFile.Formula, IS2SATInfo)
is2pb :: (Graph, Int) -> (Formula, IS2SATInfo)
is2pb (Graph
g, Int
k) = (forall s. ST s (Formula, IS2SATInfo)) -> (Formula, IS2SATInfo)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (Formula, IS2SATInfo)) -> (Formula, IS2SATInfo))
-> (forall s. ST s (Formula, IS2SATInfo)) -> (Formula, IS2SATInfo)
forall a b. (a -> b) -> a -> b
$ do
  let (Int
lb, Int
ub) = Graph -> (Int, Int)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds Graph
g
  PBStore (ST s)
db <- ST s (PBStore (ST s))
forall (m :: * -> *). PrimMonad m => m (PBStore m)
newPBStore
  [Int]
vs <- PBStore (ST s) -> Int -> ST s [Int]
forall (m :: * -> *) a. NewVar m a => a -> Int -> m [Int]
SAT.newVars PBStore (ST s)
db ((Int, Int) -> Int
forall a. Ix a => (a, a) -> Int
rangeSize (Graph -> (Int, Int)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds Graph
g))
  [(Int, Int, ())] -> ((Int, Int, ()) -> ST s ()) -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Graph -> [(Int, Int, ())]
forall a. EdgeLabeledGraph a -> [(Int, Int, a)]
graphToUnorderedEdges Graph
g) (((Int, Int, ()) -> ST s ()) -> ST s ())
-> ((Int, Int, ()) -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \(Int
node1, Int
node2, ()
_) -> do
    PBStore (ST s) -> [Int] -> ST s ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause PBStore (ST s)
db [- (Int
node1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
lb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1), - (Int
node2 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
lb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)]
  PBStore (ST s) -> PBLinSum -> Integer -> ST s ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtLeast PBStore (ST s)
db [(Integer
1,Int
v) | Int
v <- [Int]
vs] (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
k)
  Formula
formula <- PBStore (ST s) -> ST s Formula
forall (m :: * -> *). PrimMonad m => PBStore m -> m Formula
getPBFormula PBStore (ST s)
db
  (Formula, IS2SATInfo) -> ST s (Formula, IS2SATInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return
    ( Formula
formula
    , (Int, Int) -> IS2SATInfo
IS2SATInfo (Int
lb, Int
ub)
    )

mis2MaxSAT :: Graph -> (CNF.WCNF, IS2SATInfo)
mis2MaxSAT :: Graph -> (WCNF, IS2SATInfo)
mis2MaxSAT Graph
g = (forall s. ST s (WCNF, IS2SATInfo)) -> (WCNF, IS2SATInfo)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (WCNF, IS2SATInfo)) -> (WCNF, IS2SATInfo))
-> (forall s. ST s (WCNF, IS2SATInfo)) -> (WCNF, IS2SATInfo)
forall a b. (a -> b) -> a -> b
$ do
  let (Int
lb,Int
ub) = Graph -> (Int, Int)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds Graph
g
      n :: Int
n = Int
ub Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
lb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
  CNFStore (ST s)
db <- ST s (CNFStore (ST s))
forall (m :: * -> *). PrimMonad m => m (CNFStore m)
newCNFStore
  [Int]
vs <- CNFStore (ST s) -> Int -> ST s [Int]
forall (m :: * -> *) a. NewVar m a => a -> Int -> m [Int]
SAT.newVars CNFStore (ST s)
db Int
n
  [(Int, Int, ())] -> ((Int, Int, ()) -> ST s ()) -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Graph -> [(Int, Int, ())]
forall a. EdgeLabeledGraph a -> [(Int, Int, a)]
graphToUnorderedEdges Graph
g) (((Int, Int, ()) -> ST s ()) -> ST s ())
-> ((Int, Int, ()) -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \(Int
node1, Int
node2, ()
_) -> do
    CNFStore (ST s) -> [Int] -> ST s ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause CNFStore (ST s)
db [- (Int
node1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
lb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1), - (Int
node2 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
lb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)]
  CNF
cnf <- CNFStore (ST s) -> ST s CNF
forall (m :: * -> *). PrimMonad m => CNFStore m -> m CNF
getCNFFormula CNFStore (ST s)
db
  let top :: Integer
top = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
  (WCNF, IS2SATInfo) -> ST s (WCNF, IS2SATInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return
    ( WCNF :: Int -> Int -> Integer -> [WeightedClause] -> WCNF
CNF.WCNF
      { wcnfNumVars :: Int
CNF.wcnfNumVars = CNF -> Int
CNF.cnfNumVars CNF
cnf
      , wcnfNumClauses :: Int
CNF.wcnfNumClauses = CNF -> Int
CNF.cnfNumClauses CNF
cnf Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n
      , wcnfTopCost :: Integer
CNF.wcnfTopCost = Integer
top
      , wcnfClauses :: [WeightedClause]
CNF.wcnfClauses =
          [(Integer
top, PackedClause
clause) | PackedClause
clause <- CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf] [WeightedClause] -> [WeightedClause] -> [WeightedClause]
forall a. [a] -> [a] -> [a]
++
          [(Integer
1, [Int] -> PackedClause
SAT.packClause [Int
v]) | Int
v <- [Int]
vs]
      }
    , (Int, Int) -> IS2SATInfo
IS2SATInfo (Int
lb,Int
ub)
    )

newtype IS2SATInfo = IS2SATInfo (Int, Int)
  deriving (IS2SATInfo -> IS2SATInfo -> Bool
(IS2SATInfo -> IS2SATInfo -> Bool)
-> (IS2SATInfo -> IS2SATInfo -> Bool) -> Eq IS2SATInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IS2SATInfo -> IS2SATInfo -> Bool
$c/= :: IS2SATInfo -> IS2SATInfo -> Bool
== :: IS2SATInfo -> IS2SATInfo -> Bool
$c== :: IS2SATInfo -> IS2SATInfo -> Bool
Eq, Int -> IS2SATInfo -> ShowS
[IS2SATInfo] -> ShowS
IS2SATInfo -> String
(Int -> IS2SATInfo -> ShowS)
-> (IS2SATInfo -> String)
-> ([IS2SATInfo] -> ShowS)
-> Show IS2SATInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IS2SATInfo] -> ShowS
$cshowList :: [IS2SATInfo] -> ShowS
show :: IS2SATInfo -> String
$cshow :: IS2SATInfo -> String
showsPrec :: Int -> IS2SATInfo -> ShowS
$cshowsPrec :: Int -> IS2SATInfo -> ShowS
Show, ReadPrec [IS2SATInfo]
ReadPrec IS2SATInfo
Int -> ReadS IS2SATInfo
ReadS [IS2SATInfo]
(Int -> ReadS IS2SATInfo)
-> ReadS [IS2SATInfo]
-> ReadPrec IS2SATInfo
-> ReadPrec [IS2SATInfo]
-> Read IS2SATInfo
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [IS2SATInfo]
$creadListPrec :: ReadPrec [IS2SATInfo]
readPrec :: ReadPrec IS2SATInfo
$creadPrec :: ReadPrec IS2SATInfo
readList :: ReadS [IS2SATInfo]
$creadList :: ReadS [IS2SATInfo]
readsPrec :: Int -> ReadS IS2SATInfo
$creadsPrec :: Int -> ReadS IS2SATInfo
Read)

instance Transformer IS2SATInfo where
  type Source IS2SATInfo = IntSet
  type Target IS2SATInfo = SAT.Model

instance ForwardTransformer IS2SATInfo where
  transformForward :: IS2SATInfo -> Source IS2SATInfo -> Target IS2SATInfo
transformForward (IS2SATInfo (Int
lb, Int
ub)) Source IS2SATInfo
indep_set = (forall s. ST s (STUArray s Int Bool)) -> Model
forall i e. (forall s. ST s (STUArray s i e)) -> UArray i e
runSTUArray ((forall s. ST s (STUArray s Int Bool)) -> Model)
-> (forall s. ST s (STUArray s Int Bool)) -> Model
forall a b. (a -> b) -> a -> b
$ do
    let n :: Int
n = Int
ub Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
lb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
    STUArray s Int Bool
a <- (Int, Int) -> Bool -> ST s (STUArray s Int Bool)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> e -> m (a i e)
newArray (Int
1, Int
n) Bool
False
    [Int] -> (Int -> ST s ()) -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntSet -> [Int]
IntSet.toList IntSet
Source IS2SATInfo
indep_set) ((Int -> ST s ()) -> ST s ()) -> (Int -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \Int
node -> 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
a (Int
node Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
lb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Bool
True
    STUArray s Int Bool -> ST s (STUArray s Int Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return STUArray s Int Bool
a

instance BackwardTransformer IS2SATInfo where
  transformBackward :: IS2SATInfo -> Target IS2SATInfo -> Source IS2SATInfo
transformBackward (IS2SATInfo (Int
lb, Int
ub)) Target IS2SATInfo
m =
    [Int] -> IntSet
IntSet.fromList [Int
node | Int
node <- (Int, Int) -> [Int]
forall a. Ix a => (a, a) -> [a]
range (Int
lb, Int
ub), Model -> Int -> Bool
forall m. IModel m => m -> Int -> Bool
SAT.evalVar Model
Target IS2SATInfo
m (Int
node Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
lb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)]

instance ObjValueTransformer IS2SATInfo where
  type SourceObjValue IS2SATInfo = Int
  type TargetObjValue IS2SATInfo = Integer

instance ObjValueForwardTransformer IS2SATInfo where
  transformObjValueForward :: IS2SATInfo
-> SourceObjValue IS2SATInfo -> TargetObjValue IS2SATInfo
transformObjValueForward (IS2SATInfo (Int
lb, Int
ub)) SourceObjValue IS2SATInfo
k = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ (Int
ub Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
lb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
SourceObjValue IS2SATInfo
k

instance ObjValueBackwardTransformer IS2SATInfo where
  transformObjValueBackward :: IS2SATInfo
-> TargetObjValue IS2SATInfo -> SourceObjValue IS2SATInfo
transformObjValueBackward (IS2SATInfo (Int
lb, Int
ub)) TargetObjValue IS2SATInfo
k = (Int
ub Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
lb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
TargetObjValue IS2SATInfo
k

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

pairs :: [a] -> [(a,a)]
pairs :: [a] -> [(a, a)]
pairs [] = []
pairs (a
x:[a]
xs) = [(a
x,a
x2) | a
x2 <- [a]
xs] [(a, a)] -> [(a, a)] -> [(a, a)]
forall a. [a] -> [a] -> [a]
++ [a] -> [(a, a)]
forall a. [a] -> [(a, a)]
pairs [a]
xs

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