{-# OPTIONS_GHC -Wall #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Encoder.Cardinality.Internal.Naive
-- Copyright   :  (c) Masahiro Sakai 2019
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  portable
--
-----------------------------------------------------------------------------
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)

-- TODO: consider polarity
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