{-# 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 (..)
  , newEncoder
  , newEncoderWithStrategy
  , encodePBLinAtLeast
  , encodePBLinAtLeastWithPolarity

  -- * Configulation
  , Strategy (..)
  , showStrategy
  , parseStrategy

  -- * Polarity
  , Polarity (..)
  , negatePolarity
  , polarityPos
  , polarityNeg
  , polarityBoth
  , polarityNone
  ) where

import Control.Monad.Primitive
import Data.Char
import Data.Default.Class
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Cardinality as Card
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Encoder.Tseitin (Polarity (..), negatePolarity, polarityPos, polarityNeg, polarityBoth, polarityNone)
import ToySolver.SAT.Encoder.PB.Internal.Adder (addPBLinAtLeastAdder, encodePBLinAtLeastWithPolarityAdder)
import ToySolver.SAT.Encoder.PB.Internal.BCCNF (addPBLinAtLeastBCCNF, encodePBLinAtLeastWithPolarityBCCNF)
import ToySolver.SAT.Encoder.PB.Internal.BDD (addPBLinAtLeastBDD, encodePBLinAtLeastWithPolarityBDD)
import ToySolver.SAT.Encoder.PB.Internal.Sorter (addPBLinAtLeastSorter, encodePBLinAtLeastSorter)

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

data Strategy
  = BDD
  | Adder
  | Sorter
  | BCCNF
  | Hybrid -- not implemented yet
  deriving (Int -> Strategy -> ShowS
[Strategy] -> ShowS
Strategy -> String
(Int -> Strategy -> ShowS)
-> (Strategy -> String) -> ([Strategy] -> ShowS) -> Show Strategy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Strategy -> ShowS
showsPrec :: Int -> Strategy -> ShowS
$cshow :: Strategy -> String
show :: Strategy -> String
$cshowList :: [Strategy] -> ShowS
showList :: [Strategy] -> ShowS
Show, Strategy -> Strategy -> Bool
(Strategy -> Strategy -> Bool)
-> (Strategy -> Strategy -> Bool) -> Eq Strategy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Strategy -> Strategy -> Bool
== :: Strategy -> Strategy -> Bool
$c/= :: Strategy -> Strategy -> Bool
/= :: Strategy -> Strategy -> Bool
Eq, Eq Strategy
Eq Strategy =>
(Strategy -> Strategy -> Ordering)
-> (Strategy -> Strategy -> Bool)
-> (Strategy -> Strategy -> Bool)
-> (Strategy -> Strategy -> Bool)
-> (Strategy -> Strategy -> Bool)
-> (Strategy -> Strategy -> Strategy)
-> (Strategy -> Strategy -> Strategy)
-> Ord 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
$ccompare :: Strategy -> Strategy -> Ordering
compare :: Strategy -> Strategy -> Ordering
$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
>= :: Strategy -> Strategy -> Bool
$cmax :: Strategy -> Strategy -> Strategy
max :: Strategy -> Strategy -> Strategy
$cmin :: Strategy -> Strategy -> Strategy
min :: Strategy -> Strategy -> Strategy
Ord, Int -> Strategy
Strategy -> Int
Strategy -> [Strategy]
Strategy -> Strategy
Strategy -> Strategy -> [Strategy]
Strategy -> Strategy -> Strategy -> [Strategy]
(Strategy -> Strategy)
-> (Strategy -> Strategy)
-> (Int -> Strategy)
-> (Strategy -> Int)
-> (Strategy -> [Strategy])
-> (Strategy -> Strategy -> [Strategy])
-> (Strategy -> Strategy -> [Strategy])
-> (Strategy -> Strategy -> Strategy -> [Strategy])
-> Enum 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
$csucc :: Strategy -> Strategy
succ :: Strategy -> Strategy
$cpred :: Strategy -> Strategy
pred :: Strategy -> Strategy
$ctoEnum :: Int -> Strategy
toEnum :: Int -> Strategy
$cfromEnum :: Strategy -> Int
fromEnum :: Strategy -> Int
$cenumFrom :: Strategy -> [Strategy]
enumFrom :: Strategy -> [Strategy]
$cenumFromThen :: Strategy -> Strategy -> [Strategy]
enumFromThen :: Strategy -> Strategy -> [Strategy]
$cenumFromTo :: Strategy -> Strategy -> [Strategy]
enumFromTo :: Strategy -> Strategy -> [Strategy]
$cenumFromThenTo :: Strategy -> Strategy -> Strategy -> [Strategy]
enumFromThenTo :: Strategy -> Strategy -> Strategy -> [Strategy]
Enum, Strategy
Strategy -> Strategy -> Bounded Strategy
forall a. a -> a -> Bounded a
$cminBound :: Strategy
minBound :: Strategy
$cmaxBound :: Strategy
maxBound :: Strategy
Bounded)

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

showStrategy :: Strategy -> String
showStrategy :: Strategy -> String
showStrategy Strategy
BDD = String
"bdd"
showStrategy Strategy
Adder = String
"adder"
showStrategy Strategy
Sorter = String
"sorter"
showStrategy Strategy
BCCNF = String
"bccnf"
showStrategy Strategy
Hybrid = String
"hybrid"

