{-# OPTIONS_GHC -Wall #-}
module ToySolver.SAT.Encoder.Cardinality.Internal.Naive
( addAtLeastNaive
, encodeAtLeastNaive
) where
import Control.Monad.Primitive
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
addAtLeastNaive :: PrimMonad m => Tseitin.Encoder m -> SAT.AtLeast -> m ()
addAtLeastNaive :: forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m ()
addAtLeastNaive Encoder m
enc ([Int]
lhs,Int
rhs) = do
let n :: Int
n = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
lhs
if Int
n forall a. Ord a => a -> a -> Bool
< Int
rhs then do
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Encoder m
enc []
else do
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Encoder m
enc) (forall a. Int -> [a] -> [[a]]
comb (Int
n forall a. Num a => a -> a -> a
- Int
rhs forall a. Num a => a -> a -> a
+ Int
1) [Int]
lhs)
encodeAtLeastNaive :: PrimMonad m => Tseitin.Encoder m -> SAT.AtLeast -> m SAT.Lit
encodeAtLeastNaive :: forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m Int
encodeAtLeastNaive Encoder m
enc ([Int]
lhs,Int
rhs) = do
let n :: Int
n = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
lhs
if Int
n forall a. Ord a => a -> a -> Bool
< Int
rhs then do
forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeDisj Encoder m
enc []
else do
[Int]
ls <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeDisj Encoder m
enc) (forall a. Int -> [a] -> [[a]]
comb (Int
n forall a. Num a => a -> a -> a
- Int
rhs forall a. Num a => a -> a -> a
+ Int
1) [Int]
lhs)
forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeConj Encoder m
enc [Int]
ls
comb :: Int -> [a] -> [[a]]
comb :: forall a. Int -> [a] -> [[a]]
comb Int
0 [a]
_ = [[]]
comb Int
_ [] = []
comb Int
n (a
x:[a]
xs) = forall a b. (a -> b) -> [a] -> [b]
map (a
xforall a. a -> [a] -> [a]
:) (forall a. Int -> [a] -> [[a]]
comb (Int
nforall a. Num a => a -> a -> a
-Int
1) [a]
xs) forall a. [a] -> [a] -> [a]
++ forall a. Int -> [a] -> [[a]]
comb Int
n [a]
xs