{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Encoder.PB.Internal.Sorter
-- 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.Internal.Sorter
  ( Base
  , UDigit
  , UNumber
  , isRepresentable
  , encode
  , decode

  , Cost
  , optimizeBase

  , genSorterCircuit
  , sortVector

  , addPBLinAtLeastSorter
  , encodePBLinAtLeastSorter
  ) where

import Control.Monad.Primitive
import Control.Monad.State
import Control.Monad.Writer
import Data.List
import Data.Maybe
import Data.Ord
import Data.Vector (Vector, (!))
import qualified Data.Vector as V
import qualified Data.Vector.Mutable as MV
import ToySolver.Data.BoolExpr
import ToySolver.Data.Boolean
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin

-- ------------------------------------------------------------------------
-- Circuit-like implementation of Batcher's odd-even mergesort

genSorterCircuit :: Int -> [(Int,Int)]
genSorterCircuit :: Int -> [(Int, Int)]
genSorterCircuit Int
len = Writer ([(Int, Int)] -> [(Int, Int)]) ()
-> [(Int, Int)] -> [(Int, Int)]
forall w a. Writer w a -> w
execWriter (Vector Int -> Writer ([(Int, Int)] -> [(Int, Int)]) ()
forall (m :: * -> *) b.
MonadWriter ([(b, b)] -> [(b, b)]) m =>
Vector b -> m ()
mergeSort (Int -> (Int -> Int) -> Int -> Vector Int
forall a. Int -> (a -> a) -> a -> Vector a
V.iterateN Int
len (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int
0)) []
  where
    genCompareAndSwap :: a -> b -> m ()
genCompareAndSwap a
i b
j = ([(a, b)] -> [(a, b)]) -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell ((a
i,b
j) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:)

    mergeSort :: Vector b -> m ()
mergeSort Vector b
is
      | Vector b -> Int
forall a. Vector a -> Int
V.length Vector b
is Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      | Vector b -> Int
forall a. Vector a -> Int
V.length Vector b
is Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 = b -> b -> m ()
forall a b (m :: * -> *).
MonadWriter ([(a, b)] -> [(a, b)]) m =>
a -> b -> m ()
genCompareAndSwap (Vector b
isVector b -> Int -> b
forall a. Vector a -> Int -> a
!Int
0) (Vector b
isVector b -> Int -> b
forall a. Vector a -> Int -> a
!Int
1)
      | Bool
otherwise =
          case Vector b -> (Vector b, Vector b)
forall a. Vector a -> (Vector a, Vector a)
halve Vector b
is of
            (Vector b
is1,Vector b
is2) -> do
              Vector b -> m ()
mergeSort Vector b
is1
              Vector b -> m ()
mergeSort Vector b
is2
              Vector b -> m ()
forall (m :: * -> *) b.
MonadWriter ([(b, b)] -> [(b, b)]) m =>
Vector b -> m ()
oddEvenMerge Vector b
is

    oddEvenMerge :: Vector b -> m ()
oddEvenMerge Vector b
is
      | Vector b -> Int
forall a. Vector a -> Int
V.length Vector b
is Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      | Vector b -> Int
forall a. Vector a -> Int
V.length Vector b
is Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 = b -> b -> m ()
forall a b (m :: * -> *).
MonadWriter ([(a, b)] -> [(a, b)]) m =>
a -> b -> m ()
genCompareAndSwap (Vector b
isVector b -> Int -> b
forall a. Vector a -> Int -> a
!Int
0) (Vector b
isVector b -> Int -> b
forall a. Vector a -> Int -> a
!Int
1)
      | Bool
otherwise =
          case Vector b -> (Vector b, Vector b)
forall a. Vector a -> (Vector a, Vector a)
splitOddEven Vector b
is of
            (Vector b
os,Vector b
es) -> do
              Vector b -> m ()
oddEvenMerge Vector b
os
              Vector b -> m ()
oddEvenMerge Vector b
es
              [Int] -> (Int -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int
2,Int
3 .. Vector b -> Int
forall a. Vector a -> Int
V.length Vector b
isInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1] ((Int -> m ()) -> m ()) -> (Int -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \Int
i -> do
                b -> b -> m ()
forall a b (m :: * -> *).
MonadWriter ([(a, b)] -> [(a, b)]) m =>
a -> b -> m ()
genCompareAndSwap (Vector b
isVector b -> Int -> b
forall a. Vector a -> Int -> a
!(Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) (Vector b
isVector b -> Int -> b
forall a. Vector a -> Int -> a
!Int
i)

halve :: Vector a -> (Vector a, Vector a)
halve :: Vector a -> (Vector a, Vector a)
halve Vector a
v
  | Vector a -> Int
forall a. Vector a -> Int
V.length Vector a
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 = (Vector a
v, Vector a
forall a. Vector a
V.empty)
  | Bool
otherwise = (Int -> Int -> Vector a -> Vector a
forall a. Int -> Int -> Vector a -> Vector a
V.slice Int
0 Int
len1 Vector a
v, Int -> Int -> Vector a -> Vector a
forall a. Int -> Int -> Vector a -> Vector a
V.slice Int
len1 Int
len2 Vector a
v)
      where
        n :: Int
n = [Int] -> Int
forall a. [a] -> a
head ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Vector a -> Int
forall a. Vector a -> Int
V.length Vector a
v) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ (Int -> Int) -> Int -> [Int]
forall a. (a -> a) -> a -> [a]
iterate (Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
2) Int
1
        len1 :: Int
len1 = Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
        len2 :: Int
len2 = Vector a -> Int
forall a. Vector a -> Int
V.length Vector a
v Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
len1

splitOddEven :: Vector a -> (Vector a, Vector a)
splitOddEven :: Vector a -> (Vector a, Vector a)
splitOddEven Vector a
v = (Int -> (Int -> a) -> Vector a
forall a. Int -> (Int -> a) -> Vector a
V.generate Int
len1 (\Int
i -> Vector a
v Vector a -> Int -> a
forall a. Vector a -> Int -> a
V.! (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)), Int -> (Int -> a) -> Vector a
forall a. Int -> (Int -> a) -> Vector a
V.generate Int
len2 (\Int
i -> Vector a
v Vector a -> Int -> a
forall a. Vector a -> Int -> a
V.! (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
2)))
  where
    len1 :: Int
len1 = Vector a -> Int
forall a. Vector a -> Int
V.length Vector a
v Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
    len2 :: Int
len2 = (Vector a -> Int
forall a. Vector a -> Int
V.length Vector a
v Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2

sortVector :: (Ord a) => Vector a -> Vector a
sortVector :: Vector a -> Vector a
sortVector Vector a
v = (forall s. ST s (MVector s a)) -> Vector a
forall a. (forall s. ST s (MVector s a)) -> Vector a
V.create ((forall s. ST s (MVector s a)) -> Vector a)
-> (forall s. ST s (MVector s a)) -> Vector a
forall a b. (a -> b) -> a -> b
$ do
  MVector s a
m <- Vector a -> ST s (MVector (PrimState (ST s)) a)
forall (m :: * -> *) a.
PrimMonad m =>
Vector a -> m (MVector (PrimState m) a)
V.thaw Vector a
v
  [(Int, Int)] -> ((Int, Int) -> ST s ()) -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Int -> [(Int, Int)]
genSorterCircuit (Vector a -> Int
forall a. Vector a -> Int
V.length Vector a
v)) (((Int, Int) -> ST s ()) -> ST s ())
-> ((Int, Int) -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \(Int
i,Int
j) -> do
    a
vi <- MVector (PrimState (ST s)) a -> Int -> ST s a
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
MV.read MVector s a
MVector (PrimState (ST s)) a
m Int
i
    a
vj <- MVector (PrimState (ST s)) a -> Int -> ST s a
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
MV.read MVector s a
MVector (PrimState (ST s)) a
m Int
j
    Bool -> ST s () -> ST s ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (a
vi a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
vj) (ST s () -> ST s ()) -> ST s () -> ST s ()
forall a b. (a -> b) -> a -> b
$ do
      MVector (PrimState (ST s)) a -> Int -> a -> ST s ()
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> a -> m ()
MV.write MVector s a
MVector (PrimState (ST s)) a
m Int
i a
vj
      MVector (PrimState (ST s)) a -> Int -> a -> ST s ()
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> a -> m ()
MV.write MVector s a
MVector (PrimState (ST s)) a
m Int
j a
vi
  MVector s a -> ST s (MVector s a)
forall (m :: * -> *) a. Monad m => a -> m a
return MVector s a
m

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

type Base = [Int]
type UDigit = Int
type UNumber = [UDigit]

isRepresentable :: Base -> Integer -> Bool
isRepresentable :: [Int] -> Integer -> Bool
isRepresentable [Int]
_ Integer
0 = Bool
True
isRepresentable [] Integer
x = Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
forall a. Bounded a => a
maxBound :: UDigit)
isRepresentable (Int
b:[Int]
bs) Integer
x = [Int] -> Integer -> Bool
isRepresentable [Int]
bs (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
b)

encode :: Base -> Integer -> UNumber
encode :: [Int] -> Integer -> [Int]
encode [Int]
_ Integer
0 = []
encode [] Integer
x
  | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
forall a. Bounded a => a
maxBound :: UDigit) = [Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
x]
  | Bool
otherwise = [Int]
forall a. HasCallStack => a
undefined
encode (Int
b:[Int]
bs) Integer
x = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
b) Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int] -> Integer -> [Int]
encode [Int]
bs (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
b)

