{-# LANGUAGE BangPatterns, DeriveDataTypeable, DeriveGeneric #-}
{-# OPTIONS_GHC -Wall #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.PseudoBoolean.Types
-- Copyright   :  (c) Masahiro Sakai 2011-2015
-- License     :  BSD-style
-- 
-- Maintainer  :  masahiro.sakai@gmail.com
-- Portability :  non-portable (BangPatterns, DeriveDataTypeable, DeriveGeneric)
-- 
-- References:
--
-- * Input/Output Format and Solver Requirements for the Competitions of
--   Pseudo-Boolean Solvers
--   <http://www.cril.univ-artois.fr/PB11/format.pdf>
--
-----------------------------------------------------------------------------

module Data.PseudoBoolean.Types
  (
  -- * Abstract Syntax
    Formula (..)
  , Constraint
  , Op (..)
  , SoftFormula (..)
  , SoftConstraint
  , Sum
  , WeightedTerm
  , Term
  , Lit
  , Var

  -- * Internal utilities
  , pbComputeNumVars
  , pbProducts
  , wboComputeNumVars
  , wboProducts
  , wboNumSoft
  ) where

import GHC.Generics (Generic)
import Control.Monad
import Control.DeepSeq
import Data.Data
import Data.Set (Set)
import qualified Data.Set as Set
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.Hashable
import Data.Maybe

-- | Pair of /objective function/ and a list of constraints.
data Formula
  = Formula
  { Formula -> Maybe Sum
pbObjectiveFunction :: Maybe Sum
  , Formula -> [Constraint]
pbConstraints :: [Constraint]
  , Formula -> Int
pbNumVars :: !Int
  , Formula -> Int
pbNumConstraints :: !Int
  }
  deriving (Formula -> Formula -> Bool
(Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool) -> Eq Formula
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Formula -> Formula -> Bool
$c/= :: Formula -> Formula -> Bool
== :: Formula -> Formula -> Bool
$c== :: Formula -> Formula -> Bool
Eq, Eq Formula
Eq Formula
-> (Formula -> Formula -> Ordering)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Formula)
-> (Formula -> Formula -> Formula)
-> Ord Formula
Formula -> Formula -> Bool
Formula -> Formula -> Ordering
Formula -> Formula -> Formula
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Formula -> Formula -> Formula
$cmin :: Formula -> Formula -> Formula
max :: Formula -> Formula -> Formula
$cmax :: Formula -> Formula -> Formula
>= :: Formula -> Formula -> Bool
$c>= :: Formula -> Formula -> Bool
> :: Formula -> Formula -> Bool
$c> :: Formula -> Formula -> Bool
<= :: Formula -> Formula -> Bool
$c<= :: Formula -> Formula -> Bool
< :: Formula -> Formula -> Bool
$c< :: Formula -> Formula -> Bool
compare :: Formula -> Formula -> Ordering
$ccompare :: Formula -> Formula -> Ordering
$cp1Ord :: Eq Formula
Ord, Int -> Formula -> ShowS
[Formula] -> ShowS
Formula -> String
(Int -> Formula -> ShowS)
-> (Formula -> String) -> ([Formula] -> ShowS) -> Show Formula
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Formula] -> ShowS
$cshowList :: [Formula] -> ShowS
show :: Formula -> String
$cshow :: Formula -> String
showsPrec :: Int -> Formula -> ShowS
$cshowsPrec :: Int -> Formula -> ShowS
Show, ReadPrec [Formula]
ReadPrec Formula
Int -> ReadS Formula
ReadS [Formula]
(Int -> ReadS Formula)
-> ReadS [Formula]
-> ReadPrec Formula
-> ReadPrec [Formula]
-> Read Formula
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Formula]
$creadListPrec :: ReadPrec [Formula]
readPrec :: ReadPrec Formula
$creadPrec :: ReadPrec Formula
readList :: ReadS [Formula]
$creadList :: ReadS [Formula]
readsPrec :: Int -> ReadS Formula
$creadsPrec :: Int -> ReadS Formula
Read, Typeable, Typeable Formula
DataType
Constr
Typeable Formula
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Formula -> c Formula)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Formula)
-> (Formula -> Constr)
-> (Formula -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Formula))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formula))
-> ((forall b. Data b => b -> b) -> Formula -> Formula)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Formula -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Formula -> r)
-> (forall u. (forall d. Data d => d -> u) -> Formula -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Formula -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Formula -> m Formula)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Formula -> m Formula)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Formula -> m Formula)
-> Data Formula
Formula -> DataType
Formula -> Constr
(forall b. Data b => b -> b) -> Formula -> Formula
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Formula -> c Formula
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Formula
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Formula -> u
forall u. (forall d. Data d => d -> u) -> Formula -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Formula
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Formula -> c Formula
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Formula)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formula)
$cFormula :: Constr
$tFormula :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Formula -> m Formula
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
gmapMp :: (forall d. Data d => d -> m d) -> Formula -> m Formula
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
gmapM :: (forall d. Data d => d -> m d) -> Formula -> m Formula
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
gmapQi :: Int -> (forall d. Data d => d -> u) -> Formula -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Formula -> u
gmapQ :: (forall d. Data d => d -> u) -> Formula -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Formula -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r
gmapT :: (forall b. Data b => b -> b) -> Formula -> Formula
$cgmapT :: (forall b. Data b => b -> b) -> Formula -> Formula
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formula)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formula)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Formula)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Formula)
dataTypeOf :: Formula -> DataType
$cdataTypeOf :: Formula -> DataType
toConstr :: Formula -> Constr
$ctoConstr :: Formula -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Formula
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Formula
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Formula -> c Formula
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Formula -> c Formula
$cp1Data :: Typeable Formula
Data, (forall x. Formula -> Rep Formula x)
-> (forall x. Rep Formula x -> Formula) -> Generic Formula
forall x. Rep Formula x -> Formula
forall x. Formula -> Rep Formula x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Formula x -> Formula
$cfrom :: forall x. Formula -> Rep Formula x
Generic)

