{-# 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.Boolean
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Encoder.Tseitin (Formula (..))

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

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

    mergeSort :: Vector b -> m ()
mergeSort Vector b
is
      | forall a. Vector a -> Int
V.length Vector b
is forall a. Ord a => a -> a -> Bool
<= Int
1 = forall (m :: * -> *) a. Monad m => a -> m a
return ()
      | forall a. Vector a -> Int
V.length Vector b
is forall a. Eq a => a -> a -> Bool
== Int
2 = forall {a} {b} {m :: * -> *}.
MonadWriter ([(a, b)] -> [(a, b)]) m =>
a -> b -> m ()
genCompareAndSwap (Vector b
isforall a. Vector a -> Int -> a
!Int
0) (Vector b
isforall a. Vector a -> Int -> a
!Int
1)
      | Bool
otherwise =
          case 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
              forall {m :: * -> *} {b}.
MonadWriter ([(b, b)] -> [(b, b)]) m =>
Vector b -> m ()
oddEvenMerge Vector b
is

    oddEvenMerge :: Vector b -> m ()
oddEvenMerge Vector b
is
      | forall a. Vector a -> Int
V.length Vector b
is forall a. Ord a => a -> a -> Bool
<= Int
1 = forall (m :: * -> *) a. Monad m => a -> m a
return ()
      | forall a. Vector a -> Int
V.length Vector b
is forall a. Eq a => a -> a -> Bool
== Int
2 = forall {a} {b} {m :: * -> *}.
MonadWriter ([(a, b)] -> [(a, b)]) m =>
a -> b -> m ()
genCompareAndSwap (Vector b
isforall a. Vector a -> Int -> a
!Int
0) (Vector b
isforall a. Vector a -> Int -> a
!Int
1)
      | Bool
otherwise =
          case 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
              forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int
2,Int
3 .. forall a. Vector a -> Int
V.length Vector b
isforall a. Num a => a -> a -> a
-Int
1] forall a b. (a -> b) -> a -> b
$ \Int
i -> do
                forall {a} {b} {m :: * -> *}.
MonadWriter ([(a, b)] -> [(a, b)]) m =>
a -> b -> m ()
genCompareAndSwap (Vector b
isforall a. Vector a -> Int -> a
!(Int
iforall a. Num a => a -> a -> a
-Int
1)) (Vector b
isforall a. Vector a -> Int -> a
!Int
i)

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

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

sortVector :: (Ord a) => Vector a -> Vector a
sortVector :: forall a. Ord a => Vector a -> Vector a
sortVector Vector a
v = forall a. (forall s. ST s (MVector s a)) -> Vector a
V.create forall a b. (a -> b) -> a -> b
$ do
  MVector s a
m <- forall (m :: * -> *) a.
PrimMonad m =>
Vector a -> m (MVector (PrimState m) a)
V.thaw Vector a
v
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Int -> [(Int, Int)]
genSorterCircuit (forall a. Vector a -> Int
V.length Vector a
v)) forall a b. (a -> b) -> a -> b
$ \(Int
i,Int
j) -> do
    a
vi <- forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
MV.read MVector s a
m Int
i
    a
vj <- forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
MV.read MVector s a
m Int
j
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (a
vi forall a. Ord a => a -> a -> Bool
> a
vj) forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> a -> m ()
MV.write MVector s a
m Int
i a
vj
      forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> a -> m ()
MV.write MVector s a
m Int
j a
vi
  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 :: Base -> Cost -> Bool
isRepresentable Base
_ Cost
0 = Bool
True
isRepresentable [] Cost
x = Cost
x forall a. Ord a => a -> a -> Bool
<= forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
maxBound :: UDigit)
isRepresentable (Int
b:Base
bs) Cost
x = Base -> Cost -> Bool
isRepresentable Base
bs (Cost
x forall a. Integral a => a -> a -> a
`div` forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
b)

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

decode :: Base -> UNumber -> Integer
decode :: Base -> Base -> Cost
decode Base
_ [] = Cost
0
decode [] [Int
x] = forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
x
decode (Int
b:Base
bs) (Int
x:Base
xs) = forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
x forall a. Num a => a -> a -> a
+ forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
b forall a. Num a => a -> a -> a
* Base -> Base -> Cost
decode Base
bs Base
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 :: Base
primes = [Int
2, Int
3, Int
5, Int
7, Int
11, Int
13, Int
17]

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

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

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