decode :: Base -> UNumber -> Integer
decode :: [Int] -> [Int] -> Integer
decode [Int]
_ [] = Integer
0
decode [] [Int
x] = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
x
decode (Int
b:[Int]
bs) (Int
x:[Int]
xs) = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
b Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* [Int] -> [Int] -> Integer
decode [Int]
bs [Int]
xs

{-
test1 = encode [3,5] 164 -- [2,4,10]
test2 = decode [3,5] [2,4,10] -- 164

test3 = optimizeBase [1,1,2,2,3,3,3,3,7]
-}

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

type Cost = Integer

primes :: [Int]
primes :: [Int]
primes = [Int
2, Int
3, Int
5, Int
7, Int
11, Int
13, Int
17]

optimizeBase :: [Integer] -> Base
optimizeBase :: [Integer] -> [Int]
optimizeBase [Integer]
xs = [Int] -> [Int]
forall a. [a] -> [a]
reverse ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ ([Int], Integer) -> [Int]
forall a b. (a, b) -> a
fst (([Int], Integer) -> [Int]) -> ([Int], Integer) -> [Int]
forall a b. (a -> b) -> a -> b
$ Maybe ([Int], Integer) -> ([Int], Integer)
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe ([Int], Integer) -> ([Int], Integer))
-> Maybe ([Int], Integer) -> ([Int], Integer)
forall a b. (a -> b) -> a -> b
$ State (Maybe ([Int], Integer)) ()
-> Maybe ([Int], Integer) -> Maybe ([Int], Integer)
forall s a. State s a -> s -> s
execState ([Integer] -> [Int] -> Integer -> State (Maybe ([Int], Integer)) ()
m [Integer]
xs [] Integer
0) Maybe ([Int], Integer)
forall a. Maybe a
Nothing
  where
    m :: [Integer] -> Base -> Integer -> State (Maybe (Base, Cost)) ()
    m :: [Integer] -> [Int] -> Integer -> State (Maybe ([Int], Integer)) ()
