{-# 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
  , evalPBSoftFormula
  , pbLowerBound
  , pbUpperBound
  , removeNegationFromPBSum

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

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

  -- * Type-2 SOS constraints
  , addSOS2
  , evalSOS2
  ) 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 :: Lit -> Bool
validVar Lit
v = Lit
v Lit -> Lit -> Bool
forall a. Ord a => a -> a -> Bool
> Lit
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 :: Lit -> Model -> Model
restrictModel Lit
nv Model
m = (Lit, Lit) -> [(Lit, Bool)] -> Model
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Lit
1,Lit
nv) [(Lit
v, Model
m Model -> Lit -> Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Lit
v) | Lit
v <- [Lit
1..Lit
nv]]

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

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

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

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

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

type LitSet = IntSet
type LitMap = IntMap

{-# INLINE validLit #-}
validLit :: Lit -> Bool
validLit :: Lit -> Bool
validLit Lit
l = Lit
l Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
/= Lit
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 :: Lit -> Bool -> Lit
literal Lit
v Bool
polarity =
  Bool -> Lit -> Lit
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Lit -> Bool
validVar Lit
v) (Lit -> Lit) -> Lit -> Lit
forall a b. (a -> b) -> a -> b
$ if Bool
polarity then Lit
v else Lit -> Lit
litNot Lit
v

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

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

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

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

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

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

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

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

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

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

type PackedVar = PackedLit
type PackedLit = Int32

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

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

type PackedClause = VU.Vector PackedLit

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

unpackClause :: PackedClause -> Clause
unpackClause :: PackedClause -> [Lit]
unpackClause = (PackedLit -> Lit) -> [PackedLit] -> [Lit]
forall a b. (a -> b) -> [a] -> [b]
map PackedLit -> Lit
unpackLit ([PackedLit] -> [Lit])
-> (PackedClause -> [PackedLit]) -> PackedClause -> [Lit]
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 ([Lit]
lits,Lit
n) = Bool -> AtLeast -> AtLeast
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (VarSet -> Lit
IntSet.size VarSet
ys Lit -> Lit -> Lit
forall a. Integral a => a -> a -> a
`mod` Lit
2 Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
== Lit
0) (AtLeast -> AtLeast) -> AtLeast -> AtLeast
forall a b. (a -> b) -> a -> b
$
   (VarSet -> [Lit]
IntSet.toList VarSet
lits', Lit
n')
   where
     xs :: VarSet
xs = [Lit] -> VarSet
IntSet.fromList [Lit]
lits
     ys :: VarSet
ys = VarSet
xs VarSet -> VarSet -> VarSet
`IntSet.intersection` ((Lit -> Lit) -> VarSet -> VarSet
IntSet.map Lit -> Lit
litNot VarSet
xs)
     lits' :: VarSet
lits' = VarSet
xs VarSet -> VarSet -> VarSet
`IntSet.difference` VarSet
ys
     n' :: Lit
n' = Lit
n Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
- (VarSet -> Lit
IntSet.size VarSet
ys Lit -> Lit -> Lit
forall a. Integral a => a -> a -> a
`div` Lit
2)

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

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

evalExactly :: IModel m => m -> Exactly -> Bool
evalExactly :: forall m. IModel m => m -> AtLeast -> Bool
evalExactly m
m ([Lit]
lits,Lit
n) = [Lit] -> Lit
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Lit
1 | Lit
lit <- [Lit]
lits, m -> Lit -> Bool
forall m. IModel m => m -> Lit -> Bool
evalLit m
m Lit
lit] Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
== Lit
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,Lit
v) | (Lit
v,Integer
c) <- VarMap Integer -> [(Lit, Integer)]
forall a. IntMap a -> [(Lit, 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,Lit
l):[PBLinTerm]
zs) =
          if Lit -> Bool
litPolarity Lit
l
            then (VarMap Integer, Integer)