instance NFData Formula
instance Hashable Formula

-- | Lhs, relational operator and rhs.
type Constraint = (Sum, Op, Integer)

-- | Relational operators
data Op
  = Ge -- ^ /greater than or equal/
  | Eq -- ^ /equal/
  deriving (Op -> Op -> Bool
(Op -> Op -> Bool) -> (Op -> Op -> Bool) -> Eq Op
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Op -> Op -> Bool
$c/= :: Op -> Op -> Bool
== :: Op -> Op -> Bool
$c== :: Op -> Op -> Bool
Eq, Eq Op
Eq Op
-> (Op -> Op -> Ordering)
-> (Op -> Op -> Bool)
-> (Op -> Op -> Bool)
-> (Op -> Op -> Bool)
-> (Op -> Op -> Bool)
-> (Op -> Op -> Op)
-> (Op -> Op -> Op)
-> Ord Op
Op -> Op -> Bool
Op -> Op -> Ordering
Op -> Op -> Op
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Op -> Op -> Op
$cmin :: Op -> Op -> Op
max :: Op -> Op -> Op
$cmax :: Op -> Op -> Op
>= :: Op -> Op -> Bool
$c>= :: Op -> Op -> Bool
> :: Op -> Op -> Bool
$c> :: Op -> Op -> Bool
<= :: Op -> Op -> Bool
$c<= :: Op -> Op -> Bool
< :: Op -> Op -> Bool
$c< :: Op -> Op -> Bool
compare :: Op -> Op -> Ordering
$ccompare :: Op -> Op -> Ordering
$cp1Ord :: Eq Op
Ord, Int -> Op -> ShowS
[Op] -> ShowS
Op -> String
(Int -> Op -> ShowS)
-> (Op -> String) -> ([Op] -> ShowS) -> Show Op
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Op] -> ShowS
$cshowList :: [Op] -> ShowS
show :: Op -> String
$cshow :: Op -> String
showsPrec :: Int -> Op -> ShowS
$cshowsPrec :: Int -> Op -> ShowS
Show, ReadPrec [Op]
ReadPrec Op
Int -> ReadS Op
ReadS [Op]
(Int -> ReadS Op)
-> ReadS [Op] -> ReadPrec Op -> ReadPrec [Op] -> Read Op
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Op]
$creadListPrec :: ReadPrec [Op]
readPrec :: ReadPrec Op
$creadPrec :: ReadPrec Op
readList :: ReadS [Op]
$creadList :: ReadS [Op]
readsPrec :: Int -> ReadS Op
$creadsPrec :: Int -> ReadS Op
Read, Int -> Op
Op -> Int
Op -> [Op]
Op -> Op
Op -> Op -> [Op]
Op -> Op -> Op -> [Op]
(Op -> Op)
-> (Op -> Op)
-> (Int -> Op)
-> (Op -> Int)
-> (Op -> [Op])
-> (Op -> Op -> [Op])
-> (Op -> Op -> [Op])
-> (Op -> Op -> Op -> [Op])
-> Enum Op
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Op -> Op -> Op -> [Op]
$cenumFromThenTo :: Op -> Op -> Op -> [Op]
enumFromTo :: Op -> Op -> [Op]
$cenumFromTo :: Op -> Op -> [Op]
enumFromThen :: Op -> Op -> [Op]
$cenumFromThen :: Op -> Op -> [Op]
enumFrom :: Op -> [Op]
$cenumFrom :: Op -> [Op]
fromEnum :: Op -> Int
$cfromEnum :: Op -> Int
toEnum :: Int -> Op
$ctoEnum :: Int -> Op
pred :: Op -> Op
$cpred :: Op -> Op
succ :: Op -> Op
$csucc :: Op -> Op
Enum, Op
Op -> Op -> Bounded Op
forall a. a -> a -> Bounded a
maxBound :: Op
$cmaxBound :: Op
minBound :: Op
$cminBound :: Op
Bounded, Typeable, Typeable Op
DataType
Constr
Typeable Op
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Op -> c Op)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Op)
-> (Op -> Constr)
-> (Op -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Op))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Op))
-> ((forall b. Data b => b -> b) -> Op -> Op)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r)
-> (forall u. (forall d. Data d => d -> u) -> Op -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Op -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Op -> m Op)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Op -> m Op)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Op -> m Op)
-> Data Op
Op -> DataType
Op -> Constr
(forall b. Data b => b -> b) -> Op -> Op
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Op -> c Op
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Op
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Op -> u
forall u. (forall d. Data d => d -> u) -> Op -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Op -> m Op
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Op -> m Op
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Op
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Op -> c Op
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Op)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Op)
$cEq :: Constr
$cGe :: Constr
$tOp :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Op -> m Op
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Op -> m Op
gmapMp :: (forall d. Data d => d -> m d) -> Op -> m Op
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Op -> m Op
gmapM :: (forall d. Data d => d -> m d) -> Op -> m Op
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Op -> m Op
gmapQi :: Int -> (forall d. Data d => d -> u) -> Op -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Op -> u
gmapQ :: (forall d. Data d => d -> u) -> Op -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Op -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r
gmapT :: (forall b. Data b => b -> b) -> Op -> Op
$cgmapT :: (forall b. Data b => b -> b) -> Op -> Op
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Op)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Op)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Op)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Op)
dataTypeOf :: Op -> DataType
$cdataTypeOf :: Op -> DataType
toConstr :: Op -> Constr
$ctoConstr :: Op -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Op
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Op
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Op -> c Op
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Op -> c Op
$cp1Data :: Typeable Op
Data, (forall x. Op -> Rep Op x)
-> (forall x. Rep Op x -> Op) -> Generic Op
forall x. Rep Op x -> Op
forall x. Op -> Rep Op x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Op x -> Op
$cfrom :: forall x. Op -> Rep Op x
Generic)