m [Integer]
xs [Int]
base Integer
cost = do
      let lb :: Integer
lb = Integer
cost Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
1 | Integer
x <- [Integer]
xs, Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0]
      Maybe ([Int], Integer)
best <- StateT (Maybe ([Int], Integer)) Identity (Maybe ([Int], Integer))
forall s (m :: * -> *). MonadState s m => m s
get
      case Maybe ([Int], Integer)
best of
        Just ([Int]
_bestBase, Integer
bestCost) | Integer
bestCost Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
lb -> () -> State (Maybe ([Int], Integer)) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Maybe ([Int], Integer)
_ -> do
          Bool
-> State (Maybe ([Int], Integer)) ()
-> State (Maybe ([Int], Integer)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer]
xs Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
1024) (State (Maybe ([Int], Integer)) ()
 -> State (Maybe ([Int], Integer)) ())
-> State (Maybe ([Int], Integer)) ()
-> State (Maybe ([Int], Integer)) ()
forall a b. (a -> b) -> a -> b
$ do
            let cost' :: Integer
cost' = Integer
cost Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer]
xs
            case Maybe ([Int], Integer)
best of
              Just ([Int]
_bestBase, Integer
bestCost) | Integer
bestCost Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
cost' -> () -> State (Maybe ([Int], Integer)) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Maybe ([Int], Integer)
_ -> Maybe ([Int], Integer) -> State (Maybe ([Int], Integer)) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Maybe ([Int], Integer) -> State (Maybe ([Int], Integer)) ())
-> Maybe ([Int], Integer) -> State (Maybe ([Int], Integer)) ()
forall a b. (a -> b) -> a -> b
$ ([Int], Integer) -> Maybe ([Int], Integer)
forall a. a -> Maybe a
Just ([Int]
base, Integer
cost')
          Bool
-> State (Maybe ([Int], Integer)) ()
-> State (Maybe ([Int], Integer)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Integer] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Integer]
xs) (State (Maybe ([Int], Integer)) ()
 -> State (Maybe ([Int], Integer)) ())