-> [PBLinTerm] -> (VarMap Integer, Integer)
loop ((Integer -> Integer -> Integer)
-> Lit -> Integer -> VarMap Integer -> VarMap Integer
forall a. (a -> a -> a) -> Lit -> a -> IntMap a -> IntMap a
IntMap.insertWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) Lit
l Integer
c VarMap Integer
ys, Integer
m) [PBLinTerm]
zs
            else (VarMap Integer, Integer)
-> [PBLinTerm] -> (VarMap Integer, Integer)
loop ((Integer -> Integer -> Integer)
-> Lit -> Integer -> VarMap Integer -> VarMap Integer
forall a. (a -> a -> a) -> Lit -> a -> IntMap a -> IntMap a
IntMap.insertWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) (Lit -> Lit
litNot Lit
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 {b}.
(Num b, Ord b) =>
([(b, Lit)], b) -> [(b, Lit)] -> ([(b, Lit)], b)
loop ([],Integer
n) [PBLinTerm]
xs
      where
        loop :: ([(b, Lit)], b) -> [(b, Lit)] -> ([(b, Lit)], b)
loop ([(b, Lit)]
ys,b
m) [] = ([(b, Lit)]
ys,b
m)
        loop ([(b, Lit)]
ys,b
m) (t :: (b, Lit)
t@(b
c,Lit
l):[(b, Lit)]
zs)
          | b
c b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
0 = ([(b, Lit)], b) -> [(b, Lit)] -> ([(b, Lit)], b)
loop ([(b, Lit)]
ys,b
m) [(b, Lit)]
zs
          | b
c b -> b -> Bool
forall a. Ord a => a -> a -> Bool
< b
0  = ([(b, Lit)], b) -> [(b, Lit)] -> ([(b, Lit)], b)
loop ((b -> b
forall a. Num a => a -> a
negate b
c,Lit -> Lit
litNot Lit
l)(b, Lit) -> [(b, Lit)] -> [(b, Lit)]
forall a. a -> [a] -> [a]
:[(b, Lit)]
ys, b
mb -> b -> b
forall a. Num a => a -> a -> a
+b
c) [(b, Lit)]
zs
          | Bool
otherwise = ([(b, Lit)], b) -> [(b, Lit)] -> ([(b, Lit)], b)
loop ((b, Lit)
t(b, Lit) -> [(b, Lit)] -> [(b, Lit)]
forall a. a -> [a] -> [a]
:[(b, Lit)]
ys,b
m) [(b, Lit)]
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,Lit
_) <- [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,Lit
l) | (Integer
c,Lit
l) <- [PBLinTerm]
xs], Integer
1)
        [Integer]
cs ->
          let d :: Integer