instance NFData Op
instance Hashable Op

-- | A pair of /top cost/ and a list of soft constraints.
data SoftFormula
  = SoftFormula
  { SoftFormula -> Maybe Integer
wboTopCost :: Maybe Integer
  , SoftFormula -> [SoftConstraint]
wboConstraints :: [SoftConstraint]
  , SoftFormula -> Int
wboNumVars :: !Int
  , SoftFormula -> Int
wboNumConstraints :: !Int
  }
  deriving (SoftFormula -> SoftFormula -> Bool
(SoftFormula -> SoftFormula -> Bool)
-> (SoftFormula -> SoftFormula -> Bool) -> Eq SoftFormula
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SoftFormula -> SoftFormula -> Bool
$c/= :: SoftFormula -> SoftFormula -> Bool
== :: SoftFormula -> SoftFormula -> Bool
$c== :: SoftFormula -> SoftFormula -> Bool
Eq, Eq SoftFormula
Eq SoftFormula
-> (SoftFormula -> SoftFormula -> Ordering)
-> (SoftFormula -> SoftFormula -> Bool)
-> (SoftFormula -> SoftFormula -> Bool)
-> (SoftFormula -> SoftFormula -> Bool)
-> (SoftFormula -> SoftFormula -> Bool)
-> (SoftFormula -> SoftFormula -> SoftFormula)
-> (SoftFormula -> SoftFormula -> SoftFormula)
-> Ord SoftFormula
SoftFormula -> SoftFormula -> Bool
SoftFormula -> SoftFormula -> Ordering
SoftFormula -> SoftFormula -> SoftFormula
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SoftFormula -> SoftFormula -> SoftFormula
$cmin :: SoftFormula -> SoftFormula -> SoftFormula
max :: SoftFormula -> SoftFormula -> SoftFormula
$cmax :: SoftFormula -> SoftFormula -> SoftFormula
>= :: SoftFormula -> SoftFormula -> Bool
$c>= :: SoftFormula -> SoftFormula -> Bool
> :: SoftFormula -> SoftFormula -> Bool
$c> :: SoftFormula -> SoftFormula -> Bool
<= :: SoftFormula -> SoftFormula -> Bool
$c<= :: SoftFormula -> SoftFormula -> Bool
< :: SoftFormula -> SoftFormula -> Bool
$c< :: SoftFormula -> SoftFormula -> Bool
compare :: SoftFormula -> SoftFormula -> Ordering
$ccompare :: SoftFormula -> SoftFormula -> Ordering
$cp1Ord :: Eq SoftFormula
Ord, Int -> SoftFormula -> ShowS
[SoftFormula] -> ShowS
SoftFormula -> String
(Int -> SoftFormula -> ShowS)
-> (SoftFormula -> String)
-> ([SoftFormula] -> ShowS)
-> Show SoftFormula
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SoftFormula] -> ShowS
$cshowList :: [SoftFormula] -> ShowS
show :: SoftFormula -> String
$cshow :: SoftFormula -> String
showsPrec :: Int -> SoftFormula -> ShowS
$cshowsPrec :: Int -> SoftFormula -> ShowS
Show, ReadPrec [SoftFormula]
ReadPrec SoftFormula
Int -> ReadS SoftFormula
ReadS [SoftFormula]
(Int -> ReadS SoftFormula)
-> ReadS [SoftFormula]
-> ReadPrec SoftFormula
-> ReadPrec [SoftFormula]
-> Read SoftFormula
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [SoftFormula]
$creadListPrec :: ReadPrec [SoftFormula]
readPrec :: ReadPrec SoftFormula
$creadPrec :: ReadPrec SoftFormula
readList :: ReadS [SoftFormula]
$creadList :: ReadS [SoftFormula]
readsPrec :: Int -> ReadS SoftFormula
$creadsPrec :: Int -> ReadS SoftFormula
Read, Typeable, Typeable SoftFormula
DataType
Constr
Typeable SoftFormula
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> SoftFormula -> c SoftFormula)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SoftFormula)
-> (SoftFormula -> Constr)
-> (SoftFormula -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SoftFormula))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c SoftFormula))
-> ((forall b. Data b => b -> b) -> SoftFormula -> SoftFormula)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SoftFormula -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SoftFormula -> r)
-> (forall u. (forall d. Data d => d -> u) -> SoftFormula -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> SoftFormula -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SoftFormula -> m SoftFormula)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SoftFormula -> m SoftFormula)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SoftFormula -> m SoftFormula)
-> Data SoftFormula
SoftFormula -> DataType
SoftFormula -> Constr
(forall b. Data b => b -> b) -> SoftFormula -> SoftFormula
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SoftFormula -> c SoftFormula
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SoftFormula
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> SoftFormula -> u
forall u. (forall d. Data d => d -> u) -> SoftFormula -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SoftFormula -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SoftFormula -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SoftFormula -> m SoftFormula
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SoftFormula -> m SoftFormula
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SoftFormula
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SoftFormula -> c SoftFormula
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SoftFormula)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SoftFormula)
$cSoftFormula :: Constr
$tSoftFormula :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> SoftFormula -> m SoftFormula
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SoftFormula -> m SoftFormula
gmapMp :: (forall d. Data d => d -> m d) -> SoftFormula -> m SoftFormula
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SoftFormula -> m SoftFormula
gmapM :: (forall d. Data d => d -> m d) -> SoftFormula -> m SoftFormula
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SoftFormula -> m SoftFormula
gmapQi :: Int -> (forall d. Data d => d -> u) -> SoftFormula -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SoftFormula -> u
gmapQ :: (forall d. Data d => d -> u) -> SoftFormula -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SoftFormula -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SoftFormula -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SoftFormula -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SoftFormula -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SoftFormula -> r
gmapT :: (forall b. Data b => b -> b) -> SoftFormula -> SoftFormula
$cgmapT :: (forall b. Data b => b -> b) -> SoftFormula -> SoftFormula
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SoftFormula)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SoftFormula)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c SoftFormula)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SoftFormula)
dataTypeOf :: SoftFormula -> DataType
$cdataTypeOf :: SoftFormula -> DataType
toConstr :: SoftFormula -> Constr
$ctoConstr :: SoftFormula -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SoftFormula
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SoftFormula
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SoftFormula -> c SoftFormula
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SoftFormula -> c SoftFormula
$cp1Data :: Typeable SoftFormula
Data, (forall x. SoftFormula -> Rep SoftFormula x)
-> (forall x. Rep SoftFormula x -> SoftFormula)
-> Generic SoftFormula
forall x. Rep SoftFormula x -> SoftFormula
forall x. SoftFormula -> Rep SoftFormula x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SoftFormula x -> SoftFormula
$cfrom :: forall x. SoftFormula -> Rep SoftFormula x
Generic)

