{-# 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
  , encodeAtLeastWithPolarityNaive
  ) where

import Control.Monad.Primitive
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Encoder.Tseitin (Polarity ())

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 = [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
lhs
  if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
rhs then do
    Encoder m -> [Int] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Encoder m
enc []
  else do
    ([Int] -> m ()) -> [[Int]] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Encoder m -> [Int] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Encoder m
enc) (Int -> [Int] -> [[Int]]
forall a. Int -> [a] -> [[a]]
comb (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
rhs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Int]
lhs)

encodeAtLeastWithPolarityNaive :: PrimMonad m => Tseitin.Encoder m -> Polarity -> SAT.AtLeast -> m SAT.Lit
encodeAtLeastWithPolarityNaive :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> AtLeast -> m Int
encodeAtLeastWithPolarityNaive Encoder m
enc Polarity
polarity ([Int]
lhs,Int
rhs) = do
  let n :: Int
n = [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
lhs
  if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
rhs then do
    Encoder m -> Polarity -> [Int] -> m Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Int] -> m Int
Tseitin.encodeDisjWithPolarity Encoder m
enc Polarity
polarity []
  else do
    [Int]
ls <- ([Int] -> m Int) -> [[Int]] -> m [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Encoder m -> Polarity -> [Int] -> m Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Int] -> m Int
Tseitin.encodeDisjWithPolarity Encoder m
enc Polarity
polarity) (Int -> [Int] -> [[Int]]
forall a. Int -> [a] -> [[a]]
comb (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
rhs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Int]
lhs)
    Encoder m -> Polarity -> [Int] -> m Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Int] -> m Int
Tseitin.encodeConjWithPolarity Encoder m
enc Polarity
polarity [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) = ([a] -> [a]) -> [[a]] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:) (Int -> [a] -> [[a]]
forall a. Int -> [a] -> [[a]]
comb (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [a]
xs) [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ Int -> [a] -> [[a]]
forall a. Int -> [a] -> [[a]]
comb Int
n [a]
xs