d = (Integer -> Integer -> Integer) -> [Integer] -> Integer
forall a. (?callStack::CallStack) => (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, Lit
l) | (Integer
c,Lit
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,Lit
_) <- [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, Lit
l) | (Integer
c,Lit
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. (?callStack::CallStack) => (a -> a -> a) -> [a] -> a
foldl1' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
gcd [Integer
c | (Integer
c,Lit
_) <- [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,Lit
_) <- [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 :: forall (m :: * -> *).
Monad m =>
(Lit -> m LBool) -> PBLinAtLeast -> m PBLinAtLeast
instantiatePBLinAtLeast Lit -> 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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return PBLinAtLeast
ret
    loop ([PBLinTerm]
ys,Integer
m) ((Integer
c,Lit
l):[PBLinTerm]
ts) = do
      LBool
val <- Lit -> m LBool
evalLitM Lit
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,Lit
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 :: forall (m :: * -> *).
Monad m =>
(Lit -> m LBool) -> PBLinAtLeast -> m PBLinAtLeast
instantiatePBLinExactly = (Lit -> m LBool) -> PBLinAtLeast -> m PBLinAtLeast
forall (m :: * -> *).
Monad m =>
(Lit -> m LBool) -> PBLinAtLeast -> m PBLinAtLeast
instantiatePBLinAtLeast

cutResolve :: PBLinAtLeast -> PBLinAtLeast -> Var -> PBLinAtLeast
cutResolve :: PBLinAtLeast -> PBLinAtLeast -> Lit -> PBLinAtLeast
cutResolve ([PBLinTerm]
lhs1,Integer
rhs1) ([PBLinTerm]
lhs2,Integer
rhs2) Lit
v = Bool -> PBLinAtLeast -> PBLinAtLeast
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Lit
l1 Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
== Lit -> Lit
litNot Lit
l2) (PBLinAtLeast -> PBLinAtLeast) -> PBLinAtLeast -> PBLinAtLeast
forall a b. (a -> b) -> a -> b
$ PBLinAtLeast -> PBLinAtLeast
normalizePBLinAtLeast PBLinAtLeast
pb
  where
    (Integer
c1,Lit
l1) = [PBLinTerm] -> PBLinTerm
forall a. (?callStack::CallStack) => [a] -> a
head [(Integer
c,Lit
l) | (Integer
c,Lit
l) <- [PBLinTerm]
lhs1, Lit -> Lit
litVar Lit
l Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
== Lit
v]
    (Integer
c2,Lit
l2) = [PBLinTerm] -> PBLinTerm
forall a. (?callStack::CallStack) => [a] -> a
head [(Integer
c,Lit
l) | (Integer
c,Lit
l) <- [PBLinTerm]
lhs2, Lit -> Lit
litVar Lit
l Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
== Lit
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,Lit
l) | (Integer
c,Lit
l) <- [PBLinTerm]
lhs1] [PBLinTerm] -> [PBLinTerm] -> [PBLinTerm]
forall a. [a] -> [a] -> [a]
++ [(Integer
s2Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
c,Lit
l) | (Integer
c,Lit
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) = ([Lit]
ls, Lit
rhs')
  where
    rhs' :: Lit
rhs' = Integer -> Lit -> [PBLinTerm] -> Lit
forall {t} {b}. Num t => Integer -> t -> [(Integer, b)] -> t
go1 Integer
0 Lit
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 -> t -> [(Integer, b)] -> t
go1 !Integer
s !t
k ((Integer
a,b
_):[(Integer, b)]
ts)
      | Integer
s Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
rhs   = Integer -> t -> [(Integer, b)] -> t
go1 (Integer
sInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
a) (t
kt -> t -> t
forall a. Num a => a -> a -> a
+t
1) [(Integer, b)]
ts
      | Bool
otherwise = t
k
    go1 Integer
_ t
_ [] = [Char] -> t
forall a. (?callStack::CallStack) => [Char] -> a
error [Char]
"ToySolver.SAT.Types.cardinalityReduction: should not happen"

    ls :: [Lit]
ls = Integer -> [PBLinTerm] -> [Lit]
forall {a} {b}. (Ord a, Num a) => a -> [(a, b)] -> [b]
go2 ([Integer] -> Integer
forall a. Ord a => [a] -> a
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,Lit
lit) | (Integer
c,Lit
lit)<-[PBLinTerm]
xs] , -Integer
rhs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)

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

evalPBLinAtLeast :: IModel m => m -> PBLinAtLeast -> Bool
evalPBLinAtLeast :: forall m. IModel m => 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 :: forall m. IModel m => 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 a. Num a => [a] -> a
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,Lit
_) <- [PBLinTerm]
xs]

pbLinUpperBound :: PBLinSum -> Integer
pbLinUpperBound :: [PBLinTerm] -> Integer
pbLinUpperBound [PBLinTerm]
xs = [Integer] -> Integer
forall a. Num a => [a] -> a
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,Lit
_) <- [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,Lit
li) <- [PBLinTerm]
lhs1, let di :: Integer
di = Integer -> Lit -> VarMap Integer -> Integer
forall a. a -> Lit -> IntMap a -> a
IntMap.findWithDefault Integer
0 Lit
li VarMap Integer
lhs2']
  where
    lhs2' :: VarMap Integer
