{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Encoder.PB
-- Copyright   :  (c) Masahiro Sakai 2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- References:
--
-- * [ES06] N. Eén and N. Sörensson. Translating Pseudo-Boolean
--   Constraints into SAT. JSAT 2:1–26, 2006.
--
-----------------------------------------------------------------------------
module ToySolver.SAT.Encoder.PB
  ( Encoder
  , Strategy (..)
  , newEncoder
  , newEncoderWithStrategy
  , encodePBLinAtLeast
  ) where

import Control.Monad.Primitive
import Data.Default.Class
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Encoder.PB.Internal.Adder (addPBLinAtLeastAdder, encodePBLinAtLeastAdder)
import ToySolver.SAT.Encoder.PB.Internal.BDD (addPBLinAtLeastBDD, encodePBLinAtLeastBDD)
import ToySolver.SAT.Encoder.PB.Internal.Sorter (addPBLinAtLeastSorter, encodePBLinAtLeastSorter)

data Encoder m = Encoder (Tseitin.Encoder m) Strategy

data Strategy
  = BDD
  | Adder
  | Sorter
  | Hybrid -- not implemented yet
  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)

instance Default Strategy where
  def :: Strategy
def = Strategy
Hybrid

newEncoder :: Monad m => Tseitin.Encoder m -> m (Encoder m)
newEncoder :: forall (m :: * -> *). Monad m => Encoder m -> m (Encoder m)
newEncoder Encoder m
tseitin = forall (m :: * -> *).
Monad m =>
Encoder m -> Strategy -> m (Encoder m)
newEncoderWithStrategy Encoder m
tseitin Strategy
Hybrid

newEncoderWithStrategy :: Monad m => Tseitin.Encoder m -> Strategy -> m (Encoder m)
newEncoderWithStrategy :: forall (m :: * -> *).
Monad m =>
Encoder m -> Strategy -> m (Encoder m)
newEncoderWithStrategy Encoder m
tseitin Strategy
strategy = forall (m :: * -> *) a. Monad m => a -> m a
return (forall (m :: * -> *). Encoder m -> Strategy -> Encoder m
Encoder Encoder m
tseitin Strategy
strategy)

instance Monad m => SAT.NewVar m (Encoder m) where
  newVar :: Encoder m -> m Int
newVar   (Encoder Encoder m
a Strategy
_) = forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar Encoder m
a
  newVars :: Encoder m -> Int -> m [Int]
newVars  (Encoder Encoder m
a Strategy
_) = forall (m :: * -> *) a. NewVar m a => a -> Int -> m [Int]
SAT.newVars Encoder m
a
  newVars_ :: Encoder m -> Int -> m ()
newVars_ (Encoder Encoder m
a Strategy
_) = forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ Encoder m
a

instance Monad m => SAT.AddClause m (Encoder m) where
  addClause :: Encoder m -> [Int] -> m ()
addClause (Encoder Encoder m
a Strategy
_) = forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Encoder m
a

instance PrimMonad m => SAT.AddCardinality m (Encoder m) where
  addAtLeast :: Encoder m -> [Int] -> Int -> m ()
addAtLeast Encoder m
enc [Int]
lhs Int
rhs = forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtLeast Encoder m
enc [(Integer
1, Int
l) | Int
l <- [Int]
lhs] (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
rhs)

instance PrimMonad m => SAT.AddPBLin m (Encoder m) where
  addPBAtLeast :: Encoder m -> PBLinSum -> Integer -> m ()
addPBAtLeast Encoder m
enc PBLinSum
lhs Integer
rhs = do
    let (PBLinSum
lhs',Integer
rhs') = (PBLinSum, Integer) -> (PBLinSum, Integer)
SAT.normalizePBLinAtLeast (PBLinSum
lhs,Integer
rhs)
    if Integer
rhs' forall a. Eq a => a -> a -> Bool
== Integer
1 Bool -> Bool -> Bool
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Integer
cforall a. Eq a => a -> a -> Bool
==Integer
1 | (Integer
c,Int
_) <- PBLinSum
lhs'] then
      forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Encoder m
enc [Int
l | (Integer
_,Int
l) <- PBLinSum
lhs']
    else do
      forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m ()
addPBLinAtLeast' Encoder m
enc (PBLinSum
lhs',Integer
rhs')

encodePBLinAtLeast :: forall m. PrimMonad m => Encoder m -> SAT.PBLinAtLeast -> m SAT.Lit
encodePBLinAtLeast :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m Int
encodePBLinAtLeast Encoder m
enc (PBLinSum, Integer)
constr =
  forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m Int
encodePBLinAtLeast' Encoder m
enc forall a b. (a -> b) -> a -> b
$ (PBLinSum, Integer) -> (PBLinSum, Integer)
SAT.normalizePBLinAtLeast (PBLinSum, Integer)
constr

-- -----------------------------------------------------------------------

addPBLinAtLeast' :: PrimMonad m => Encoder m -> SAT.PBLinAtLeast -> m ()
addPBLinAtLeast' :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m ()
addPBLinAtLeast' (Encoder Encoder m
tseitin Strategy
strategy) =
  case Strategy
strategy of
    Strategy
Adder -> forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m ()
addPBLinAtLeastAdder Encoder m
tseitin
    Strategy
Sorter -> forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m ()
addPBLinAtLeastSorter Encoder m
tseitin
    Strategy
_ -> forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m ()
addPBLinAtLeastBDD Encoder m
tseitin

encodePBLinAtLeast' :: PrimMonad m => Encoder m -> SAT.PBLinAtLeast -> m SAT.Lit
encodePBLinAtLeast' :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m Int
encodePBLinAtLeast' (Encoder Encoder m
tseitin Strategy
strategy) =
  case Strategy
strategy of
    Strategy
Adder -> forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m Int
encodePBLinAtLeastAdder Encoder m
tseitin
    Strategy
Sorter -> forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m Int
encodePBLinAtLeastSorter Encoder m
tseitin
    Strategy
_ -> forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m Int
encodePBLinAtLeastBDD Encoder m
tseitin

-- -----------------------------------------------------------------------