{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Types
-- Copyright   :  (c) Masahiro Sakai 2012
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.SAT.Types
  (
  -- * Variable
    Var
  , VarSet
  , VarMap
  , validVar

  -- * Model
  , IModel (..)
  , Model
  , restrictModel

  -- * Literal
  , Lit
  , LitSet
  , LitMap
  , litUndef
  , validLit
  , literal
  , litNot
  , litVar
  , litPolarity
  , evalLit

  -- * Clause
  , Clause
  , normalizeClause
  , instantiateClause
  , clauseSubsume
  , evalClause
  , clauseToPBLinAtLeast

  -- * Packed Clause
  , PackedVar
  , PackedLit
  , packLit
  , unpackLit
  , PackedClause
  , packClause
  , unpackClause

  -- * Cardinality Constraint
  , AtLeast
  , Exactly
  , normalizeAtLeast
  , instantiateAtLeast
  , evalAtLeast
  , evalExactly

  -- * (Linear) Pseudo Boolean Constraint
  , PBLinTerm
  , PBLinSum
  , PBLinAtLeast
  , PBLinExactly
  , normalizePBLinSum
  , normalizePBLinAtLeast
  , normalizePBLinExactly
  , instantiatePBLinAtLeast
  , instantiatePBLinExactly
  , cutResolve
  , cardinalityReduction
  , negatePBLinAtLeast
  , evalPBLinSum
  , evalPBLinAtLeast
  , evalPBLinExactly
  , pbLinLowerBound
  , pbLinUpperBound
  , pbLinSubsume

  -- * Non-linear Pseudo Boolean constraint
  , PBTerm
  , PBSum
  , evalPBSum
  , evalPBConstraint
  , evalPBFormula
  , pbLowerBound
  , pbUpperBound
  , removeNegationFromPBSum

  -- * XOR Clause
  , XORClause
  , normalizeXORClause
  , instantiateXORClause
  , evalXORClause

  -- * Type classes for solvers
  , NewVar (..)
  , AddClause (..)
  , AddCardinality (..)
  , AddPBLin (..)
  , AddPBNL (..)
  , AddXORClause (..)
  ) where

import Control.Monad
import Control.Exception
import Data.Array.Unboxed
import Data.Ord
import Data.List
import Data.Int
import Data.IntMap.Strict (IntMap)
import qualified Data.IntMap.Strict as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe
import qualified Data.Vector as V
import qualified Data.Vector.Unboxed as VU
import qualified Data.PseudoBoolean as PBFile
import ToySolver.Data.LBool
import qualified ToySolver.Combinatorial.SubsetSum as SubsetSum

-- | Variable is represented as positive integers (DIMACS format).
type Var = Int

type VarSet = IntSet
type VarMap = IntMap

{-# INLINE validVar #-}
validVar :: Var -> Bool
validVar :: Var -> Bool
validVar Var
v = Var
v Var -> Var -> Bool
forall a. Ord a => a -> a -> Bool
> Var
0

class IModel a where
  evalVar :: a -> Var -> Bool

-- | A model is represented as a mapping from variables to its values.
type Model = UArray Var Bool

-- | Restrict model to first @nv@ variables.
restrictModel :: Int -> Model -> Model
restrictModel :: Var -> Model -> Model
restrictModel Var
nv Model
m = (Var, Var) -> [(Var, Bool)] -> Model
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Var
1,Var
nv) [(Var
v, Model
m Model -> Var -> Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
v) | Var
v <- [Var
1..Var
nv]]

instance IModel (UArray Var Bool) where
  evalVar :: Model -> Var -> Bool
evalVar Model
m Var
v = Model
m Model -> Var -> Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
v

instance IModel (Array Var Bool) where
  evalVar :: Array Var Bool -> Var -> Bool
evalVar Array Var Bool
m Var
v = Array Var Bool
m Array Var Bool -> Var -> Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
v

instance IModel (Var -> Bool) where
  evalVar :: (Var -> Bool) -> Var -> Bool
evalVar Var -> Bool
m Var
v = Var -> Bool
m Var
v

-- | Positive (resp. negative) literals are represented as positive (resp.
-- negative) integers. (DIMACS format).
type Lit = Int

{-# INLINE litUndef #-}
litUndef :: Lit
litUndef :: Var
litUndef = Var
0

type LitSet = IntSet
type LitMap = IntMap

{-# INLINE validLit #-}
validLit :: Lit -> Bool
validLit :: Var -> Bool
validLit Var
l = Var
l Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
/= Var
0

{-# INLINE literal #-}
-- | Construct a literal from a variable and its polarity.
-- 'True' (resp 'False') means positive (resp. negative) literal.
literal :: Var  -- ^ variable
        -> Bool -- ^ polarity
        -> Lit
literal :: Var -> Bool -> Var
literal Var
v Bool
polarity =
  Bool -> Var -> Var
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Var -> Bool
validVar Var
v) (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$ if Bool
polarity then Var
v else Var -> Var
litNot Var
v

{-# INLINE litNot #-}
-- | Negation of the 'Lit'.
litNot :: Lit -> Lit
litNot :: Var -> Var
litNot Var
l = Bool -> Var -> Var
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Var -> Bool
validLit Var
l) (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$ Var -> Var
forall a. Num a => a -> a
negate Var
l

{-# INLINE litVar #-}
-- | Underlying variable of the 'Lit'
litVar :: Lit -> Var
litVar :: Var -> Var
litVar Var
l = Bool -> Var -> Var
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Var -> Bool
validLit Var
l) (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$ Var -> Var
forall a. Num a => a -> a
abs Var
l

{-# INLINE litPolarity #-}
-- | Polarity of the 'Lit'.
-- 'True' means positive literal and 'False' means negative literal.
litPolarity :: Lit -> Bool
litPolarity :: Var -> Bool
litPolarity Var
l = Bool -> Bool -> Bool
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Var -> Bool
validLit Var
l) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Var
l Var -> Var -> Bool
forall a. Ord a => a -> a -> Bool
> Var
0

{-# INLINEABLE evalLit #-}
{-# SPECIALIZE evalLit :: Model -> Lit -> Bool #-}
evalLit :: IModel m => m -> Lit -> Bool
evalLit :: m -> Var -> Bool
evalLit m
m Var
l = if Var
l Var -> Var -> Bool
forall a. Ord a => a -> a -> Bool
> Var
0 then m -> Var -> Bool
forall a. IModel a => a -> Var -> Bool
evalVar m
m Var
l else Bool -> Bool
not (m -> Var -> Bool
forall a. IModel a => a -> Var -> Bool
evalVar m
m (Var -> Var
forall a. Num a => a -> a
abs Var
l))

-- | Disjunction of 'Lit'.
type Clause = [Lit]

-- | Normalizing clause
--
-- 'Nothing' if the clause is trivially true.
normalizeClause :: Clause -> Maybe Clause
normalizeClause :: Clause -> Maybe Clause
normalizeClause Clause
lits = Bool -> Maybe Clause -> Maybe Clause
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (IntSet -> Var
IntSet.size IntSet
ys Var -> Var -> Var
forall a. Integral a => a -> a -> a
`mod` Var
2 Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
0) (Maybe Clause -> Maybe Clause) -> Maybe Clause -> Maybe Clause
forall a b. (a -> b) -> a -> b
$
  if IntSet -> Bool
IntSet.null IntSet
ys
    then Clause -> Maybe Clause
forall a. a -> Maybe a
Just (IntSet -> Clause
IntSet.toList IntSet
xs)
    else Maybe Clause
forall a. Maybe a
Nothing
  where
    xs :: IntSet
xs = Clause -> IntSet
IntSet.fromList Clause
lits
    ys :: IntSet
ys = IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.intersection` ((Var -> Var) -> IntSet -> IntSet
IntSet.map Var -> Var
litNot IntSet
xs)

{-# SPECIALIZE instantiateClause :: (Lit -> IO LBool) -> Clause -> IO (Maybe Clause) #-}
instantiateClause :: forall m. Monad m => (Lit -> m LBool) -> Clause -> m (Maybe Clause)
instantiateClause :: (Var -> m LBool) -> Clause -> m (Maybe Clause)
instantiateClause Var -> m LBool
evalLitM = Clause -> Clause -> m (Maybe Clause)
loop []
  where
    loop :: [Lit] -> [Lit] -> m (Maybe Clause)
    loop :: Clause -> Clause -> m (Maybe Clause)
loop Clause
ret [] = Maybe Clause -> m (Maybe Clause)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Clause -> m (Maybe Clause))
-> Maybe Clause -> m (Maybe Clause)
forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Clause
forall a. a -> Maybe a
Just Clause
ret
    loop Clause
ret (Var
l:Clause
ls) = do
      LBool
val <- Var -> m LBool
evalLitM Var
l
      if LBool
valLBool -> LBool -> Bool
forall a. Eq a => a -> a -> Bool
==LBool
lTrue then
        Maybe Clause -> m (Maybe Clause)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Clause
forall a. Maybe a
Nothing
      else if LBool
valLBool -> LBool -> Bool
forall a. Eq a => a -> a -> Bool
==LBool
lFalse then
        Clause -> Clause -> m (Maybe Clause)
loop Clause
ret Clause
ls
      else
        Clause -> Clause -> m (Maybe Clause)
loop (Var
l Var -> Clause -> Clause
forall a. a -> [a] -> [a]
: Clause
ret) Clause
ls

clauseSubsume :: Clause -> Clause -> Bool
clauseSubsume :: Clause -> Clause -> Bool
clauseSubsume Clause
cl1 Clause
cl2 = IntSet
cl1' IntSet -> IntSet -> Bool
`IntSet.isSubsetOf` IntSet
cl2'
  where
    cl1' :: IntSet
cl1' = Clause -> IntSet
IntSet.fromList Clause
cl1
    cl2' :: IntSet
cl2' = Clause -> IntSet
IntSet.fromList Clause
cl2

evalClause :: IModel m => m -> Clause -> Bool
evalClause :: m -> Clause -> Bool
evalClause m
m Clause
cl = (Var -> Bool) -> Clause -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (m -> Var -> Bool
forall a. IModel a => a -> Var -> Bool
evalLit m
m) Clause
cl

clauseToPBLinAtLeast :: Clause -> PBLinAtLeast
clauseToPBLinAtLeast :: Clause -> PBLinAtLeast
clauseToPBLinAtLeast Clause
xs = ([(Integer
1,Var
l) | Var
l <- Clause
xs], Integer
1)

type PackedVar = PackedLit
type PackedLit = Int32

packLit :: Lit -> PackedLit
packLit :: Var -> PackedLit
packLit = Var -> PackedLit
forall a b. (Integral a, Num b) => a -> b
fromIntegral

unpackLit :: PackedLit -> Lit
unpackLit :: PackedLit -> Var
unpackLit = PackedLit -> Var
forall a b. (Integral a, Num b) => a -> b
fromIntegral

type PackedClause = VU.Vector PackedLit

packClause :: Clause -> PackedClause
packClause :: Clause -> PackedClause
packClause = [PackedLit] -> PackedClause
forall a. Unbox a => [a] -> Vector a
VU.fromList ([PackedLit] -> PackedClause)
-> (Clause -> [PackedLit]) -> Clause -> PackedClause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var -> PackedLit) -> Clause -> [PackedLit]
forall a b. (a -> b) -> [a] -> [b]
map Var -> PackedLit
packLit

unpackClause :: PackedClause -> Clause
unpackClause :: PackedClause -> Clause
unpackClause = (PackedLit -> Var) -> [PackedLit] -> Clause
forall a b. (a -> b) -> [a] -> [b]
map PackedLit -> Var
unpackLit ([PackedLit] -> Clause)
-> (PackedClause -> [PackedLit]) -> PackedClause -> Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PackedClause -> [PackedLit]
forall a. Unbox a => Vector a -> [a]
VU.toList

type AtLeast = ([Lit], Int)
type Exactly = ([Lit], Int)

normalizeAtLeast :: AtLeast -> AtLeast
normalizeAtLeast :: AtLeast -> AtLeast
normalizeAtLeast (Clause
lits,Var
n) = Bool -> AtLeast -> AtLeast
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (IntSet -> Var
IntSet.size IntSet
ys Var -> Var -> Var
forall a. Integral a => a -> a -> a
`mod` Var
2 Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
0) (AtLeast -> AtLeast) -> AtLeast -> AtLeast
forall a b. (a -> b) -> a -> b
$
   (IntSet -> Clause
IntSet.toList IntSet
lits', Var
n')
   where
     xs :: IntSet
xs = Clause -> IntSet
IntSet.fromList Clause
lits
     ys :: IntSet
ys = IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.intersection` ((Var -> Var) -> IntSet -> IntSet
IntSet.map Var -> Var
litNot IntSet
xs)
     lits' :: IntSet
lits' = IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
ys
     n' :: Var
n' = Var
n Var -> Var -> Var
forall a. Num a => a -> a -> a
- (IntSet -> Var
IntSet.size IntSet
ys Var -> Var -> Var
forall a. Integral a => a -> a -> a
`div` Var
2)

{-# SPECIALIZE instantiateAtLeast :: (Lit -> IO LBool) -> AtLeast -> IO AtLeast #-}
instantiateAtLeast :: forall m. Monad m => (Lit -> m LBool) -> AtLeast -> m AtLeast
instantiateAtLeast :: (Var -> m LBool) -> AtLeast -> m AtLeast
instantiateAtLeast Var -> m LBool
evalLitM (Clause
xs,Var
n) = AtLeast -> Clause -> m AtLeast
loop ([],Var
n) Clause
xs
  where
    loop :: AtLeast -> [Lit] -> m AtLeast
    loop :: AtLeast -> Clause -> m AtLeast
loop AtLeast
ret [] = AtLeast -> m AtLeast
forall (m :: * -> *) a. Monad m => a -> m a
return AtLeast
ret
    loop (Clause
ys,Var
m) (Var
l:Clause
ls) = do
      LBool
val <- Var -> m LBool
evalLitM Var
l
      if LBool
val LBool -> LBool -> Bool
forall a. Eq a => a -> a -> Bool
== LBool
lTrue then
        AtLeast -> Clause -> m AtLeast
loop (Clause
ys, Var
mVar -> Var -> Var
forall a. Num a => a -> a -> a
-Var
1) Clause
ls
      else if LBool
val LBool -> LBool -> Bool
forall a. Eq a => a -> a -> Bool
== LBool
lFalse then
        AtLeast -> Clause -> m AtLeast
loop (Clause
ys, Var
m) Clause
ls
      else
        AtLeast -> Clause -> m AtLeast
loop (Var
lVar -> Clause -> Clause
forall a. a -> [a] -> [a]
:Clause
ys, Var
m) Clause
ls

evalAtLeast :: IModel m => m -> AtLeast -> Bool
evalAtLeast :: m -> AtLeast -> Bool
evalAtLeast m
m (Clause
lits,Var
n) = Clause -> Var
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Var
1 | Var
lit <- Clause
lits, m -> Var -> Bool
forall a. IModel a => a -> Var -> Bool
evalLit m
m Var
lit] Var -> Var -> Bool
forall a. Ord a => a -> a -> Bool
>= Var
n

evalExactly :: IModel m => m -> Exactly -> Bool
evalExactly :: m -> AtLeast -> Bool
evalExactly m
m (Clause
lits,Var
n) = Clause -> Var
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Var
1 | Var
lit <- Clause
lits, m -> Var -> Bool
forall a. IModel a => a -> Var -> Bool
evalLit m
m Var
lit] Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
n

type PBLinTerm = (Integer, Lit)
type PBLinSum = [PBLinTerm]
type PBLinAtLeast = (PBLinSum, Integer)
type PBLinExactly = (PBLinSum, Integer)

-- | normalizing PB term of the form /c1 x1 + c2 x2 ... cn xn + c/ into
-- /d1 x1 + d2 x2 ... dm xm + d/ where d1,...,dm ≥ 1.
normalizePBLinSum :: (PBLinSum, Integer) -> (PBLinSum, Integer)
normalizePBLinSum :: PBLinAtLeast -> PBLinAtLeast
normalizePBLinSum = PBLinAtLeast -> PBLinAtLeast
step2 (PBLinAtLeast -> PBLinAtLeast)
-> (PBLinAtLeast -> PBLinAtLeast) -> PBLinAtLeast -> PBLinAtLeast
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PBLinAtLeast -> PBLinAtLeast
step1
  where
    -- 同じ変数が複数回現れないように、一度全部 @v@ に統一。
    step1 :: (PBLinSum, Integer) -> (PBLinSum, Integer)
    step1 :: PBLinAtLeast -> PBLinAtLeast
step1 ([PBLinTerm]
xs,Integer
n) =
      case (VarMap Integer, Integer)
-> [PBLinTerm] -> (VarMap Integer, Integer)
loop (VarMap Integer
forall a. IntMap a
IntMap.empty,Integer
n) [PBLinTerm]
xs of
        (VarMap Integer
ys,Integer
n') -> ([(Integer
c,Var
v) | (Var
v,Integer
c) <- VarMap Integer -> [(Var, Integer)]
forall a. IntMap a -> [(Var, a)]
IntMap.toList VarMap Integer
ys], Integer
n')
      where
        loop :: (VarMap Integer, Integer) -> PBLinSum -> (VarMap Integer, Integer)
        loop :: (VarMap Integer, Integer)
-> [PBLinTerm] -> (VarMap Integer, Integer)
loop (VarMap Integer
ys,Integer
m) [] = (VarMap Integer
ys,Integer
m)
        loop (VarMap Integer
ys,Integer
m) ((Integer
c,Var
l):[PBLinTerm]
zs) =
          if Var -> Bool
litPolarity Var
l
            then (VarMap Integer, Integer)
-> [PBLinTerm] -> (VarMap Integer, Integer)
loop ((Integer -> Integer -> Integer)
-> Var -> Integer -> VarMap Integer -> VarMap Integer
forall a. (a -> a -> a) -> Var -> a -> IntMap a -> IntMap a
IntMap.insertWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) Var
l Integer
c VarMap Integer
ys, Integer
m) [PBLinTerm]
zs
            else (VarMap Integer, Integer)
-> [PBLinTerm] -> (VarMap Integer, Integer)
loop ((Integer -> Integer -> Integer)
-> Var -> Integer -> VarMap Integer -> VarMap Integer
forall a. (a -> a -> a) -> Var -> a -> IntMap a -> IntMap a
IntMap.insertWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) (Var -> Var
litNot Var
l) (Integer -> Integer
forall a. Num a => a -> a
negate Integer
c) VarMap Integer
ys, Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
c) [PBLinTerm]
zs

    -- 係数が0のものも取り除き、係数が負のリテラルを反転することで、
    -- 係数が正になるようにする。
    step2 :: (PBLinSum, Integer) -> (PBLinSum, Integer)
    step2 :: PBLinAtLeast -> PBLinAtLeast
step2 ([PBLinTerm]
xs,Integer
n) = PBLinAtLeast -> [PBLinTerm] -> PBLinAtLeast
forall a.
(Num a, Ord a) =>
([(a, Var)], a) -> [(a, Var)] -> ([(a, Var)], a)
loop ([],Integer
n) [PBLinTerm]
xs
      where
        loop :: ([(a, Var)], a) -> [(a, Var)] -> ([(a, Var)], a)
loop ([(a, Var)]
ys,a
m) [] = ([(a, Var)]
ys,a
m)
        loop ([(a, Var)]
ys,a
m) (t :: (a, Var)
t@(a
c,Var
l):[(a, Var)]
zs)
          | a
c a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0 = ([(a, Var)], a) -> [(a, Var)] -> ([(a, Var)], a)
loop ([(a, Var)]
ys,a
m) [(a, Var)]
zs
          | a
c a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0  = ([(a, Var)], a) -> [(a, Var)] -> ([(a, Var)], a)
loop ((a -> a
forall a. Num a => a -> a
negate a
c,Var -> Var
litNot Var
l)(a, Var) -> [(a, Var)] -> [(a, Var)]
forall a. a -> [a] -> [a]
:[(a, Var)]
ys, a
ma -> a -> a
forall a. Num a => a -> a -> a
+a
c) [(a, Var)]
zs
          | Bool
otherwise = ([(a, Var)], a) -> [(a, Var)] -> ([(a, Var)], a)
loop ((a, Var)
t(a, Var) -> [(a, Var)] -> [(a, Var)]
forall a. a -> [a] -> [a]
:[(a, Var)]
ys,a
m) [(a, Var)]
zs

-- | normalizing PB constraint of the form /c1 x1 + c2 cn ... cn xn >= b/.
normalizePBLinAtLeast :: PBLinAtLeast -> PBLinAtLeast
normalizePBLinAtLeast :: PBLinAtLeast -> PBLinAtLeast
normalizePBLinAtLeast PBLinAtLeast
a =
  case PBLinAtLeast -> PBLinAtLeast
step1 PBLinAtLeast
a of
    ([PBLinTerm]
xs,Integer
n)
      | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0     -> PBLinAtLeast -> PBLinAtLeast
step4 (PBLinAtLeast -> PBLinAtLeast) -> PBLinAtLeast -> PBLinAtLeast
forall a b. (a -> b) -> a -> b
$ PBLinAtLeast -> PBLinAtLeast
step3 ([PBLinTerm]
xs,Integer
n)
      | Bool
otherwise -> ([], Integer
0) -- trivially true
  where
    step1 :: PBLinAtLeast -> PBLinAtLeast
    step1 :: PBLinAtLeast -> PBLinAtLeast
step1 ([PBLinTerm]
xs,Integer
n) =
      case PBLinAtLeast -> PBLinAtLeast
normalizePBLinSum ([PBLinTerm]
xs,-Integer
n) of
        ([PBLinTerm]
ys,Integer
m) -> ([PBLinTerm]
ys, -Integer
m)

    -- saturation + gcd reduction
    step3 :: PBLinAtLeast -> PBLinAtLeast
    step3 :: PBLinAtLeast -> PBLinAtLeast
step3 ([PBLinTerm]
xs,Integer
n) =
      case [Integer
c | (Integer
c,Var
_) <- [PBLinTerm]
xs, Bool -> Bool -> Bool
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Integer
cInteger -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>Integer
0) (Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n)] of
        [] -> ([(Integer
1,Var
l) | (Integer
c,Var
l) <- [PBLinTerm]
xs], Integer
1)
        [Integer]
cs ->
          let d :: Integer
d = (Integer -> Integer -> Integer) -> [Integer] -> Integer
forall a. (a -> a -> a) -> [a] -> a
foldl1' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
gcd [Integer]
cs
              m :: Integer
m = (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
dInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
d
          in ([(if Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
n then Integer
m else Integer
c Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
d, Var
l) | (Integer
c,Var
l) <- [PBLinTerm]
xs], Integer
m)

    -- subset sum
    step4 :: PBLinAtLeast -> PBLinAtLeast
    step4 :: PBLinAtLeast -> PBLinAtLeast
step4 ([PBLinTerm]
xs,Integer
n) =
      case Vector Integer -> Integer -> Maybe (Integer, Vector Bool)
forall (v :: * -> *).
Vector v Integer =>
v Integer -> Integer -> Maybe (Integer, Vector Bool)
SubsetSum.minSubsetSum ([Integer] -> Vector Integer
forall a. [a] -> Vector a
V.fromList [Integer
c | (Integer
c,Var
_) <- [PBLinTerm]
xs]) Integer
n of
        Just (Integer
m, Vector Bool
_) -> ([PBLinTerm]
xs, Integer
m)
        Maybe (Integer, Vector Bool)
Nothing -> ([], Integer
1) -- false

-- | normalizing PB constraint of the form /c1 x1 + c2 cn ... cn xn = b/.
normalizePBLinExactly :: PBLinExactly -> PBLinExactly
normalizePBLinExactly :: PBLinAtLeast -> PBLinAtLeast
normalizePBLinExactly PBLinAtLeast
a =
　case PBLinAtLeast -> PBLinAtLeast
step1 (PBLinAtLeast -> PBLinAtLeast) -> PBLinAtLeast -> PBLinAtLeast
forall a b. (a -> b) -> a -> b
$ PBLinAtLeast
a of
    ([PBLinTerm]
xs,Integer
n)
      | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0    -> PBLinAtLeast -> PBLinAtLeast
step3 (PBLinAtLeast -> PBLinAtLeast) -> PBLinAtLeast -> PBLinAtLeast
forall a b. (a -> b) -> a -> b
$ PBLinAtLeast -> PBLinAtLeast
step2 ([PBLinTerm]
xs, Integer
n)
      | Bool
otherwise -> ([], Integer
1) -- false
  where
    step1 :: PBLinExactly -> PBLinExactly
    step1 :: PBLinAtLeast -> PBLinAtLeast
step1 ([PBLinTerm]
xs,Integer
n) =
      case PBLinAtLeast -> PBLinAtLeast
normalizePBLinSum ([PBLinTerm]
xs,-Integer
n) of
        ([PBLinTerm]
ys,Integer
m) -> ([PBLinTerm]
ys, -Integer
m)

    -- omega test と同様の係数の gcd による単純化
    step2 :: PBLinExactly -> PBLinExactly
    step2 :: PBLinAtLeast -> PBLinAtLeast
step2 ([],Integer
n) = ([],Integer
n)
    step2 ([PBLinTerm]
xs,Integer
n)
      | Integer
n Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
d Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = ([(Integer
c Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
d, Var
l) | (Integer
c,Var
l) <- [PBLinTerm]
xs], Integer
n Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
d)
      | Bool
otherwise      = ([], Integer
1) -- false
      where
        d :: Integer
d = (Integer -> Integer -> Integer) -> [Integer] -> Integer
forall a. (a -> a -> a) -> [a] -> a
foldl1' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
gcd [Integer
c | (Integer
c,Var
_) <- [PBLinTerm]
xs]

    -- subset sum
    step3 :: PBLinExactly -> PBLinExactly
    step3 :: PBLinAtLeast -> PBLinAtLeast
step3 constr :: PBLinAtLeast
constr@([PBLinTerm]
xs,Integer
n) =
      case Vector Integer -> Integer -> Maybe (Vector Bool)
forall (v :: * -> *).
Vector v Integer =>
v Integer -> Integer -> Maybe (Vector Bool)
SubsetSum.subsetSum ([Integer] -> Vector Integer
forall a. [a] -> Vector a
V.fromList [Integer
c | (Integer
c,Var
_) <- [PBLinTerm]
xs]) Integer
n of
        Just Vector Bool
_ -> PBLinAtLeast
constr
        Maybe (Vector Bool)
Nothing -> ([], Integer
1) -- false

{-# SPECIALIZE instantiatePBLinAtLeast :: (Lit -> IO LBool) -> PBLinAtLeast -> IO PBLinAtLeast #-}
instantiatePBLinAtLeast :: forall m. Monad m => (Lit -> m LBool) -> PBLinAtLeast -> m PBLinAtLeast
instantiatePBLinAtLeast :: (Var -> m LBool) -> PBLinAtLeast -> m PBLinAtLeast
instantiatePBLinAtLeast Var -> m LBool
evalLitM ([PBLinTerm]
xs,Integer
n) = PBLinAtLeast -> [PBLinTerm] -> m PBLinAtLeast
loop ([],Integer
n) [PBLinTerm]
xs
  where
    loop :: PBLinAtLeast -> PBLinSum -> m PBLinAtLeast
    loop :: PBLinAtLeast -> [PBLinTerm] -> m PBLinAtLeast
loop PBLinAtLeast
ret [] = PBLinAtLeast -> m PBLinAtLeast
forall (m :: * -> *) a. Monad m => a -> m a
return PBLinAtLeast
ret
    loop ([PBLinTerm]
ys,Integer
m) ((Integer
c,Var
l):[PBLinTerm]
ts) = do
      LBool
val <- Var -> m LBool
evalLitM Var
l
      if LBool
val LBool -> LBool -> Bool
forall a. Eq a => a -> a -> Bool
== LBool
lTrue then
        PBLinAtLeast -> [PBLinTerm] -> m PBLinAtLeast
loop ([PBLinTerm]
ys, Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
c) [PBLinTerm]
ts
      else if LBool
val LBool -> LBool -> Bool
forall a. Eq a => a -> a -> Bool
== LBool
lFalse then
        PBLinAtLeast -> [PBLinTerm] -> m PBLinAtLeast
loop ([PBLinTerm]
ys, Integer
m) [PBLinTerm]
ts
      else
        PBLinAtLeast -> [PBLinTerm] -> m PBLinAtLeast
loop ((Integer
c,Var
l)PBLinTerm -> [PBLinTerm] -> [PBLinTerm]
forall a. a -> [a] -> [a]
:[PBLinTerm]
ys, Integer
m) [PBLinTerm]
ts

{-# SPECIALIZE instantiatePBLinExactly :: (Lit -> IO LBool) -> PBLinExactly -> IO PBLinExactly #-}
instantiatePBLinExactly :: Monad m => (Lit -> m LBool) -> PBLinExactly -> m PBLinExactly
instantiatePBLinExactly :: (Var -> m LBool) -> PBLinAtLeast -> m PBLinAtLeast
instantiatePBLinExactly = (Var -> m LBool) -> PBLinAtLeast -> m PBLinAtLeast
forall (m :: * -> *).
Monad m =>
(Var -> m LBool) -> PBLinAtLeast -> m PBLinAtLeast
instantiatePBLinAtLeast

cutResolve :: PBLinAtLeast -> PBLinAtLeast -> Var -> PBLinAtLeast
cutResolve :: PBLinAtLeast -> PBLinAtLeast -> Var -> PBLinAtLeast
cutResolve ([PBLinTerm]
lhs1,Integer
rhs1) ([PBLinTerm]
lhs2,Integer
rhs2) Var
v = Bool -> PBLinAtLeast -> PBLinAtLeast
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Var
l1 Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var -> Var
litNot Var
l2) (PBLinAtLeast -> PBLinAtLeast) -> PBLinAtLeast -> PBLinAtLeast
forall a b. (a -> b) -> a -> b
$ PBLinAtLeast -> PBLinAtLeast
normalizePBLinAtLeast PBLinAtLeast
pb
  where
    (Integer
c1,Var
l1) = [PBLinTerm] -> PBLinTerm
forall a. [a] -> a
head [(Integer
c,Var
l) | (Integer
c,Var
l) <- [PBLinTerm]
lhs1, Var -> Var
litVar Var
l Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
v]
    (Integer
c2,Var
l2) = [PBLinTerm] -> PBLinTerm
forall a. [a] -> a
head [(Integer
c,Var
l) | (Integer
c,Var
l) <- [PBLinTerm]
lhs2, Var -> Var
litVar Var
l Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
v]
    g :: Integer
g = Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
gcd Integer
c1 Integer
c2
    s1 :: Integer
s1 = Integer
c2 Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
g
    s2 :: Integer
s2 = Integer
c1 Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
g
    pb :: PBLinAtLeast
pb = ([(Integer
s1Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
c,Var
l) | (Integer
c,Var
l) <- [PBLinTerm]
lhs1] [PBLinTerm] -> [PBLinTerm] -> [PBLinTerm]
forall a. [a] -> [a] -> [a]
++ [(Integer
s2Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
c,Var
l) | (Integer
c,Var
l) <- [PBLinTerm]
lhs2], Integer
s1Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
rhs1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
s2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
rhs2)

cardinalityReduction :: PBLinAtLeast -> AtLeast
cardinalityReduction :: PBLinAtLeast -> AtLeast
cardinalityReduction ([PBLinTerm]
lhs,Integer
rhs) = (Clause
ls, Var
rhs')
  where
    rhs' :: Var
rhs' = Integer -> Var -> [PBLinTerm] -> Var
forall p b. Num p => Integer -> p -> [(Integer, b)] -> p
go1 Integer
0 Var
0 ((PBLinTerm -> PBLinTerm -> Ordering) -> [PBLinTerm] -> [PBLinTerm]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ((PBLinTerm -> PBLinTerm -> Ordering)
-> PBLinTerm -> PBLinTerm -> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((PBLinTerm -> Integer) -> PBLinTerm -> PBLinTerm -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing PBLinTerm -> Integer
forall a b. (a, b) -> a
fst)) [PBLinTerm]
lhs)

    go1 :: Integer -> p -> [(Integer, b)] -> p
go1 !Integer
s !p
k ((Integer
a,b
_):[(Integer, b)]
ts)
      | Integer
s Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
rhs   = Integer -> p -> [(Integer, b)] -> p
go1 (Integer
sInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
a) (p
kp -> p -> p
forall a. Num a => a -> a -> a
+p
1) [(Integer, b)]
ts
      | Bool
otherwise = p
k
    go1 Integer
_ p
_ [] = [Char] -> p
forall a. (?callStack::CallStack) => [Char] -> a
error [Char]
"ToySolver.SAT.Types.cardinalityReduction: should not happen"

    ls :: Clause
ls = Integer -> [PBLinTerm] -> Clause
forall a b. (Ord a, Num a) => a -> [(a, b)] -> [b]
go2 ([Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum (Integer
rhs Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: (PBLinTerm -> Integer) -> [PBLinTerm] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
subtract Integer
1 (Integer -> Integer)
-> (PBLinTerm -> Integer) -> PBLinTerm -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PBLinTerm -> Integer
forall a b. (a, b) -> a
fst) [PBLinTerm]
lhs)) ((PBLinTerm -> PBLinTerm -> Ordering) -> [PBLinTerm] -> [PBLinTerm]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ((PBLinTerm -> Integer) -> PBLinTerm -> PBLinTerm -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing PBLinTerm -> Integer
forall a b. (a, b) -> a
fst) [PBLinTerm]
lhs)

    go2 :: a -> [(a, b)] -> [b]
go2 !a
guard' ((a
a,b
_) : [(a, b)]
ts)
      | a
a a -> a -> a
forall a. Num a => a -> a -> a
- a
1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
guard' = a -> [(a, b)] -> [b]
go2 (a
guard' a -> a -> a
forall a. Num a => a -> a -> a
- a
a) [(a, b)]
ts
      | Bool
otherwise      = ((a, b) -> b) -> [(a, b)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (a, b) -> b
forall a b. (a, b) -> b
snd [(a, b)]
ts
    go2 a
_ [] = [Char] -> [b]
forall a. (?callStack::CallStack) => [Char] -> a
error [Char]
"ToySolver.SAT.Types.cardinalityReduction: should not happen"

negatePBLinAtLeast :: PBLinAtLeast -> PBLinAtLeast
negatePBLinAtLeast :: PBLinAtLeast -> PBLinAtLeast
negatePBLinAtLeast ([PBLinTerm]
xs, Integer
rhs) = ([(-Integer
c,Var
lit) | (Integer
c,Var
lit)<-[PBLinTerm]
xs] , -Integer
rhs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)

evalPBLinSum :: IModel m => m -> PBLinSum -> Integer
evalPBLinSum :: m -> [PBLinTerm] -> Integer
evalPBLinSum m
m [PBLinTerm]
xs = [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
c | (Integer
c,Var
lit) <- [PBLinTerm]
xs, m -> Var -> Bool
forall a. IModel a => a -> Var -> Bool
evalLit m
m Var
lit]

evalPBLinAtLeast :: IModel m => m -> PBLinAtLeast -> Bool
evalPBLinAtLeast :: m -> PBLinAtLeast -> Bool
evalPBLinAtLeast m
m ([PBLinTerm]
lhs,Integer
rhs) = m -> [PBLinTerm] -> Integer
forall m. IModel m => m -> [PBLinTerm] -> Integer
evalPBLinSum m
m [PBLinTerm]
lhs Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
rhs

evalPBLinExactly :: IModel m => m -> PBLinAtLeast -> Bool
evalPBLinExactly :: m -> PBLinAtLeast -> Bool
evalPBLinExactly m
m ([PBLinTerm]
lhs,Integer
rhs) = m -> [PBLinTerm] -> Integer
forall m. IModel m => m -> [PBLinTerm] -> Integer
evalPBLinSum m
m [PBLinTerm]
lhs Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
rhs

pbLinLowerBound :: PBLinSum -> Integer
pbLinLowerBound :: [PBLinTerm] -> Integer
pbLinLowerBound [PBLinTerm]
xs = [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [if Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 then Integer
c else Integer
0 | (Integer
c,Var
_) <- [PBLinTerm]
xs]

pbLinUpperBound :: PBLinSum -> Integer
pbLinUpperBound :: [PBLinTerm] -> Integer
pbLinUpperBound [PBLinTerm]
xs = [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [if Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 then Integer
c else Integer
0 | (Integer
c,Var
_) <- [PBLinTerm]
xs]

-- (Σi ci li ≥ rhs1) subsumes (Σi di li ≥ rhs2) iff rhs1≥rhs2 and di≥ci for all i.
pbLinSubsume :: PBLinAtLeast -> PBLinAtLeast -> Bool
pbLinSubsume :: PBLinAtLeast -> PBLinAtLeast -> Bool
pbLinSubsume ([PBLinTerm]
lhs1,Integer
rhs1) ([PBLinTerm]
lhs2,Integer
rhs2) =
  Integer
rhs1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
rhs2 Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Integer
di Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
ci | (Integer
ci,Var
li) <- [PBLinTerm]
lhs1, let di :: Integer
di = Integer -> Var -> VarMap Integer -> Integer
forall a. a -> Var -> IntMap a -> a
IntMap.findWithDefault Integer
0 Var
li VarMap Integer
lhs2']
  where
    lhs2' :: VarMap Integer
lhs2' = [(Var, Integer)] -> VarMap Integer
forall a. [(Var, a)] -> IntMap a
IntMap.fromList [(Var
l,Integer
c) | (Integer
c,Var
l) <- [PBLinTerm]
lhs2]

type PBTerm = (Integer, [Lit])
type PBSum = [PBTerm]

evalPBSum :: IModel m => m -> PBSum -> Integer
evalPBSum :: m -> PBSum -> Integer
evalPBSum m
m PBSum
xs = [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
c | (Integer
c,Clause
lits) <- PBSum
xs, (Var -> Bool) -> Clause -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (m -> Var -> Bool
forall a. IModel a => a -> Var -> Bool
evalLit m
m) Clause
lits]

evalPBConstraint :: IModel m => m -> PBFile.Constraint -> Bool
evalPBConstraint :: m -> Constraint -> Bool
evalPBConstraint m
m (PBSum
lhs,Op
op,Integer
rhs) = Integer -> Integer -> Bool
op' (m -> PBSum -> Integer
forall m. IModel m => m -> PBSum -> Integer
evalPBSum m
m PBSum
lhs) Integer
rhs
  where
    op' :: Integer -> Integer -> Bool
op' = case Op
op of
            Op
PBFile.Ge -> Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
(>=)
            Op
PBFile.Eq -> Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
(==)

evalPBFormula :: IModel m => m -> PBFile.Formula -> Maybe Integer
evalPBFormula :: m -> Formula -> Maybe Integer
evalPBFormula m
m Formula
formula = do
  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ (Constraint -> Bool) -> [Constraint] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (m -> Constraint -> Bool
forall m. IModel m => m -> Constraint -> Bool
evalPBConstraint m
m) ([Constraint] -> Bool) -> [Constraint] -> Bool
forall a b. (a -> b) -> a -> b
$ Formula -> [Constraint]
PBFile.pbConstraints Formula
formula
  Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ m -> PBSum -> Integer
forall m. IModel m => m -> PBSum -> Integer
evalPBSum m
m (PBSum -> Integer) -> PBSum -> Integer
forall a b. (a -> b) -> a -> b
$ PBSum -> Maybe PBSum -> PBSum
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe PBSum -> PBSum) -> Maybe PBSum -> PBSum
forall a b. (a -> b) -> a -> b
$ Formula -> Maybe PBSum
PBFile.pbObjectiveFunction Formula
formula

pbLowerBound :: PBSum -> Integer
pbLowerBound :: PBSum -> Integer
pbLowerBound PBSum
xs = [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
c | (Integer
c,Clause
ls) <- PBSum
xs, Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 Bool -> Bool -> Bool
|| Clause -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Clause
ls]

pbUpperBound :: PBSum -> Integer
pbUpperBound :: PBSum -> Integer
pbUpperBound PBSum
xs = [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
c | (Integer
c,Clause
ls) <- PBSum
xs, Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 Bool -> Bool -> Bool
|| Clause -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Clause
ls]

removeNegationFromPBSum :: PBSum -> PBSum
removeNegationFromPBSum :: PBSum -> PBSum
removeNegationFromPBSum PBSum
ts =
  [(Integer
c, IntSet -> Clause
IntSet.toList IntSet
m) | (IntSet
m, Integer
c) <- Map IntSet Integer -> [(IntSet, Integer)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map IntSet Integer -> [(IntSet, Integer)])
-> Map IntSet Integer -> [(IntSet, Integer)]
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer)
-> [Map IntSet Integer] -> Map IntSet Integer
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) ([Map IntSet Integer] -> Map IntSet Integer)
-> [Map IntSet Integer] -> Map IntSet Integer
forall a b. (a -> b) -> a -> b
$ ((Integer, Clause) -> Map IntSet Integer)
-> PBSum -> [Map IntSet Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, Clause) -> Map IntSet Integer
f PBSum
ts, Integer
c Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0]
  where
    f :: PBTerm -> Map VarSet Integer
    f :: (Integer, Clause) -> Map IntSet Integer
f (Integer
c, Clause
ls) = (Map IntSet Integer -> Var -> Map IntSet Integer)
-> Map IntSet Integer -> IntSet -> Map IntSet Integer
forall a. (a -> Var -> a) -> a -> IntSet -> a
IntSet.foldl' Map IntSet Integer -> Var -> Map IntSet Integer
g (IntSet -> Integer -> Map IntSet Integer
forall k a. k -> a -> Map k a
Map.singleton IntSet
IntSet.empty Integer
c) (Clause -> IntSet
IntSet.fromList Clause
ls)

    g :: Map VarSet Integer -> Lit -> Map VarSet Integer
    g :: Map IntSet Integer -> Var -> Map IntSet Integer
g Map IntSet Integer
m Var
l
      | Var
l Var -> Var -> Bool
forall a. Ord a => a -> a -> Bool
> Var
0     = (Integer -> Integer -> Integer)
-> (IntSet -> IntSet) -> Map IntSet Integer -> Map IntSet Integer
forall k2 a k1.
Ord k2 =>
(a -> a -> a) -> (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeysWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) (Var -> IntSet -> IntSet
IntSet.insert Var
v) Map IntSet Integer
m
      | Bool
otherwise = (Integer -> Integer -> Integer)
-> Map IntSet Integer -> Map IntSet Integer -> Map IntSet Integer
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) Map IntSet Integer
m (Map IntSet Integer -> Map IntSet Integer)
-> Map IntSet Integer -> Map IntSet Integer
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer)
-> [(IntSet, Integer)] -> Map IntSet Integer
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) [(Var -> IntSet -> IntSet
IntSet.insert Var
v IntSet
xs, Integer -> Integer
forall a. Num a => a -> a
negate Integer
c) | (IntSet
xs,Integer
c) <- Map IntSet Integer -> [(IntSet, Integer)]
forall k a. Map k a -> [(k, a)]
Map.toList Map IntSet Integer
m]
      where
        v :: Var