lhs2' = [(Lit, Integer)] -> VarMap Integer
forall a. [(Lit, a)] -> IntMap a
IntMap.fromList [(Lit
l,Integer
c) | (Integer
c,Lit
l) <- [PBLinTerm]
lhs2]

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

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

evalPBConstraint :: IModel m => m -> PBFile.Constraint -> Bool
evalPBConstraint :: forall m. IModel m => 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 :: forall m. IModel m => 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 a. a -> Maybe a
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

evalPBSoftFormula :: IModel m => m -> PBFile.SoftFormula -> Maybe Integer
evalPBSoftFormula :: forall m. IModel m => m -> SoftFormula -> Maybe Integer
evalPBSoftFormula m
m SoftFormula
formula = do
  Integer
obj <- ([Integer] -> Integer) -> Maybe [Integer] -> Maybe Integer
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Integer] -> Integer
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (Maybe [Integer] -> Maybe Integer)
-> Maybe [Integer] -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ [SoftConstraint]
-> (SoftConstraint -> Maybe Integer) -> Maybe [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (SoftFormula -> [SoftConstraint]
PBFile.wboConstraints SoftFormula
formula) ((SoftConstraint -> Maybe Integer) -> Maybe [Integer])
-> (SoftConstraint -> Maybe Integer) -> Maybe [Integer]
forall a b. (a -> b) -> a -> b
$ \(Maybe Integer
cost, Constraint
constr) -> do
    case Maybe Integer
cost of
      Maybe Integer
Nothing -> do
        Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ m -> Constraint -> Bool
forall m. IModel m => m -> Constraint -> Bool
evalPBConstraint m
m Constraint
constr
        Integer -> Maybe Integer
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
0
      Just Integer
w
        | m -> Constraint -> Bool
forall m. IModel m => m -> Constraint -> Bool
evalPBConstraint m
m Constraint
constr -> Integer -> Maybe Integer
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
0
        | Bool
otherwise -> Integer -> Maybe Integer
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
w
  case SoftFormula -> Maybe Integer
PBFile.wboTopCost SoftFormula
formula of
    Maybe Integer
Nothing -> () -> Maybe ()
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just Integer
c -> Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
obj Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
c)
  Integer -> Maybe Integer
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
obj

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

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

removeNegationFromPBSum :: PBSum -> PBSum
removeNegationFromPBSum :: PBSum -> PBSum
removeNegationFromPBSum PBSum
ts =
  [(Integer
c, VarSet -> [Lit]
IntSet.toList VarSet
m) | (VarSet
m, Integer
c) <- Map VarSet Integer -> [(VarSet, Integer)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map VarSet Integer -> [(VarSet, Integer)])
-> Map VarSet Integer -> [(VarSet, Integer)]
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer)
-> [Map VarSet Integer] -> Map VarSet 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 VarSet Integer] -> Map VarSet Integer)
-> [Map VarSet Integer] -> Map VarSet Integer
forall a b. (a -> b) -> a -> b
$ ((Integer, [Lit]) -> Map VarSet Integer)
-> PBSum -> [Map VarSet Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, [Lit]) -> Map VarSet 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, [Lit]) -> Map VarSet Integer
f (Integer
c, [Lit]
ls) = (Map VarSet Integer -> Lit -> Map VarSet Integer)
-> Map VarSet Integer -> VarSet -> Map VarSet Integer
forall a. (a -> Lit -> a) -> a -> VarSet -> a
IntSet.foldl' Map VarSet Integer -> Lit -> Map VarSet Integer
g (VarSet -> Integer -> Map VarSet Integer
forall k a. k -> a -> Map k a
Map.singleton VarSet
IntSet.empty Integer
c) ([Lit] -> VarSet
IntSet.fromList [Lit]
ls)

    g :: Map VarSet Integer -> Lit -> Map VarSet Integer
    g :: Map VarSet Integer -> Lit -> Map VarSet Integer