instance NFData SoftFormula
instance Hashable SoftFormula

-- | A pair of weight and constraint.
type SoftConstraint = (Maybe Integer, Constraint)

-- | Sum of 'WeightedTerm'
type Sum = [WeightedTerm]

-- | Coefficient and 'Term'
type WeightedTerm = (Integer, Term)

-- | List of variables interpreted as products
type Term = [Lit]

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

-- | Variable are repserented as positive integers.
type Var = Int

-- | Utility function for computing number of variables in given objective function and constraints.
pbComputeNumVars :: Maybe Sum -> [Constraint] -> Int
pbComputeNumVars :: Maybe Sum -> [Constraint] -> Int
pbComputeNumVars Maybe Sum
obj [Constraint]
cs = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
vs)
  where
    vs :: [Int]
vs = do
      Sum
s <- Maybe Sum -> [Sum]
forall a. Maybe a -> [a]
maybeToList Maybe Sum
obj [Sum] -> [Sum] -> [Sum]
forall a. [a] -> [a] -> [a]
++ [Sum
s | (Sum
s,Op
_,Integer
_) <- [Constraint]
cs]
      (Integer
_, [Int]
tm) <- Sum
s
      Int
lit <- [Int]
tm
      Int -> [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [Int]) -> Int -> [Int]