v = Var -> Var
litVar Var
l

-- | XOR clause
--
-- '([l1,l2..ln], b)' means l1 ⊕ l2 ⊕ ⋯ ⊕ ln = b.
--
-- Note that:
--
-- * True can be represented as ([], False)
--
-- * False can be represented as ([], True)
--
type XORClause = ([Lit], Bool)

-- | Normalize XOR clause
normalizeXORClause :: XORClause -> XORClause
normalizeXORClause :: XORClause -> XORClause
normalizeXORClause (Clause
lits, Bool
b) =
  case IntMap Bool -> Clause
forall a. IntMap a -> Clause
IntMap.keys IntMap Bool
m of
    Var
0:Clause
xs -> (Clause
xs, Bool -> Bool
not Bool
b)
    Clause
xs -> (Clause
xs, Bool
b)
  where
    m :: IntMap Bool
m = (Bool -> Bool) -> IntMap Bool -> IntMap Bool
forall a. (a -> Bool) -> IntMap a -> IntMap a
IntMap.filter Bool -> Bool
forall a. a -> a
id (IntMap Bool -> IntMap Bool) -> IntMap Bool -> IntMap Bool
forall a b. (a -> b) -> a -> b
$ (Bool -> Bool -> Bool) -> [IntMap Bool] -> IntMap Bool
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> f (IntMap a) -> IntMap a
IntMap.unionsWith Bool -> Bool -> Bool
xor [Var -> IntMap Bool
f Var
lit | Var
lit <- Clause
lits]
    xor :: Bool -> Bool -> Bool
