{-# 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 :: Lit -> Bool
validVar Lit
v = Lit
v 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 = 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 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 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 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 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 =
  forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Lit -> Bool
validVar Lit
v) 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 = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Lit -> Bool
validLit Lit
l) forall a b. (a -> b) -> a -> b
$ 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 = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Lit -> Bool
validLit Lit
l) forall a b. (a -> b) -> a -> b
$ 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 = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Lit -> Bool
validLit Lit
l) forall a b. (a -> b) -> a -> b
$ Lit
l 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 forall a. Ord a => a -> a -> Bool
> Lit
0 then forall m. IModel m => m -> Lit -> Bool
evalVar m
m Lit
l else Bool -> Bool
not (forall m. IModel m => m -> Lit -> Bool
evalVar m
m (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 :: Clause -> Maybe Clause
normalizeClause Clause
lits = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (VarSet -> Lit
IntSet.size VarSet
ys forall a. Integral a => a -> a -> a
`mod` Lit
2 forall a. Eq a => a -> a -> Bool
== Lit
0) forall a b. (a -> b) -> a -> b
$
  if VarSet -> Bool
IntSet.null VarSet
ys
    then forall a. a -> Maybe a
Just (VarSet -> Clause
IntSet.toList VarSet
xs)
    else forall a. Maybe a
Nothing
  where
    xs :: VarSet
xs = Clause -> VarSet
IntSet.fromList Clause
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) -> Clause -> m (Maybe Clause)
instantiateClause Lit -> 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 [] = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Clause
ret
    loop Clause
ret (Lit
l:Clause
ls) = do
      LBool
val <- Lit -> m LBool
evalLitM Lit
l
      if LBool
valforall a. Eq a => a -> a -> Bool
==LBool
lTrue then
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
      else if LBool
valforall 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 (Lit
l forall a. a -> [a] -> [a]
: Clause
ret) Clause
ls

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

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

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

type PackedVar = PackedLit
type PackedLit = Int32

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

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

type PackedClause = VU.Vector PackedLit

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

unpackClause :: PackedClause -> Clause
unpackClause :: PackedClause -> Clause
unpackClause = forall a b. (a -> b) -> [a] -> [b]
map PackedLit -> Lit
unpackLit forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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,Lit
n) = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (VarSet -> Lit
IntSet.size VarSet
ys forall a. Integral a => a -> a -> a
`mod` Lit
2 forall a. Eq a => a -> a -> Bool
== Lit
0) forall a b. (a -> b) -> a -> b
$
   (VarSet -> Clause
IntSet.toList VarSet
lits', Lit
n')
   where
     xs :: VarSet
xs = Clause -> VarSet
IntSet.fromList Clause
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 forall a. Num a => a -> a -> a
- (VarSet -> Lit
IntSet.size VarSet
ys 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 (Clause
xs,Lit
n) = AtLeast -> Clause -> m AtLeast
loop ([],Lit
n) Clause
xs
  where
    loop :: AtLeast -> [Lit] -> m AtLeast
    loop :: AtLeast -> Clause -> m AtLeast
loop AtLeast
ret [] = forall (m :: * -> *) a. Monad m => a -> m a
return AtLeast
ret
    loop (Clause
ys,Lit
m) (Lit
l:Clause
ls) = do
      LBool
val <- Lit -> m LBool
evalLitM Lit
l
      if LBool
val forall a. Eq a => a -> a -> Bool
== LBool
lTrue then
        AtLeast -> Clause -> m AtLeast
loop (Clause
ys, Lit
mforall a. Num a => a -> a -> a
-Lit
1) Clause
ls
      else if LBool
val forall a. Eq a => a -> a -> Bool
== LBool
lFalse then
        AtLeast -> Clause -> m AtLeast
loop (Clause
ys, Lit
m) Clause
ls
      else
        AtLeast -> Clause -> m AtLeast
loop (Lit
lforall a. a -> [a] -> [a]
:Clause
ys, Lit
m) Clause
ls

evalAtLeast :: IModel m => m -> AtLeast -> Bool
evalAtLeast :: forall m. IModel m => m -> AtLeast -> Bool
evalAtLeast m
m (Clause
lits,Lit
n) = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Lit
1 | Lit
lit <- Clause
lits, forall m. IModel m => m -> Lit -> Bool
evalLit m
m Lit
lit] 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 (Clause
lits,Lit
n) = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Lit
1 | Lit
lit <- Clause
lits, forall m. IModel m => m -> Lit -> Bool
evalLit m
m Lit
lit] 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 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 (forall a. IntMap a
IntMap.empty,Integer
n) [PBLinTerm]
xs of
        (VarMap Integer
ys,Integer
n') -> ([(Integer
c,Lit
v) | (Lit
v,Integer
c) <- 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 (forall a. (a -> a -> a) -> Lit -> a -> IntMap a -> IntMap a
IntMap.insertWith 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 (forall a. (a -> a -> a) -> Lit -> a -> IntMap a -> IntMap a
IntMap.insertWith forall a. Num a => a -> a -> a
(+) (Lit -> Lit
litNot Lit
l) (forall a. Num a => a -> a
negate Integer
c) VarMap Integer
ys, Integer
mforall a. Num a => a -> a -> a
+Integer
c) [PBLinTerm]
zs

    -- 係数が0のものも取り除き、係数が負のリテラルを反転することで、
    -- 係数が正になるようにする。
    step2 :: (PBLinSum, Integer) -> (PBLinSum, Integer)
    step2 :: PBLinAtLeast -> PBLinAtLeast
step2 ([PBLinTerm]
xs,Integer
n) = 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 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 forall a. Ord a => a -> a -> Bool
< b
0  = ([(b, Lit)], b) -> [(b, Lit)] -> ([(b, Lit)], b)
loop ((forall a. Num a => a -> a
negate b
c,Lit -> Lit
litNot Lit
l)forall a. a -> [a] -> [a]
:[(b, Lit)]
ys, b
mforall a. Num a => a -> a -> a
+b
c) [(b, Lit)]
zs
          | Bool
otherwise = ([(b, Lit)], b) -> [(b, Lit)] -> ([(b, Lit)], b)
loop ((b, Lit)
tforall 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 forall a. Ord a => a -> a -> Bool
> Integer
0     -> PBLinAtLeast -> PBLinAtLeast
step4 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, forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Integer
cforall a. Ord a => a -> a -> Bool
>Integer
0) (Integer
c 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 = forall a. (a -> a -> a) -> [a] -> a
foldl1' forall a. Integral a => a -> a -> a
gcd [Integer]
cs
              m :: Integer
m = (Integer
nforall a. Num a => a -> a -> a
+Integer
dforall a. Num a => a -> a -> a
-Integer
1) forall a. Integral a => a -> a -> a
`div` Integer
d
          in ([(if Integer
c forall a. Ord a => a -> a -> Bool
>= Integer
n then Integer
m else Integer
c 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 forall (v :: * -> *).
Vector v Integer =>
v Integer -> Integer -> Maybe (Integer, Vector Bool)
SubsetSum.minSubsetSum (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 forall a b. (a -> b) -> a -> b
$ PBLinAtLeast
a of
    ([PBLinTerm]
xs,Integer
n)
      | Integer
n forall a. Ord a => a -> a -> Bool
>= Integer
0    -> PBLinAtLeast -> PBLinAtLeast
step3 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 forall a. Integral a => a -> a -> a
`mod` Integer
d forall a. Eq a => a -> a -> Bool
== Integer
0 = ([(Integer
c forall a. Integral a => a -> a -> a
`div` Integer
d, Lit
l) | (Integer
c,Lit
l) <- [PBLinTerm]
xs], Integer
n forall a. Integral a => a -> a -> a
`div` Integer
d)
      | Bool
otherwise      = ([], Integer
1) -- false
      where
        d :: Integer
d = forall a. (a -> a -> a) -> [a] -> a
foldl1' 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 forall (v :: * -> *).
Vector v Integer =>
v Integer -> Integer -> Maybe (Vector Bool)
SubsetSum.subsetSum (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 [] = 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 forall a. Eq a => a -> a -> Bool
== LBool
lTrue then
        PBLinAtLeast -> [PBLinTerm] -> m PBLinAtLeast
loop ([PBLinTerm]
ys, Integer
mforall a. Num a => a -> a -> a
-Integer
c) [PBLinTerm]
ts
      else if LBool
val 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)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 = 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 = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Lit
l1 forall a. Eq a => a -> a -> Bool
== Lit -> Lit
litNot Lit
l2) forall a b. (a -> b) -> a -> b
$ PBLinAtLeast -> PBLinAtLeast
normalizePBLinAtLeast PBLinAtLeast
pb
  where
    (Integer
c1,Lit
l1) = forall a. [a] -> a
head [(Integer
c,Lit
l) | (Integer
c,Lit
l) <- [PBLinTerm]
lhs1, Lit -> Lit
litVar Lit
l forall a. Eq a => a -> a -> Bool
== Lit
v]
    (Integer
c2,Lit
l2) = forall a. [a] -> a
head [(Integer
c,Lit
l) | (Integer
c,Lit
l) <- [PBLinTerm]
lhs2, Lit -> Lit
litVar Lit
l forall a. Eq a => a -> a -> Bool
== Lit
v]
    g :: Integer
g = forall a. Integral a => a -> a -> a
gcd Integer
c1 Integer
c2
    s1 :: Integer
s1 = Integer
c2 forall a. Integral a => a -> a -> a
`div` Integer
g
    s2 :: Integer
s2 = Integer
c1 forall a. Integral a => a -> a -> a
`div` Integer
g
    pb :: PBLinAtLeast
pb = ([(Integer
s1forall a. Num a => a -> a -> a
*Integer
c,Lit
l) | (Integer
c,Lit
l) <- [PBLinTerm]
lhs1] forall a. [a] -> [a] -> [a]
++ [(Integer
s2forall a. Num a => a -> a -> a
*Integer
c,Lit
l) | (Integer
c,Lit
l) <- [PBLinTerm]
lhs2], Integer
s1forall a. Num a => a -> a -> a
*Integer
rhs1 forall a. Num a => a -> a -> a
+ Integer
s2 forall a. Num a => a -> a -> a
* Integer
rhs2)

cardinalityReduction :: PBLinAtLeast -> AtLeast
cardinalityReduction :: PBLinAtLeast -> AtLeast
cardinalityReduction ([PBLinTerm]
lhs,Integer
rhs) = (Clause
ls, Lit
rhs')
  where
    rhs' :: Lit
rhs' = forall {t} {b}. Num t => Integer -> t -> [(Integer, b)] -> t
go1 Integer
0 Lit
0 (forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing 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 forall a. Ord a => a -> a -> Bool
< Integer
rhs   = Integer -> t -> [(Integer, b)] -> t
go1 (Integer
sforall a. Num a => a -> a -> a
+Integer
a) (t
kforall a. Num a => a -> a -> a
+t
1) [(Integer, b)]
ts
      | Bool
otherwise = t
k
    go1 Integer
_ t
_ [] = forall a. (?callStack::CallStack) => [Char] -> a
error [Char]
"ToySolver.SAT.Types.cardinalityReduction: should not happen"

    ls :: Clause
ls = forall {a} {b}. (Ord a, Num a) => a -> [(a, b)] -> [b]
go2 (forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum (Integer
rhs forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall a. Num a => a -> a -> a
subtract Integer
1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [PBLinTerm]
lhs)) (forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing 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 forall a. Num a => a -> a -> a
- a
1 forall a. Ord a => a -> a -> Bool
< a
guard' = a -> [(a, b)] -> [b]
go2 (a
guard' forall a. Num a => a -> a -> a
- a
a) [(a, b)]
ts
      | Bool
otherwise      = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(a, b)]
ts
    go2 a
_ [] = 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 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 = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
c | (Integer
c,Lit
lit) <- [PBLinTerm]
xs, 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) = forall m. IModel m => m -> [PBLinTerm] -> Integer
evalPBLinSum m
m [PBLinTerm]
lhs 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) = forall m. IModel m => m -> [PBLinTerm] -> Integer
evalPBLinSum m
m [PBLinTerm]
lhs forall a. Eq a => a -> a -> Bool
== Integer
rhs

pbLinLowerBound :: PBLinSum -> Integer
pbLinLowerBound :: [PBLinTerm] -> Integer
pbLinLowerBound [PBLinTerm]
xs = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [if Integer
c 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 = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [if Integer
c 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 forall a. Ord a => a -> a -> Bool
>= Integer
rhs2 Bool -> Bool -> Bool
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Integer
di forall a. Ord a => a -> a -> Bool
>= Integer
ci | (Integer
ci,Lit
li) <- [PBLinTerm]
lhs1, let di :: Integer
di = forall a. a -> Lit -> IntMap a -> a
IntMap.findWithDefault Integer
0 Lit
li VarMap Integer
lhs2']
  where
    lhs2' :: VarMap Integer
lhs2' = 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 = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
c | (Integer
c,Clause
lits) <- PBSum
xs, forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall m. IModel m => m -> Lit -> Bool
evalLit m
m) Clause
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' (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 -> forall a. Ord a => a -> a -> Bool
(>=)
            Op
PBFile.Eq -> 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
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall m. IModel m => m -> Constraint -> Bool
evalPBConstraint m
m) forall a b. (a -> b) -> a -> b
$ Formula -> [Constraint]
PBFile.pbConstraints Formula
formula
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall m. IModel m => m -> PBSum -> Integer
evalPBSum m
m forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe [] forall a b. (a -> b) -> a -> b
$ Formula -> Maybe PBSum
PBFile.pbObjectiveFunction Formula
formula

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

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

removeNegationFromPBSum :: PBSum -> PBSum
removeNegationFromPBSum :: PBSum -> PBSum
removeNegationFromPBSum PBSum
ts =
  [(Integer
c, VarSet -> Clause
IntSet.toList VarSet
m) | (VarSet
m, Integer
c) <- forall k a. Map k a -> [(k, a)]
Map.toList forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith forall a. Num a => a -> a -> a
(+) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Integer, Clause) -> Map VarSet Integer
f PBSum
ts, Integer
c forall a. Eq a => a -> a -> Bool
/= Integer
0]
  where
    f :: PBTerm -> Map VarSet Integer
    f :: (Integer, Clause) -> Map VarSet Integer
f (Integer
c, Clause
ls) = forall a. (a -> Lit -> a) -> a -> VarSet -> a
IntSet.foldl' Map VarSet Integer -> Lit -> Map VarSet Integer
g (forall k a. k -> a -> Map k a
Map.singleton VarSet
IntSet.empty Integer
c) (Clause -> VarSet
IntSet.fromList Clause
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 forall a. Ord a => a -> a -> Bool
> Lit
0     = forall k2 a k1.
Ord k2 =>
(a -> a -> a) -> (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeysWith forall a. Num a => a -> a -> a
(+) (Lit -> VarSet -> VarSet
IntSet.insert Lit
v) Map VarSet Integer
m
      | Bool
otherwise = forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. Num a => a -> a -> a
(+) Map VarSet Integer
m forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. Num a => a -> a -> a
(+) [(Lit -> VarSet -> VarSet
IntSet.insert Lit
v VarSet
xs, forall a. Num a => a -> a
negate Integer
c) | (VarSet
xs,Integer
c) <- 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 (Clause
lits, Bool
b) =
  case forall a. IntMap a -> Clause
IntMap.keys IntMap Bool
m of
    Lit
0:Clause
xs -> (Clause
xs, Bool -> Bool
not Bool
b)
    Clause
xs -> (Clause
xs, Bool
b)
  where
    m :: IntMap Bool
m = forall a. (a -> Bool) -> IntMap a -> IntMap a
IntMap.filter forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ 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 <- Clause
lits]
    xor :: Bool -> Bool -> Bool
xor = forall a. Eq a => a -> a -> Bool
(/=)

    f :: Lit -> IntMap Bool
f Lit
0 = forall a. Lit -> a -> IntMap a
IntMap.singleton Lit
0 Bool
True
    f Lit
lit =
      if Lit -> Bool
litPolarity Lit
lit
      then forall a. Lit -> a -> IntMap a
IntMap.singleton Lit
lit Bool
True
      else 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 (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 [] = forall (m :: * -> *) a. Monad m => a -> m a
return (Clause
lhs, Bool
rhs)
    loop Clause
lhs !Bool
rhs (Lit
l:Clause
ls) = do
      LBool
val <- Lit -> m LBool
evalLitM Lit
l
      if LBool
valforall 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
valforall 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 (Lit
l forall a. a -> [a] -> [a]
: Clause
lhs) Bool
rhs Clause
ls

evalXORClause :: IModel m => m -> XORClause -> Bool
evalXORClause :: forall m. IModel m => m -> XORClause -> Bool
evalXORClause m
m (Clause
lits, Bool
rhs) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Bool -> Bool -> Bool
xor Bool
False (forall a b. (a -> b) -> [a] -> [b]
map Lit -> Bool
f Clause
lits) forall a. Eq a => a -> a -> Bool
== Bool
rhs
  where
    xor :: Bool -> Bool -> Bool
xor = forall a. Eq a => a -> a -> Bool
(/=)
    f :: Lit -> Bool
f Lit
0 = Bool
True
    f Lit
lit = 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 = forall (m :: * -> *) a. Applicative m => Lit -> m a -> m [a]
replicateM Lit
n (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 = forall (m :: * -> *) a. Applicative m => Lit -> m a -> m ()
replicateM_ Lit
n (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 Clause
lits Lit
n = do
    forall (m :: * -> *) a.
AddCardinality m a =>
a -> Clause -> Lit -> m ()
addAtLeast a
a (forall a b. (a -> b) -> [a] -> [b]
map Lit -> Lit
litNot Clause
lits) (forall (t :: * -> *) a. Foldable t => t a -> Lit
length Clause
lits 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 Clause
lits Lit
n = do
    forall (m :: * -> *) a.
AddCardinality m a =>
a -> Clause -> Lit -> m ()
addAtLeast a
a Clause
lits Lit
n
    forall (m :: * -> *) a.
AddCardinality m a =>
a -> Clause -> Lit -> m ()
addAtMost a
a Clause
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 = forall (m :: * -> *) a.
AddPBLin m a =>
a -> [PBLinTerm] -> Integer -> m ()
addPBAtLeast a
a [(-Integer
c,Lit
l) | (Integer
c,Lit
l) <- [PBLinTerm]
ts] (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
    forall (m :: * -> *) a.
AddPBLin m a =>
a -> [PBLinTerm] -> Integer -> m ()
addPBAtLeast a
a [PBLinTerm]
ts Integer
n
    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)
    forall (m :: * -> *) a.
AddPBLin m a =>
a -> [PBLinTerm] -> Integer -> m ()
addPBAtLeast a
a ((Integer
rhs2, Lit -> Lit
litNot Lit
sel) 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 =
    forall (m :: * -> *) a.
AddPBLin m a =>
a -> Lit -> [PBLinTerm] -> Integer -> m ()
addPBAtLeastSoft a
a Lit
sel [(forall a. Num a => a -> a
negate Integer
c, Lit
lit) | (Integer
c,Lit
lit) <- [PBLinTerm]
lhs] (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
    forall (m :: * -> *) a.
AddPBLin m a =>
a -> Lit -> [PBLinTerm] -> Integer -> m ()
addPBAtLeastSoft a
a Lit
sel [PBLinTerm]
lhs Integer
rhs
    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 = forall (m :: * -> *) a.
AddPBNL m a =>
a -> PBSum -> Integer -> m ()
addPBNLAtLeast a
a [(-Integer
c,Clause
ls) | (Integer
c,Clause
ls) <- PBSum
ts] (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
    forall (m :: * -> *) a.
AddPBNL m a =>
a -> PBSum -> Integer -> m ()
addPBNLAtLeast a
a PBSum
ts Integer
n
    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 forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [forall a. Ord a => a -> a -> a
min Integer
c Integer
0 | (Integer
c,Clause
_) <- PBSum
lhs]
    forall (m :: * -> *) a.
AddPBNL m a =>
a -> PBSum -> Integer -> m ()
addPBNLAtLeast a
a ((Integer
n, [Lit -> Lit
litNot Lit
sel]) 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 =
    forall (m :: * -> *) a.
AddPBNL m a =>
a -> Lit -> PBSum -> Integer -> m ()
addPBNLAtLeastSoft a
a Lit
sel [(forall a. Num a => a -> a
negate Integer
c, Clause
ls) | (Integer
c,Clause
ls) <- PBSum
lhs] (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
    forall (m :: * -> *) a.
AddPBNL m a =>
a -> Lit -> PBSum -> Integer -> m ()
addPBNLAtLeastSoft a
a Lit
sel PBSum
lhs Integer
rhs
    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 Clause
lits Bool
rhs = do
    Lit
reified <- forall (m :: * -> *) a. NewVar m a => a -> m Lit
newVar a
a
    forall (m :: * -> *) a.
AddXORClause m a =>
a -> Clause -> Bool -> m ()
addXORClause a
a (Lit -> Lit
litNot Lit
reified forall a. a -> [a] -> [a]
: Clause
lits) Bool
rhs
    forall (m :: * -> *) a. AddClause m a => a -> Clause -> m ()
addClause a
a [Lit -> Lit
litNot Lit
sel, Lit
reified] -- sel ⇒ reified