-> State (Maybe ([Int], Integer)) ()
-> State (Maybe ([Int], Integer)) ()
forall a b. (a -> b) -> a -> b
$ do
            let delta :: [(Int, Integer)]
delta = ((Int, Integer) -> (Int, Integer) -> Ordering)
-> [(Int, Integer)] -> [(Int, Integer)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Int, Integer) -> Integer)
-> (Int, Integer) -> (Int, Integer) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Int, Integer) -> Integer
forall a b. (a, b) -> b
snd) [(Int
p, [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
p | Integer
x <- [Integer]
xs]) | Int
p <- [Int]
primes]
            case [(Int, Integer)]
delta of
              (Int
p,Integer
0) : [(Int, Integer)]
_ -> do
                [Integer] -> [Int] -> Integer -> State (Maybe ([Int], Integer)) ()
m [Integer
d | Integer
x <- [Integer]
xs, let d :: Integer
d = Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
p, Integer
d Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0] (Int
p Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
base) Integer
cost
              [(Int, Integer)]
_ -> do
                [(Int, Integer)]
-> ((Int, Integer) -> State (Maybe ([Int], Integer)) ())
-> State (Maybe ([Int], Integer)) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Int, Integer)]
delta (((Int, Integer) -> State (Maybe ([Int], Integer)) ())
 -> State (Maybe ([Int], Integer)) ())
-> ((Int, Integer) -> State (Maybe ([Int], Integer)) ())
-> State (Maybe ([Int], Integer)) ()
forall a b. (a -> b) -> a -> b
$ \(Int
p,Integer
s) -> do
                  [Integer] -> [Int] -> Integer -> State (Maybe ([Int], Integer)) ()
m [Integer
d | Integer
x <- [Integer]
xs, let d :: Integer
d = Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
p, Integer
d Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0] (Int
p Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
base) (Integer
cost Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
s)

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

addPBLinAtLeastSorter :: PrimMonad m => Tseitin.Encoder m -> SAT.PBLinAtLeast -> m ()
addPBLinAtLeastSorter :: Encoder m -> PBLinAtLeast -> m ()
addPBLinAtLeastSorter Encoder m
enc PBLinAtLeast
constr = do
  Formula
formula <- Encoder m -> PBLinAtLeast -> m Formula
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> PBLinAtLeast -> m Formula
encodePBLinAtLeastSorter' Encoder m
enc PBLinAtLeast
constr
  Encoder m -> Formula -> m ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula Encoder m
enc Formula
formula

encodePBLinAtLeastSorter :: PrimMonad m => Tseitin.Encoder m -> SAT.PBLinAtLeast -> m SAT.Lit
encodePBLinAtLeastSorter :: Encoder m -> PBLinAtLeast -> m Int
encodePBLinAtLeastSorter Encoder m
enc PBLinAtLeast
constr = do
  Formula
formula <- Encoder m -> PBLinAtLeast -> m Formula
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> PBLinAtLeast -> m Formula
encodePBLinAtLeastSorter' Encoder m
enc PBLinAtLeast
constr
  Encoder m -> Formula -> m Int
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Int
Tseitin.encodeFormula Encoder m
enc Formula
formula

encodePBLinAtLeastSorter' :: PrimMonad m => Tseitin.Encoder m -> SAT.PBLinAtLeast -> m Tseitin.Formula
encodePBLinAtLeastSorter' :: Encoder m -> PBLinAtLeast -> m Formula
encodePBLinAtLeastSorter' Encoder m
enc (PBLinSum
lhs,Integer
rhs) = do
  let base :: [Int]
