module Satchmo.Counting.Direct
( atleast
, atmost
, exactly
, assert_implies_atmost
, assert_implies_exactly
)
where
import Satchmo.Boolean ( Boolean, MonadSAT )
import qualified Satchmo.Boolean as B
import Control.Monad ( forM, forM_ )
select :: Int -> [a] -> [[a]]
select 0 xs = [[]]
select k [] = []
select k (x:xs) =
select k xs ++ (map (x:) $ select (k1) xs)
atleast :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
atleast k xs = B.or =<< forM (select k xs) B.and
atmost :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
atmost k xs = atleast (length xs k) $ map B.not xs
exactly :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
exactly k xs = do
this <- atleast k xs
that <- atmost k xs
this B.&& that
assert_implies_atmost ys k xs | k >= 0 =
forM_ (select (k+1) xs) $ \ sub -> do
B.assert $ map B.not ys ++ map B.not sub
assert_implies_atmost ys k _ =
B.assert $ map B.not ys
assert_implies_atleast ys k xs =
assert_implies_atmost ys (length xs k) (map B.not xs)
assert_implies_exactly ys k xs = do
assert_implies_atmost ys k xs
assert_implies_atleast ys k xs
assert_atmost_implies xs k ys =
assert_implies_atleast (map B.not ys) (k+1) xs
assert_atleast_implies xs k ys =
assert_implies_atmost (map B.not ys) (k+1) xs