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

-- TODO: consider polarity
encodeAtLeastNaive :: PrimMonad m => Tseitin.Encoder m -> SAT.AtLeast -> m SAT.Lit
encodeAtLeastNaive :: Encoder m -> AtLeast -> m Lit
encodeAtLeastNaive Encoder m
enc ([Lit]
lhs,Lit
rhs) = do
  let n :: Lit
n = [Lit] -> Lit
forall (t :: * -> *) a. Foldable t => t a -> Lit
length [Lit]
lhs
  if Lit
n Lit -> Lit -> Bool
forall a. Ord a => a -> a -> Bool
< Lit
rhs then do
    Encoder m -> [Lit] -> m Lit
forall (m :: * -> *). PrimMonad m => Encoder m -> [Lit] -> m Lit
Tseitin.encodeDisj Encoder m
enc []
  else do
    [Lit]
ls <- ([Lit] -> m Lit) -> [[Lit]] -> m [Lit]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Encoder m -> [Lit] -> m Lit
forall (m :: * -> *). PrimMonad m => Encoder m -> [Lit] -> m Lit
Tseitin.encodeDisj Encoder m
enc) (Lit -> [Lit] -> [[Lit]]
forall a. Lit -> [a] -> [[a]]
comb (Lit
n Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
- Lit
rhs Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
+ Lit
1) [Lit]
lhs)
    Encoder m -> [Lit] -> m Lit
forall (m :: * -> *). PrimMonad m => Encoder m -> [Lit] -> m Lit
Tseitin.encodeConj Encoder m
enc [Lit]
ls

comb :: Int -> [a] -> [[a]]
comb :: Lit -> [a] -> [[a]]
comb Lit
0 [a]
_ = [[]]
comb Lit
_ [] = []
comb Lit
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]
:) (Lit -> [a] -> [[a]]
forall a. Lit -> [a] -> [[a]]
comb (Lit
nLit -> Lit -> Lit
forall a. Num a => a -> a -> a
-Lit
1) [a]
xs) [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ Lit -> [a] -> [[a]]
forall a. Lit -> [a] -> [[a]]
comb Lit
n [a]
xs