genSorters :: PrimMonad m => Tseitin.Encoder m -> Base -> [(UNumber, SAT.Lit)] -> [SAT.Lit] -> m [Vector SAT.Lit]
genSorters :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Base -> [(Base, Int)] -> Base -> m [Vector Int]
genSorters Encoder m
enc Base
base [(Base, Int)]
lhs Base
carry = do
  let is :: Vector Int
is = forall a. [a] -> Vector a
V.fromList Base
carry forall a. Semigroup a => a -> a -> a
<> forall a. [Vector a] -> Vector a
V.concat [forall a. Int -> a -> Vector a
V.replicate (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
d) Int
l | (Int
d:Base
_,Int
l) <- [(Base, Int)]
lhs, Int
d forall a. Eq a => a -> a -> Bool
/= Int
0]
  MVector (PrimState m) Int
buf <- forall (m :: * -> *) a.
PrimMonad m =>
Vector a -> m (MVector (PrimState m) a)
V.thaw Vector Int
is
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Int -> [(Int, Int)]
genSorterCircuit (forall a. Vector a -> Int
V.length Vector Int
is)) forall a b. (a -> b) -> a -> b
$ \(Int
i,Int
j) -> do
    Int
vi <- forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
MV.read MVector (PrimState m) Int
buf Int
i
    Int
vj <- forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
MV.read MVector (PrimState m) Int
buf Int
j
    forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> a -> m ()
MV.write MVector (PrimState m) Int
buf Int
i forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). PrimMonad m => Encoder m -> Base -> m Int
Tseitin.encodeDisj Encoder m
enc [Int
vi,Int
vj]
    forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> a -> m ()
MV.write MVector (PrimState m) Int
buf Int
j forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). PrimMonad m => Encoder m -> Base -> m Int
Tseitin.encodeConj Encoder m
enc [Int
vi,Int
vj]
  Vector Int
os <- forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> m (Vector a)
V.freeze MVector (PrimState m) Int
buf
  case Base
base of
    [] -> forall (m :: * -> *) a. Monad m => a -> m a
return [Vector Int
os]
    Int
b:Base
bs -> do
      [Vector Int]
oss <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Base -> [(Base, Int)] -> Base -> m [Vector Int]
genSorters Encoder m
enc Base
bs [(Base
ds,Int
l) | (Int
_:Base
ds,Int
l) <- [(Base, Int)]
lhs] [Vector Int
osforall a. Vector a -> Int -> a
!(Int
iforall a. Num a => a -> a -> a
-Int
1) | Int
i <- forall a. (a -> Bool) -> [a] -> [a]
takeWhile (forall a. Ord a => a -> a -> Bool
<= forall a. Vector a -> Int
V.length Vector Int
os) (forall a. (a -> a) -> a -> [a]
iterate (forall a. Num a => a -> a -> a
+Int
b) Int
b)]
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Vector Int
os 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 forall a. Ord a => a -> a -> Bool
<= Int
0 = forall a. MonotoneBoolean a => a
true
  | Int
lim forall a. Num a => a -> a -> a
- Int
1 forall a. Ord a => a -> a -> Bool
< forall a. Vector a -> Int
V.length Vector Int
out = Int -> Formula
Atom forall a b. (a -> b) -> a -> b
$ Vector Int
out forall a. Vector a -> Int -> a
! (Int
lim forall a. Num a => a -> a -> a
- Int
1)
  | Bool
otherwise = 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 forall a. Ord a => a -> a -> Bool
<= Int
0 = forall a. MonotoneBoolean a => a
true
isGEMod Int
n Vector Int
out Int
lim =
  forall a. MonotoneBoolean a => [a] -> a
orB [Vector Int -> Int -> Formula
isGE Vector Int
out (Int
j forall a. Num a => a -> a -> a
+ Int
lim) forall a. MonotoneBoolean a => a -> a -> a
.&&. forall a. Complement a => a -> a
notB Vector Int -> Int -> Formula
isGE Vector Int
out (Int
j forall a. Num a => a -> a -> a
+ Int
n) | Int
j <- [Int
0, Int
n .. forall a. Vector a -> Int
V.length Vector Int
out forall a. Num a => a -> a -> a
- Int
1]]

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

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