forall a b. (a -> b) -> a -> b
$ Int -> Int
forall a. Num a => a -> a
abs Int
lit

-- | Utility function for computing number of variables in given objective function and constraints.
wboComputeNumVars :: [SoftConstraint] -> Int
wboComputeNumVars :: [SoftConstraint] -> Int
wboComputeNumVars [SoftConstraint]
cs = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
vs)
  where
    vs :: [Int]
vs = do
      Sum
s <- [Sum
s | (Maybe Integer
_, (Sum
s,Op
_,Integer
_)) <- [SoftConstraint]
cs]
      (Integer
_, [Int]
tm) <- Sum
s
      Int
lit <- [Int]
tm
      Int -> [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [Int]) -> Int -> [Int]
forall a b. (a -> b) -> a -> b
$ Int -> Int
forall a. Num a => a -> a
abs Int
lit

pbProducts :: Formula -> Set IntSet
pbProducts :: Formula -> Set IntSet
pbProducts Formula
formula = [IntSet] -> Set IntSet
forall a. Ord a => [a] -> Set a
Set.fromList ([IntSet] -> Set IntSet) -> [IntSet] -> Set IntSet
forall a b. (a -> b) -> a -> b
$ do  
  Sum
s <- Maybe Sum -> [Sum]
forall a. Maybe a -> [a]
maybeToList (Formula -> Maybe Sum
pbObjectiveFunction Formula
formula) [Sum] -> [Sum] -> [Sum]
forall a. [a] -> [a] -> [a]
++ [Sum
s | (Sum
s,Op
_,Integer
_) <- Formula -> [Constraint]
pbConstraints Formula
formula]
  (Integer
_, [Int]
tm)  <- Sum
s
  let tm2 :: IntSet
