{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module ToySolver.SAT.Encoder.Cardinality
( Encoder
, Strategy (..)
, newEncoder
, newEncoderWithStrategy
, encodeAtLeast
, TotalizerDefinitions
, getTotalizerDefinitions
, evalTotalizerDefinitions
) where
import Control.Monad.Primitive
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Encoder.Cardinality.Internal.Naive
import ToySolver.SAT.Encoder.Cardinality.Internal.ParallelCounter
import ToySolver.SAT.Encoder.PB.Internal.BDD as BDD
import qualified ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer as Totalizer
data Encoder m = Encoder (Totalizer.Encoder m) Strategy
data Strategy
= Naive
| SequentialCounter
| ParallelCounter
| Totalizer
deriving (Int -> Strategy -> ShowS
[Strategy] -> ShowS
Strategy -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Strategy] -> ShowS
$cshowList :: [Strategy] -> ShowS
show :: Strategy -> String
$cshow :: Strategy -> String
showsPrec :: Int -> Strategy -> ShowS
$cshowsPrec :: Int -> Strategy -> ShowS
Show, Strategy -> Strategy -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Strategy -> Strategy -> Bool
$c/= :: Strategy -> Strategy -> Bool
== :: Strategy -> Strategy -> Bool
$c== :: Strategy -> Strategy -> Bool
Eq, Eq Strategy
Strategy -> Strategy -> Bool
Strategy -> Strategy -> Ordering
Strategy -> Strategy -> Strategy
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Strategy -> Strategy -> Strategy
$cmin :: Strategy -> Strategy -> Strategy
max :: Strategy -> Strategy -> Strategy
$cmax :: Strategy -> Strategy -> Strategy
>= :: Strategy -> Strategy -> Bool
$c>= :: Strategy -> Strategy -> Bool
> :: Strategy -> Strategy -> Bool
$c> :: Strategy -> Strategy -> Bool
<= :: Strategy -> Strategy -> Bool
$c<= :: Strategy -> Strategy -> Bool
< :: Strategy -> Strategy -> Bool
$c< :: Strategy -> Strategy -> Bool
compare :: Strategy -> Strategy -> Ordering
$ccompare :: Strategy -> Strategy -> Ordering
Ord, Int -> Strategy
Strategy -> Int
Strategy -> [Strategy]
Strategy -> Strategy
Strategy -> Strategy -> [Strategy]
Strategy -> Strategy -> Strategy -> [Strategy]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Strategy -> Strategy -> Strategy -> [Strategy]
$cenumFromThenTo :: Strategy -> Strategy -> Strategy -> [Strategy]
enumFromTo :: Strategy -> Strategy -> [Strategy]
$cenumFromTo :: Strategy -> Strategy -> [Strategy]
enumFromThen :: Strategy -> Strategy -> [Strategy]
$cenumFromThen :: Strategy -> Strategy -> [Strategy]
enumFrom :: Strategy -> [Strategy]
$cenumFrom :: Strategy -> [Strategy]
fromEnum :: Strategy -> Int
$cfromEnum :: Strategy -> Int
toEnum :: Int -> Strategy
$ctoEnum :: Int -> Strategy
pred :: Strategy -> Strategy
$cpred :: Strategy -> Strategy
succ :: Strategy -> Strategy
$csucc :: Strategy -> Strategy
Enum, Strategy
forall a. a -> a -> Bounded a
maxBound :: Strategy
$cmaxBound :: Strategy
minBound :: Strategy
$cminBound :: Strategy
Bounded)
newEncoder :: PrimMonad m => Tseitin.Encoder m -> m (Encoder m)
newEncoder :: forall (m :: * -> *). PrimMonad m => Encoder m -> m (Encoder m)
newEncoder Encoder m
tseitin = forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Strategy -> m (Encoder m)
newEncoderWithStrategy Encoder m
tseitin Strategy
ParallelCounter
newEncoderWithStrategy :: PrimMonad m => Tseitin.Encoder m -> Strategy -> m (Encoder m)
newEncoderWithStrategy :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Strategy -> m (Encoder m)
newEncoderWithStrategy Encoder m
tseitin Strategy
strategy = do
Encoder m
base <- forall (m :: * -> *). PrimMonad m => Encoder m -> m (Encoder m)
Totalizer.newEncoder Encoder m
tseitin
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Encoder m -> Strategy -> Encoder m
Encoder Encoder m
base Strategy
strategy
type TotalizerDefinitions = Totalizer.Definitions
getTotalizerDefinitions :: PrimMonad m => Encoder m -> m TotalizerDefinitions
getTotalizerDefinitions :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> m TotalizerDefinitions
getTotalizerDefinitions (Encoder Encoder m
base Strategy
_) = forall (m :: * -> *).
PrimMonad m =>
Encoder m -> m TotalizerDefinitions
Totalizer.getDefinitions Encoder m
base
evalTotalizerDefinitions :: SAT.IModel m => m -> TotalizerDefinitions -> [(SAT.Var, Bool)]
evalTotalizerDefinitions :: forall m. IModel m => m -> TotalizerDefinitions -> [(Int, Bool)]
evalTotalizerDefinitions m
m TotalizerDefinitions
defs = forall m. IModel m => m -> TotalizerDefinitions -> [(Int, Bool)]
Totalizer.evalDefinitions m
m TotalizerDefinitions
defs
instance Monad m => SAT.NewVar m (Encoder m) where
newVar :: Encoder m -> m Int
newVar (Encoder Encoder m
base Strategy
_) = forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar Encoder m
base
newVars :: Encoder m -> Int -> m [Int]
newVars (Encoder Encoder m
base Strategy
_) = forall (m :: * -> *) a. NewVar m a => a -> Int -> m [Int]
SAT.newVars Encoder m
base
newVars_ :: Encoder m -> Int -> m ()
newVars_ (Encoder Encoder m
base Strategy
_) = forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ Encoder m
base
instance Monad m => SAT.AddClause m (Encoder m) where
addClause :: Encoder m -> [Int] -> m ()
addClause (Encoder Encoder m
base Strategy
_) = forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Encoder m
base
instance PrimMonad m => SAT.AddCardinality m (Encoder m) where
addAtLeast :: Encoder m -> [Int] -> Int -> m ()
addAtLeast (Encoder base :: Encoder m
base@(Totalizer.Encoder Encoder m
tseitin MutVar (PrimState m) (Map LitSet (Vector Int))
_) Strategy
strategy) [Int]
lhs Int
rhs
| Int
rhs forall a. Ord a => a -> a -> Bool
<= Int
0 = forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise =
case Strategy
strategy of
Strategy
Naive -> forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m ()
addAtLeastNaive Encoder m
tseitin ([Int]
lhs,Int
rhs)
Strategy
ParallelCounter -> forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m ()
addAtLeastParallelCounter Encoder m
tseitin ([Int]
lhs,Int
rhs)
Strategy
SequentialCounter -> forall (m :: * -> *).
PrimMonad m =>
Encoder m -> PBLinAtLeast -> m ()
BDD.addPBLinAtLeastBDD Encoder m
tseitin ([(Integer
1,Int
l) | Int
l <- [Int]
lhs], forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
rhs)
Strategy
Totalizer -> forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m ()
Totalizer.addAtLeast Encoder m
base ([Int]
lhs,Int
rhs)
encodeAtLeast :: PrimMonad m => Encoder m -> SAT.AtLeast -> m SAT.Lit
encodeAtLeast :: forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m Int
encodeAtLeast (Encoder base :: Encoder m
base@(Totalizer.Encoder Encoder m
tseitin MutVar (PrimState m) (Map LitSet (Vector Int))
_) Strategy
strategy) =
case Strategy
strategy of
Strategy
Naive -> forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m Int
encodeAtLeastNaive Encoder m
tseitin
Strategy
ParallelCounter -> forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m Int
encodeAtLeastParallelCounter Encoder m
tseitin
Strategy
SequentialCounter -> \([Int]
lhs,Int
rhs) -> forall (m :: * -> *).
PrimMonad m =>
Encoder m -> PBLinAtLeast -> m Int
BDD.encodePBLinAtLeastBDD Encoder m
tseitin ([(Integer
1,Int
l) | Int
l <- [Int]
lhs], forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
rhs)
Strategy
Totalizer -> forall (m :: * -> *). PrimMonad m => Encoder m -> AtLeast -> m Int
Totalizer.encodeAtLeast Encoder m
base