base = [Integer] -> [Int]
optimizeBase [Integer
c | (Integer
c,Int
_) <- PBLinSum
lhs]
  if [Int] -> Integer -> Bool
isRepresentable [Int]
base Integer
rhs then do
    [Vector Int]
sorters <- Encoder m -> [Int] -> [([Int], Int)] -> [Int] -> m [Vector Int]
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> [Int] -> [([Int], Int)] -> [Int] -> m [Vector Int]
genSorters Encoder m
enc [Int]
base [([Int] -> Integer -> [Int]
encode [Int]
base Integer
c, Int
l) | (Integer
c,Int
l) <- PBLinSum
lhs] []
    Formula -> m Formula
forall (m :: * -> *) a. Monad m => a -> m a
return (Formula -> m Formula) -> Formula -> m Formula
forall a b. (a -> b) -> a -> b
$ [Int] -> [Vector Int] -> [Int] -> Formula
lexComp [Int]
base [Vector Int]
sorters ([Int] -> Integer -> [Int]
encode [Int]
base Integer
rhs)
  else do
    Formula -> m Formula
forall (m :: * -> *) a. Monad m => a -> m a
return Formula
forall a. MonotoneBoolean a => a
false

genSorters :: PrimMonad m => Tseitin.Encoder m -> Base -> [(UNumber, SAT.Lit)] -> [SAT.Lit] -> m [Vector SAT.Lit]
genSorters :: Encoder m -> [Int] -> [([Int], Int)] -> [Int] -> m [Vector Int]
genSorters Encoder m
enc [Int]
base [([Int], Int)]
lhs [Int]
carry = do
  let is :: Vector Int
is = [Int] -> Vector Int
forall a. [a] -> Vector a
V.fromList [Int]
carry Vector Int -> Vector Int -> Vector Int
forall a. Semigroup a => a -> a -> a
<> [Vector Int] -> Vector Int
forall a. [Vector a] -> Vector a
V.concat [Int -> Int -> Vector Int
forall a. Int -> a -> Vector a
V.replicate (Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
d) Int
l | (Int
d:[Int]
_,Int
l) <- [([Int], Int)]
lhs, Int
d Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0]
  MVector (PrimState m) Int
buf <- Vector Int -> m (MVector (PrimState m) Int)
forall (m :: * -> *) a.
PrimMonad m =>
Vector a -> m (MVector (PrimState m) a)
V.thaw Vector Int
is
  [(Int, Int)] -> ((Int, Int) -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Int -> [(Int, Int)]
genSorterCircuit (Vector Int -> Int
forall a. Vector a -> Int
V.length Vector Int
is)) (((Int, Int) -> m ()) -> m ()) -> ((Int, Int) -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \(Int
i,Int
j) -> do
    Int
vi <- MVector (PrimState m) Int -> Int -> m Int
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
MV.read MVector (PrimState m) Int
buf Int
i
    Int
vj <- MVector (PrimState m) Int -> Int -> m Int
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
MV.read MVector (PrimState m) Int
buf Int
j
    MVector (PrimState m) Int -> Int -> Int -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> a -> m ()
MV.write MVector (PrimState m) Int
buf Int
i (Int -> m ()) -> m Int -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Encoder m -> [Int] -> m Int
forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeDisj Encoder m
enc [Int
vi,Int
vj]
    MVector (PrimState m) Int -> Int -> Int -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> a -> m ()
MV.write MVector (PrimState m) Int
buf Int
j (Int -> m ()) -> m Int -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Encoder m -> [Int] -> m Int
forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeConj Encoder m
enc [Int
vi,Int
vj]
  Vector Int
os <- MVector (PrimState m) Int -> m (Vector Int)
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> m (Vector a)
V.freeze MVector (PrimState m) Int
buf
  case [Int]
base of
    [] -> [Vector Int] -> m [Vector Int]
forall (m :: * -> *) a. Monad m => a -> m a
return [Vector Int
os]
    Int
b:[Int]
bs -> do
      [Vector Int]
oss <- Encoder m -> [Int] -> [([Int], Int)] -> [Int] -> m [Vector Int]
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> [Int] -> [([Int], Int)] -> [Int] -> m [Vector Int]
genSorters Encoder m
enc [Int]
bs [([Int]
ds,Int
l) | (Int
_:[Int]
ds,Int
l) <- [([Int], Int)]
lhs] [Vector Int
osVector Int -> Int -> Int
forall a. Vector a -> Int -> a
!(Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) | Int
i <- (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Vector Int -> Int
forall a. Vector a -> Int
V.length Vector Int
os) ((Int -> Int) -> Int -> [Int]
forall a. (a -> a) -> a -> [a]
iterate (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
b) Int
b)]
      [Vector Int] -> m [Vector Int]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Vector Int] -> m [Vector Int]) -> [Vector Int] -> m [Vector Int]