g Map VarSet Integer
m Lit
l
      | Lit
l Lit -> Lit -> Bool
forall a. Ord a => a -> a -> Bool
> Lit
0     = (Integer -> Integer -> Integer)
-> (VarSet -> VarSet) -> Map VarSet Integer -> Map VarSet 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
(+) (Lit -> VarSet -> VarSet
IntSet.insert Lit
v) Map VarSet Integer
m
      | Bool
otherwise = (Integer -> Integer -> Integer)
-> Map VarSet Integer -> Map VarSet Integer -> Map VarSet 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 VarSet Integer
m (Map VarSet Integer -> Map VarSet Integer)
-> Map VarSet Integer -> Map VarSet Integer
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer)
-> [(VarSet, Integer)] -> Map VarSet 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
(+) [(Lit -> VarSet -> VarSet
IntSet.insert Lit
v VarSet
xs, Integer -> Integer
forall a. Num a => a -> a
negate Integer
c) | (VarSet
xs,Integer
c) <- Map VarSet Integer -> [(VarSet, Integer)]
forall k a. Map k a -> [(k, a)]
Map.toList Map VarSet Integer
m]
      where
        v :: Lit
v = Lit -> Lit
litVar Lit
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 ([Lit]
lits, Bool
b) =
  case IntMap Bool -> [Lit]
forall a. IntMap a -> [Lit]
IntMap.keys IntMap Bool
m of
    Lit
0:[Lit]
xs -> ([Lit]
xs, Bool -> Bool
not Bool
b)
    [Lit]