parseStrategy :: String -> Maybe Strategy
parseStrategy :: String -> Maybe Strategy
parseStrategy String
s =
  case (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
s of
    String
"bdd"    -> Strategy -> Maybe Strategy
forall a. a -> Maybe a
Just Strategy
BDD
    String
"adder"  -> Strategy -> Maybe Strategy
forall a. a -> Maybe a
Just Strategy
Adder
    String
"sorter" -> Strategy -> Maybe Strategy
forall a. a -> Maybe a
Just Strategy
Sorter
    String
"bccnf"  -> Strategy -> Maybe Strategy
forall a. a -> Maybe a
Just Strategy
BCCNF
    String
"hybrid" -> Strategy -> Maybe Strategy
forall a. a -> Maybe a
Just Strategy
Hybrid
    String
_ -> Maybe Strategy
forall a. Maybe a
Nothing

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

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
card <- Encoder m -> Strategy -> m (Encoder m)
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Strategy -> m (Encoder m)
Card.newEncoderWithStrategy Encoder m
tseitin Strategy
Card.SequentialCounter
  Encoder m -> m (Encoder m)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Encoder m -> Strategy -> Encoder m
forall (m :: * -> *). Encoder m -> Strategy -> Encoder m
Encoder Encoder m
card Strategy
strategy)

instance Monad m => SAT.NewVar m (Encoder m) where
  newVar :: Encoder m -> m Int
newVar   (Encoder Encoder m
a Strategy
_) = Encoder m -> m Int
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
_) = Encoder m -> Int -> m [Int]
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
_) = Encoder m -> Int -> m ()
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
_) = Encoder m -> [Int] -> m ()
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 = Encoder m -> PBLinSum -> Integer -> m ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtLeast Encoder m
enc [(Integer
1, Int
l) | Int
l <- [Int]
lhs] (Int -> Integer
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' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1 Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Integer
cInteger -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
==Integer
1 | (Integer
c,Int
_) <- PBLinSum
lhs'] then
      Encoder m -> [Int] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Encoder m
enc [Int
l | (Integer
_,Int
l) <- PBLinSum
lhs']
    else do
      Encoder m -> (PBLinSum, Integer) -> m ()
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 = Encoder m -> Polarity -> (PBLinSum, Integer) -> m Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> (PBLinSum, Integer) -> m Int
encodePBLinAtLeastWithPolarity Encoder m
enc Polarity
polarityBoth (PBLinSum, Integer)
constr

encodePBLinAtLeastWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> SAT.PBLinAtLeast -> m SAT.Lit
encodePBLinAtLeastWithPolarity :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> (PBLinSum, Integer) -> m Int
encodePBLinAtLeastWithPolarity Encoder m
enc Polarity
polarity (PBLinSum, Integer)
constr =
  Encoder m -> Polarity -> (PBLinSum, Integer) -> m Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> (PBLinSum, Integer) -> m Int
encodePBLinAtLeastWithPolarity' Encoder m
enc Polarity
polarity ((PBLinSum, Integer) -> m Int) -> (PBLinSum, Integer) -> m Int
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
card Strategy
strategy) = do
  let tseitin :: Encoder m
tseitin = Encoder m -> Encoder m
forall (m :: * -> *). Encoder m -> Encoder m
Card.getTseitinEncoder Encoder m
card
  case Strategy
strategy of
    Strategy
Adder -> Encoder m -> (PBLinSum, Integer) -> m ()
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m ()
addPBLinAtLeastAdder Encoder m
tseitin
    Strategy
Sorter -> Encoder m -> (PBLinSum, Integer) -> m ()
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m ()
addPBLinAtLeastSorter Encoder m
tseitin
    Strategy
BCCNF -> Encoder m -> (PBLinSum, Integer) -> m ()
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m ()
addPBLinAtLeastBCCNF Encoder m
card
    Strategy
_ -> Encoder m -> (PBLinSum, Integer) -> m ()
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m ()
addPBLinAtLeastBDD Encoder m
tseitin

encodePBLinAtLeastWithPolarity' :: PrimMonad m => Encoder m -> Polarity -> SAT.PBLinAtLeast -> m SAT.Lit
encodePBLinAtLeastWithPolarity' :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> (PBLinSum, Integer) -> m Int
encodePBLinAtLeastWithPolarity' (Encoder Encoder m
card Strategy
strategy) Polarity
polarity (PBLinSum, Integer)
constr = do
  let tseitin :: Encoder m
tseitin = Encoder m -> Encoder m
forall (m :: * -> *). Encoder m -> Encoder m
Card.getTseitinEncoder Encoder m
card
  case Strategy
strategy of
    Strategy
Adder -> Encoder m -> Polarity -> (PBLinSum, Integer) -> m Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> (PBLinSum, Integer) -> m Int
encodePBLinAtLeastWithPolarityAdder Encoder m
tseitin Polarity
polarity (PBLinSum, Integer)
constr
    Strategy
Sorter -> Encoder m -> (PBLinSum, Integer) -> m Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m Int
encodePBLinAtLeastSorter Encoder m
tseitin (PBLinSum, Integer)
constr
    Strategy
BCCNF -> Encoder m -> Polarity -> (PBLinSum, Integer) -> m Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> (PBLinSum, Integer) -> m Int
encodePBLinAtLeastWithPolarityBCCNF Encoder m
card Polarity
polarity (PBLinSum, Integer)
constr
    Strategy
_ -> Encoder m -> Polarity -> (PBLinSum, Integer) -> m Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> (PBLinSum, Integer) -> m Int
encodePBLinAtLeastWithPolarityBDD Encoder m
tseitin Polarity
polarity (PBLinSum, Integer)
constr

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