xor = Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(/=)

    f :: Var -> IntMap Bool
f Var
0 = Var -> Bool -> IntMap Bool
forall a. Var -> a -> IntMap a
IntMap.singleton Var
0 Bool
True
    f Var
lit =
      if Var -> Bool
litPolarity Var
lit
      then Var -> Bool -> IntMap Bool
forall a. Var -> a -> IntMap a
IntMap.singleton Var
lit Bool
True
      else [(Var, Bool)] -> IntMap Bool
forall a. [(Var, a)] -> IntMap a
IntMap.fromList [(Var -> Var
litVar Var
lit, Bool
True), (Var
0, Bool
True)]  -- ¬x = x ⊕ 1

{-# SPECIALIZE instantiateXORClause :: (Lit -> IO LBool) -> XORClause -> IO XORClause #-}
instantiateXORClause :: forall m. Monad m => (Lit -> m LBool) -> XORClause -> m XORClause
instantiateXORClause :: (Var -> m LBool) -> XORClause -> m XORClause
instantiateXORClause Var -> m LBool
evalLitM (Clause
ls,Bool
b) = Clause -> Bool -> Clause -> m XORClause
loop [] Bool
b Clause
ls
  where
    loop :: [Lit] -> Bool -> [Lit] -> m XORClause
    loop :: Clause -> Bool -> Clause -> m XORClause
loop Clause
lhs !Bool
rhs [] = XORClause -> m XORClause
forall (m :: * -> *) a. Monad m => a -> m a
return (Clause
lhs, Bool
rhs)
    loop Clause
lhs !Bool
rhs (Var
l:Clause
ls) = do
      LBool
val <- Var -> m LBool
evalLitM Var
l
      if LBool
valLBool -> LBool -> Bool
forall a. Eq a => a -> a -> Bool
==LBool
lTrue then
        Clause -> Bool -> Clause -> m XORClause
loop Clause
lhs (Bool -> Bool
not Bool
rhs) Clause
ls
      else if LBool
valLBool -> LBool -> Bool
forall a. Eq a => a -> a -> Bool
==LBool
lFalse then
        Clause -> Bool -> Clause -> m XORClause
loop Clause
lhs Bool
rhs Clause
ls
      else
        Clause -> Bool -> Clause -> m XORClause
loop (Var
l Var -> Clause -> Clause
forall a. a -> [a] -> [a]
: Clause
lhs) Bool
rhs Clause
ls

evalXORClause :: IModel m => m -> XORClause -> Bool
evalXORClause :: m -> XORClause -> Bool
evalXORClause m
m (Clause
lits, Bool
rhs) = (Bool -> Bool -> Bool) -> Bool -> [Bool] -> Bool
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Bool -> Bool -> Bool
xor Bool
False ((Var -> Bool) -> Clause -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map Var -> Bool
f Clause
lits) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
rhs
  where
    xor :: Bool -> Bool -> Bool
xor = Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(/=)
    f :: Var -> Bool
f Var
0 = Bool
True
    f Var
lit = m -> Var -> Bool
forall a. IModel a => a -> Var -> Bool
evalLit m
m Var
lit


class Monad m => NewVar m a | a -> m where
  {-# MINIMAL newVar #-}

  -- | Add a new variable
  newVar :: a -> m Var

  -- | Add variables. @newVars a n = replicateM n (newVar a)@, but maybe faster.
  newVars :: a -> Int -> m [Var]
  newVars a
a Var
n = Var -> m Var -> m Clause
forall (m :: * -> *) a. Applicative m => Var -> m a -> m [a]
replicateM Var
n (a -> m Var
forall (m :: * -> *) a. NewVar m a => a -> m Var
newVar a
a)

  -- | Add variables. @newVars_ a n = newVars a n >> return ()@, but maybe faster.
  newVars_ :: a -> Int -> m ()
  newVars_ a
a Var
n = Var -> m Var -> m ()
forall (m :: * -> *) a. Applicative m => Var -> m a -> m ()
replicateM_ Var
n (a -> m Var
forall (m :: * -> *) a. NewVar m a => a -> m Var
newVar a
a)

class NewVar m a => AddClause m a | a -> m where
  addClause :: a -> Clause -> m ()

class AddClause m a => AddCardinality m a | a -> m where
  {-# MINIMAL addAtLeast #-}

  -- | Add a cardinality constraints /atleast({l1,l2,..},n)/.
  addAtLeast
    :: a
    -> [Lit] -- ^ set of literals /{l1,l2,..}/ (duplicated elements are ignored)
    -> Int   -- ^ /n/
    -> m ()

  -- | Add a cardinality constraints /atmost({l1,l2,..},n)/.
  addAtMost
    :: a
    -> [Lit] -- ^ set of literals /{l1,l2,..}/ (duplicated elements are ignored)
    -> Int   -- ^ /n/
    -> m ()
  addAtMost a
a Clause
lits Var
n = do
    a -> Clause -> Var -> m ()
forall (m :: * -> *) a.
AddCardinality m a =>
a -> Clause -> Var -> m ()
addAtLeast a
a ((Var -> Var) -> Clause -> Clause
forall a b. (a -> b) -> [a] -> [b]
map Var -> Var
litNot Clause
lits) (Clause -> Var
forall (t :: * -> *) a. Foldable t => t a -> Var
length Clause
lits Var -> Var -> Var
forall a. Num a => a -> a -> a
- Var
n)

  -- | Add a cardinality constraints /exactly({l1,l2,..},n)/.
  addExactly
    :: a
    -> [Lit] -- ^ set of literals /{l1,l2,..}/ (duplicated elements are ignored)
    -> Int   -- ^ /n/
    -> m ()
  addExactly a
a Clause
lits Var
n = do
    a -> Clause -> Var -> m ()
forall (m :: * -> *) a.
AddCardinality m a =>
a -> Clause -> Var -> m ()
addAtLeast a
a Clause
lits Var
n
    a -> Clause -> Var -> m ()
forall (m :: * -> *) a.
AddCardinality m a =>
a -> Clause -> Var -> m ()
addAtMost a
a Clause
lits Var
n

class AddCardinality m a => AddPBLin m a | a -> m where
  {-# MINIMAL addPBAtLeast #-}

  -- | Add a pseudo boolean constraints /c1*l1 + c2*l2 + … ≥ n/.
  addPBAtLeast
    :: a
    -> PBLinSum -- ^ list of terms @[(c1,l1),(c2,l2),…]@
    -> Integer  -- ^ /n/
    -> m ()

  -- | Add a pseudo boolean constraints /c1*l1 + c2*l2 + … ≤ n/.
  addPBAtMost
    :: a
    -> PBLinSum -- ^ list of @[(c1,l1),(c2,l2),…]@
    -> Integer  -- ^ /n/
    -> m ()
  addPBAtMost a
a [PBLinTerm]
ts Integer
n = a -> [PBLinTerm] -> Integer -> m ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> [PBLinTerm] -> Integer -> m ()
addPBAtLeast a
a [(-Integer
c,Var
l) | (Integer
c,Var
l) <- [PBLinTerm]
ts] (Integer -> Integer
forall a. Num a => a -> a
negate Integer
n)

  -- | Add a pseudo boolean constraints /c1*l1 + c2*l2 + … = n/.
  addPBExactly
    :: a
    -> PBLinSum -- ^ list of terms @[(c1,l1),(c2,l2),…]@
    -> Integer  -- ^ /n/
    -> m ()
  addPBExactly a
a [PBLinTerm]
ts Integer
n = do
    a -> [PBLinTerm] -> Integer -> m ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> [PBLinTerm] -> Integer -> m ()
addPBAtLeast a
a [PBLinTerm]
ts Integer
n
    a -> [PBLinTerm] -> Integer -> m ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> [PBLinTerm] -> Integer -> m ()
addPBAtMost a
a [PBLinTerm]
ts Integer
n

  -- | Add a soft pseudo boolean constraints /sel ⇒ c1*l1 + c2*l2 + … ≥ n/.
  addPBAtLeastSoft
    :: a
    -> Lit             -- ^ Selector literal @sel@
    -> PBLinSum        -- ^ list of terms @[(c1,l1),(c2,l2),…]@
    -> Integer         -- ^ /n/
    -> m ()
  addPBAtLeastSoft a
a Var
sel [PBLinTerm]
lhs Integer
rhs = do
    let ([PBLinTerm]
lhs2,Integer
rhs2) = PBLinAtLeast -> PBLinAtLeast
normalizePBLinAtLeast ([PBLinTerm]
lhs,Integer
rhs)
    a -> [PBLinTerm] -> Integer -> m ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> [PBLinTerm] -> Integer -> m ()
addPBAtLeast a
a ((Integer
rhs2, Var -> Var
litNot Var
sel) PBLinTerm -> [PBLinTerm] -> [PBLinTerm]
forall a. a -> [a] -> [a]
: [PBLinTerm]
lhs2) Integer
rhs2

  -- | Add a soft pseudo boolean constraints /sel ⇒ c1*l1 + c2*l2 + … ≤ n/.
  addPBAtMostSoft
    :: a
    -> Lit             -- ^ Selector literal @sel@
    -> PBLinSum        -- ^ list of terms @[(c1,l1),(c2,l2),…]@
    -> Integer         -- ^ /n/
    -> m ()
  addPBAtMostSoft a
a Var
sel [PBLinTerm]
lhs Integer
rhs =
    a -> Var -> [PBLinTerm] -> Integer -> m ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> Var -> [PBLinTerm] -> Integer -> m ()
addPBAtLeastSoft a
a Var
sel [(Integer -> Integer
forall a. Num a => a -> a
negate Integer
c, Var
lit) | (Integer
c,Var
lit) <- [PBLinTerm]
lhs] (Integer -> Integer
forall a. Num a => a -> a
negate Integer
rhs)

  -- | Add a soft pseudo boolean constraints /sel ⇒ c1*l1 + c2*l2 + … = n/.
  addPBExactlySoft
    :: a
    -> Lit             -- ^ Selector literal @sel@
    -> PBLinSum        -- ^ list of terms @[(c1,l1),(c2,l2),…]@
    -> Integer         -- ^ /n/
    -> m ()
  addPBExactlySoft a
a Var
sel [PBLinTerm]
lhs Integer
rhs = do
    a -> Var -> [PBLinTerm] -> Integer -> m ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> Var -> [PBLinTerm] -> Integer -> m ()
addPBAtLeastSoft a
a Var
sel [PBLinTerm]
lhs Integer
rhs
    a -> Var -> [PBLinTerm] -> Integer -> m ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> Var -> [PBLinTerm] -> Integer -> m ()
addPBAtMostSoft a
a Var
sel [PBLinTerm]
lhs Integer
rhs

class AddPBLin m a => AddPBNL m a | a -> m where
  {-# MINIMAL addPBNLAtLeast #-}

  -- | Add a non-linear pseudo boolean constraints /c1*ls1 + c2*ls2 + … ≥ n/.
  addPBNLAtLeast
    :: a
    -> PBSum   -- ^ List of terms @[(c1,ls1),(c2,ls2),…]@
    -> Integer -- ^ /n/
    -> m ()

  -- | Add a non-linear pseudo boolean constraints /c1*ls1 + c2*ls2 + … ≥ n/.
  addPBNLAtMost
    :: a
    -> PBSum   -- ^ List of terms @[(c1,ls1),(c2,ls2),…]@
    -> Integer -- ^ /n/
    -> m ()
  addPBNLAtMost a
a PBSum
ts Integer
n = a -> PBSum -> Integer -> m ()
forall (m :: * -> *) a.
AddPBNL m a =>
a -> PBSum -> Integer -> m ()
addPBNLAtLeast a
a [(-Integer
c,Clause
ls) | (Integer
c,Clause
ls) <- PBSum
ts] (Integer -> Integer
forall a. Num a => a -> a
negate Integer
n)

  -- | Add a non-linear pseudo boolean constraints /c1*ls1 + c2*ls2 + … = n/.
  addPBNLExactly
    :: a
    -> PBSum   -- ^ List of terms @[(c1,ls1),(c2,ls2),…]@
    -> Integer -- ^ /n/
    -> m ()
  addPBNLExactly a
a PBSum
ts Integer
n = do
    a -> PBSum -> Integer -> m ()
forall (m :: * -> *) a.
AddPBNL m a =>
a -> PBSum -> Integer -> m ()
addPBNLAtLeast a
a PBSum
ts Integer
n
    a -> PBSum -> Integer -> m ()
forall (m :: * -> *) a.
AddPBNL m a =>
a -> PBSum -> Integer -> m ()
addPBNLAtMost a
a PBSum
ts Integer
n

  -- | Add a soft non-linear pseudo boolean constraints /sel ⇒ c1*ls1 + c2*ls2 + … ≥ n/.
  addPBNLAtLeastSoft
    :: a
    -> Lit     -- ^ Selector literal @sel@
    -> PBSum   -- ^ List of terms @[(c1,ls1),(c2,ls2),…]@
    -> Integer -- ^ /n/
    -> m ()
  addPBNLAtLeastSoft a
a Var
sel PBSum
lhs Integer
rhs = do
    let n :: Integer
n = Integer
rhs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
c Integer
0 | (Integer
c,Clause
_) <- PBSum
lhs]
    a -> PBSum -> Integer -> m ()
forall (m :: * -> *) a.
AddPBNL m a =>
a -> PBSum -> Integer -> m ()
addPBNLAtLeast a
a ((Integer
n, [Var -> Var
litNot Var
sel]) (Integer, Clause) -> PBSum -> PBSum
forall a. a -> [a] -> [a]
: PBSum
lhs) Integer
rhs

  -- | Add a soft non-linear pseudo boolean constraints /sel ⇒ c1*ls1 + c2*ls2 + … ≤ n/.
  addPBNLAtMostSoft
    :: a
    -> Lit     -- ^ Selector literal @sel@
    -> PBSum   -- ^ List of terms @[(c1,ls1),(c2,ls2),…]@
    -> Integer -- ^ /n/
    -> m ()
  addPBNLAtMostSoft a
a Var
sel PBSum
lhs Integer
rhs =
    a -> Var -> PBSum -> Integer -> m ()
forall (m :: * -> *) a.
AddPBNL m a =>
a -> Var -> PBSum -> Integer -> m ()
addPBNLAtLeastSoft a
a Var
sel [(Integer -> Integer
forall a. Num a => a -> a
negate Integer
c, Clause
ls) | (Integer
c,Clause
ls) <- PBSum
lhs] (Integer -> Integer
forall a. Num a => a -> a
negate Integer
rhs)

  -- | Add a soft non-linear pseudo boolean constraints /lit ⇒ c1*ls1 + c2*ls2 + … = n/.
  addPBNLExactlySoft
    :: a
    -> Lit     -- ^ Selector literal @sel@
    -> PBSum   -- ^ List of terms @[(c1,ls1),(c2,ls2),…]@
    -> Integer -- ^ /n/
    -> m ()
  addPBNLExactlySoft a
a Var
sel PBSum
lhs Integer
rhs = do
    a -> Var -> PBSum -> Integer -> m ()
forall (m :: * -> *) a.
AddPBNL m a =>
a -> Var -> PBSum -> Integer -> m ()
addPBNLAtLeastSoft a
a Var
sel PBSum
lhs Integer
rhs
    a -> Var -> PBSum -> Integer -> m ()
forall (m :: * -> *) a.
AddPBNL m a =>
a -> Var -> PBSum -> Integer -> m ()
addPBNLAtMostSoft a
a Var
sel PBSum
lhs Integer
rhs

class AddClause m a => AddXORClause m a | a -> m where
  {-# MINIMAL addXORClause #-}

  -- | Add a parity constraint /l1 ⊕ l2 ⊕ … ⊕ ln = rhs/
  addXORClause
    :: a
    -> [Lit]  -- ^ literals @[l1, l2, …, ln]@
    -> Bool   -- ^ /rhs/
    -> m ()

  -- | Add a soft parity constraint /sel ⇒ l1 ⊕ l2 ⊕ … ⊕ ln = rhs/
  addXORClauseSoft
    :: a
    -> Lit    -- ^ Selector literal @sel@
    -> [Lit]  -- ^ literals @[l1, l2, …, ln]@
    -> Bool   -- ^ /rhs/
    -> m ()
  addXORClauseSoft a
a Var
sel Clause
lits Bool
rhs = do
    Var
reified <- a -> m Var
forall (m :: * -> *) a. NewVar m a => a -> m Var
newVar a
a
    a -> Clause -> Bool -> m ()
forall (m :: * -> *) a.
AddXORClause m a =>
a -> Clause -> Bool -> m ()
addXORClause a
a (Var -> Var
litNot Var
reified Var -> Clause -> Clause
forall a. a -> [a] -> [a]
: Clause
lits) Bool
rhs
    a -> Clause -> m ()
forall (m :: * -> *) a. AddClause m a => a -> Clause -> m ()
addClause a
a [Var -> Var
litNot Var
sel, Var
reified] -- sel ⇒ reified