xs -> ([Lit]
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 [Lit -> IntMap Bool
f Lit
lit | Lit
lit <- [Lit]
lits]
    xor :: Bool -> Bool -> Bool
xor = Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(/=)

    f :: Lit -> IntMap Bool
f Lit
0 = Lit -> Bool -> IntMap Bool
forall a. Lit -> a -> IntMap a
IntMap.singleton Lit
0 Bool
True
    f Lit
lit =
      if Lit -> Bool
litPolarity Lit
lit
      then Lit -> Bool -> IntMap Bool
forall a. Lit -> a -> IntMap a
IntMap.singleton Lit
lit Bool
True
      else [(Lit, Bool)] -> IntMap Bool
forall a. [(Lit, a)] -> IntMap a
IntMap.fromList [(Lit -> Lit
litVar Lit
lit, Bool
True), (Lit
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 :: forall (m :: * -> *).
Monad m =>
(Lit -> m LBool) -> XORClause -> m XORClause
instantiateXORClause Lit -> m LBool
evalLitM ([Lit]
ls,Bool
b) = [Lit] -> Bool -> [Lit] -> m XORClause
loop [] Bool
b [Lit]
ls
  where
    loop :: [Lit] -> Bool -> [Lit] -> m XORClause
    loop :: [Lit] -> Bool -> [Lit] -> m XORClause
loop [Lit]
lhs !Bool
rhs [] = XORClause -> m XORClause
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Lit]
lhs, Bool
rhs)
    loop [Lit]
lhs !Bool
rhs (Lit
l:[Lit]
ls) = do
      LBool
val <- Lit -> m LBool
evalLitM Lit
l
      if LBool
valLBool -> LBool -> Bool
forall a. Eq a => a -> a -> Bool
==LBool
lTrue then
        [Lit] -> Bool -> [Lit] -> m XORClause
loop [Lit]
lhs (Bool -> Bool
not Bool
rhs) [Lit]
ls
      else if LBool
valLBool -> LBool -> Bool
forall a. Eq a => a -> a -> Bool
==LBool
lFalse then
        [Lit] -> Bool -> [Lit] -> m XORClause
loop [Lit]
lhs Bool
rhs [Lit]
ls
      else
        [Lit] -> Bool -> [Lit] -> m XORClause
loop (Lit
l Lit -> [Lit] -> [Lit]
forall a. a -> [a] -> [a]
: [Lit]
lhs) Bool
rhs [Lit]
ls

evalXORClause :: IModel m => m -> XORClause -> Bool
evalXORClause :: forall m. IModel m => m -> XORClause -> Bool
evalXORClause m
m ([Lit]
lits, Bool
rhs) = (Bool -> Bool -> Bool) -> Bool -> [Bool] -> Bool
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Bool -> Bool -> Bool
xor Bool
False ((Lit -> Bool) -> [Lit] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map Lit -> Bool
f [Lit]
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 :: Lit -> Bool
f Lit
0 = Bool
True
    f Lit
lit = m -> Lit -> Bool
forall m. IModel m => m -> Lit -> Bool
evalLit m
m Lit
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 Lit
n = Lit -> m Lit -> m [Lit]
forall (m :: * -> *) a. Applicative m => Lit -> m a -> m [a]
replicateM Lit
n (a -> m Lit
forall (m :: * -> *) a. NewVar m a => a -> m Lit
newVar a
a)

  -- | Add variables. @newVars_ a n = newVars a n >> return ()@, but maybe faster.
  newVars_ :: a -> Int -> m ()
  newVars_ a
a Lit
n = Lit -> m Lit -> m ()
forall (m :: * -> *) a. Applicative m => Lit -> m a -> m ()
replicateM_ Lit
n (a -> m Lit
forall (m :: * -> *) a. NewVar m a => a -> m Lit
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 [Lit]
lits Lit
n = do
    a -> [Lit] -> Lit -> m ()
forall (m :: * -> *) a.
AddCardinality m a =>
a -> [Lit] -> Lit -> m ()
addAtLeast a
a ((Lit -> Lit) -> [Lit] -> [Lit]
forall a b. (a -> b) -> [a] -> [b]
map Lit -> Lit
litNot [Lit]
lits) ([Lit] -> Lit
forall a. [a] -> Lit
forall (t :: * -> *) a. Foldable t => t a -> Lit
length [Lit]
lits Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
- Lit
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 [Lit]
lits Lit
n = do
    a -> [Lit] -> Lit -> m ()
forall (m :: * -> *) a.
AddCardinality m a =>
a -> [Lit] -> Lit -> m ()
addAtLeast a
a [Lit]
lits Lit
n
    a -> [Lit] -> Lit -> m ()
forall (m :: * -> *) a.
AddCardinality m a =>
a -> [Lit] -> Lit -> m ()
addAtMost a
a [Lit]
lits Lit
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,Lit
l) | (Integer
c,Lit
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 Lit
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, Lit -> Lit
litNot Lit
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 Lit
sel [PBLinTerm]
lhs Integer
rhs =
    a -> Lit -> [PBLinTerm] -> Integer -> m ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> Lit -> [PBLinTerm] -> Integer -> m ()
addPBAtLeastSoft a
a Lit
sel [(Integer -> Integer
forall a. Num a => a -> a
negate Integer
c, Lit
lit) | (Integer
c,Lit
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 Lit
sel [PBLinTerm]
lhs Integer
rhs = do
    a -> Lit -> [PBLinTerm] -> Integer -> m ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> Lit -> [PBLinTerm] -> Integer -> m ()
addPBAtLeastSoft a
a Lit
sel [PBLinTerm]
lhs Integer
rhs
    a -> Lit -> [PBLinTerm] -> Integer -> m ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> Lit -> [PBLinTerm] -> Integer -> m ()
addPBAtMostSoft a
a Lit
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,[Lit]
ls) | (Integer
c,[Lit]
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 Lit
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 a. Num a => [a] -> a
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,[Lit]
_) <- PBSum
lhs]
    a -> PBSum -> Integer -> m ()
forall (m :: * -> *) a.
AddPBNL m a =>
a -> PBSum -> Integer -> m ()
addPBNLAtLeast a
a ((Integer
n, [Lit -> Lit
litNot Lit
sel]) (Integer, [Lit]) -> 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 Lit
sel PBSum
lhs Integer
rhs =
    a -> Lit -> PBSum -> Integer -> m ()
forall (m :: * -> *) a.
AddPBNL m a =>
a -> Lit -> PBSum -> Integer -> m ()
addPBNLAtLeastSoft a
a Lit
sel [(Integer -> Integer
forall a. Num a => a -> a
negate Integer
c, [Lit]
ls) | (Integer
c,[Lit]
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 Lit
sel PBSum
lhs Integer
rhs = do
    a -> Lit -> PBSum -> Integer -> m ()
forall (m :: * -> *) a.
AddPBNL m a =>
a -> Lit -> PBSum -> Integer -> m ()
addPBNLAtLeastSoft a
a Lit
sel PBSum
lhs Integer
rhs
    a -> Lit -> PBSum -> Integer -> m ()
forall (m :: * -> *) a.
AddPBNL m a =>
a -> Lit -> PBSum -> Integer -> m ()
addPBNLAtMostSoft a
a Lit
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 Lit
sel [Lit]
lits Bool
rhs = do
    Lit
reified <- a -> m Lit
forall (m :: * -> *) a. NewVar m a => a -> m Lit
newVar a
a
    a -> [Lit] -> Bool -> m ()
forall (m :: * -> *) a.
AddXORClause m a =>
a -> [Lit] -> Bool -> m ()
addXORClause a
a (Lit -> Lit
litNot Lit
reified Lit -> [Lit] -> [Lit]
forall a. a -> [a] -> [a]
: [Lit]
lits) Bool
rhs
    a -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
addClause a
a [Lit -> Lit
litNot Lit
sel, Lit
reified] -- sel ⇒ reified

-- | Add a type-2 SOS constraint
--
-- At most two adjacnt literals can be true.
addSOS2 :: AddClause m a => a -> [Lit] -> m ()
addSOS2 :: forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
addSOS2 a
a [Lit]
xs =
  [(Lit, Lit)] -> ((Lit, Lit) -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([Lit] -> [(Lit, Lit)]
forall a. [a] -> [(a, a)]
nonAdjacentPairs [Lit]
xs) (((Lit, Lit) -> m ()) -> m ()) -> ((Lit, Lit) -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \(Lit
x1,Lit
x2) -> do
    a -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
addClause a
a [Lit -> Lit
litNot Lit
v | Lit
v <- [Lit
x1,Lit
x2]]
  where
    nonAdjacentPairs :: [a] -> [(a,a)]
    nonAdjacentPairs :: forall a. [a] -> [(a, a)]
nonAdjacentPairs (a
x1:a
x2:[a]
xs) = [(a
x1,a
x3) | a
x3 <- [a]
xs] [(a, a)] -> [(a, a)] -> [(a, a)]
forall a. [a] -> [a] -> [a]
++ [a] -> [(a, a)]
forall a. [a] -> [(a, a)]
nonAdjacentPairs (a
x2a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs)
    nonAdjacentPairs [a]
_ = []

-- | Evaluate type-2 SOS constraint
evalSOS2 :: IModel m => m -> [Lit] -> Bool
evalSOS2 :: forall m. IModel m => m -> [Lit] -> Bool
evalSOS2 m
m = [Lit] -> Bool
f
  where
    f :: [Lit] -> Bool
f [] = Bool
True
    f [Lit
_] = Bool
True
    f (Lit
l1 : Lit
l2 : [Lit]
ls)
      | m -> Lit -> Bool
forall m. IModel m => m -> Lit -> Bool
evalLit m
m Lit
l1 = (Lit -> Bool) -> [Lit] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (Lit -> Bool) -> Lit -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m -> Lit -> Bool
forall m. IModel m => m -> Lit -> Bool
evalLit m
m) [Lit]
ls
      | Bool
otherwise = [Lit] -> Bool
f (Lit
l2 Lit -> [Lit] -> [Lit]
forall a. a -> [a] -> [a]
: [Lit]
ls)