tm2 = [Int] -> IntSet
IntSet.fromList [Int]
tm
  Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ IntSet -> Int
IntSet.size IntSet
tm2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1
  IntSet -> [IntSet]
forall (m :: * -> *) a. Monad m => a -> m a
return IntSet
tm2

wboProducts :: SoftFormula -> Set IntSet
wboProducts :: SoftFormula -> Set IntSet
wboProducts SoftFormula
softformula = [IntSet] -> Set IntSet
forall a. Ord a => [a] -> Set a
Set.fromList ([IntSet] -> Set IntSet) -> [IntSet] -> Set IntSet
forall a b. (a -> b) -> a -> b
$ do
  (Maybe Integer
_,(Sum
s,Op
_,Integer
_)) <- SoftFormula -> [SoftConstraint]
wboConstraints SoftFormula
softformula
  (Integer
_, [Int]
tm) <- Sum
s
  let tm2 :: IntSet
tm2 = [Int] -> IntSet
IntSet.fromList [Int]
tm
  Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ IntSet -> Int
IntSet.size IntSet
tm2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1
  IntSet -> [IntSet]
forall (m :: * -> *) a. Monad m => a -> m a
return IntSet
tm2

wboNumSoft :: SoftFormula -> Int
wboNumSoft :: SoftFormula -> Int
wboNumSoft SoftFormula
softformula = [()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [() | (Just Integer
_, Constraint
_) <- SoftFormula -> [SoftConstraint]
wboConstraints SoftFormula
softformula]