forall a b. (a -> b) -> a -> b
$ Vector Int
os Vector Int -> [Vector Int] -> [Vector Int]
forall a. a -> [a] -> [a]
: [Vector Int]
oss

isGE :: Vector SAT.Lit -> Int -> Tseitin.Formula
isGE :: Vector Int -> Int -> Formula
isGE Vector Int
out Int
lim
  | Int
lim Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = Formula
forall a. MonotoneBoolean a => a
true
  | Int
lim Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Vector Int -> Int
forall a. Vector a -> Int
V.length Vector Int
out = Int -> Formula
forall a. a -> BoolExpr a
Atom (Int -> Formula) -> Int -> Formula
forall a b. (a -> b) -> a -> b
$ Vector Int
out Vector Int -> Int -> Int
forall a. Vector a -> Int -> a
! (Int
lim Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
  | Bool
otherwise = Formula
forall a. MonotoneBoolean a => a
false

isGEMod :: Int -> Vector SAT.Lit -> Int -> Tseitin.Formula
isGEMod :: Int -> Vector Int -> Int -> Formula
isGEMod Int
_n Vector Int
_out Int
lim | Int
lim Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = Formula
forall a. MonotoneBoolean a => a
true
isGEMod Int
n Vector Int
out Int
lim =
  [Formula] -> Formula
forall a. MonotoneBoolean a => [a] -> a
orB [Vector Int -> Int -> Formula
isGE Vector Int
out (Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
lim) Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. (Vector Int -> Int -> Formula) -> Vector Int -> Int -> Formula
forall a. Complement a => a -> a
notB Vector Int -> Int -> Formula
isGE Vector Int
out (Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) | Int
j <- [Int
0, Int
n .. Vector Int -> Int
forall a. Vector a -> Int
V.length Vector Int
out Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]

lexComp :: Base -> [Vector SAT.Lit] -> UNumber -> Tseitin.Formula
lexComp :: [Int] -> [Vector Int] -> [Int] -> Formula
lexComp [Int]
base [Vector Int]
lhs [Int]
rhs = Formula -> [Int] -> [Vector Int] -> [Int] -> Formula
f Formula
forall a. MonotoneBoolean a => a
true [Int]
base [Vector Int]
lhs [Int]
rhs
  where
    f :: Formula -> [Int] -> [Vector Int] -> [Int] -> Formula
f Formula
ret (Int
b:[Int]
bs) (Vector Int
out:[Vector Int]
os) [Int]
ds = Formula -> [Int] -> [Vector Int] -> [Int] -> Formula
f (Formula
gt Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.||. (Formula
ge Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Formula
ret)) [Int]
bs [Vector Int]
os (Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
drop Int
1 [Int]
ds)
      where
        d :: Int
d = if [Int] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
ds then Int
0 else [Int] -> Int
forall a. [a] -> a
head [Int]
ds
        gt :: Formula
gt = Int -> Vector Int -> Int -> Formula
isGEMod Int
b Vector Int
out (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
        ge :: Formula
ge = Int -> Vector Int -> Int -> Formula
isGEMod Int
b Vector Int
out Int
d
    f Formula
ret [] [Vector Int
out] [Int]
ds = Formula
gt Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.||. (Formula
ge Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Formula
ret)
      where
        d :: Int
d = if [Int] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
ds then Int
0 else [Int] -> Int
forall a. [a] -> a
head [Int]
ds
        gt :: Formula
gt = Vector Int -> Int -> Formula
isGE Vector Int
out (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
        ge :: Formula
ge = Vector Int -> Int -> Formula
isGE Vector Int
out Int
d

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