{-# LANGUAGE BangPatterns, DeriveDataTypeable, DeriveGeneric #-}
{-# OPTIONS_GHC -Wall #-}
module Data.PseudoBoolean.Types
(
Formula (..)
, Constraint
, Op (..)
, SoftFormula (..)
, SoftConstraint
, Sum
, WeightedTerm
, Term
, Lit
, Var
, 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
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
$c== :: Formula -> Formula -> Bool
== :: Formula -> Formula -> Bool
$c/= :: Formula -> Formula -> Bool
/= :: 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
$ccompare :: Formula -> Formula -> Ordering
compare :: Formula -> Formula -> Ordering
$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
>= :: Formula -> Formula -> Bool
$cmax :: Formula -> Formula -> Formula
max :: Formula -> Formula -> Formula
$cmin :: Formula -> Formula -> Formula
min :: Formula -> Formula -> 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
$cshowsPrec :: Int -> Formula -> ShowS
showsPrec :: Int -> Formula -> ShowS
$cshow :: Formula -> String
show :: Formula -> String
$cshowList :: [Formula] -> ShowS
showList :: [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
$creadsPrec :: Int -> ReadS Formula
readsPrec :: Int -> ReadS Formula
$creadList :: ReadS [Formula]
readList :: ReadS [Formula]
$creadPrec :: ReadPrec Formula
readPrec :: ReadPrec Formula
$creadListPrec :: ReadPrec [Formula]
readListPrec :: ReadPrec [Formula]
Read, Typeable, Typeable Formula
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 -> Constr
Formula -> DataType
(forall b. Data b => b -> b) -> Formula -> 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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Formula -> c Formula
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Formula -> c Formula
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Formula
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Formula
$ctoConstr :: Formula -> Constr
toConstr :: Formula -> Constr
$cdataTypeOf :: Formula -> DataType
dataTypeOf :: Formula -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Formula)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Formula)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formula)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formula)
$cgmapT :: (forall b. Data b => b -> b) -> Formula -> Formula
gmapT :: (forall b. Data b => b -> b) -> Formula -> Formula
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r
gmapQl :: forall r r'.
(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
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Formula -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Formula -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Formula -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Formula -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Formula -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Formula -> m Formula
gmapM :: forall (m :: * -> *).
Monad m =>
(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
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(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
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Formula -> m 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
$cfrom :: forall x. Formula -> Rep Formula x
from :: forall x. Formula -> Rep Formula x
$cto :: forall x. Rep Formula x -> Formula
to :: forall x. Rep Formula x -> Formula
Generic)
instance NFData Formula
instance Hashable Formula
type Constraint = (Sum, Op, Integer)
data Op
= Ge
| Eq
deriving (Op -> Op -> Bool
(Op -> Op -> Bool) -> (Op -> Op -> Bool) -> Eq Op
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Op -> Op -> Bool
== :: Op -> Op -> Bool
$c/= :: Op -> Op -> Bool
/= :: 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
$ccompare :: Op -> Op -> Ordering
compare :: Op -> Op -> Ordering
$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
>= :: Op -> Op -> Bool
$cmax :: Op -> Op -> Op
max :: Op -> Op -> Op
$cmin :: Op -> Op -> Op
min :: Op -> Op -> 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
$cshowsPrec :: Int -> Op -> ShowS
showsPrec :: Int -> Op -> ShowS
$cshow :: Op -> String
show :: Op -> String
$cshowList :: [Op] -> ShowS
showList :: [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
$creadsPrec :: Int -> ReadS Op
readsPrec :: Int -> ReadS Op
$creadList :: ReadS [Op]
readList :: ReadS [Op]
$creadPrec :: ReadPrec Op
readPrec :: ReadPrec Op
$creadListPrec :: ReadPrec [Op]
readListPrec :: ReadPrec [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
$csucc :: Op -> Op
succ :: Op -> Op
$cpred :: Op -> Op
pred :: Op -> Op
$ctoEnum :: Int -> Op
toEnum :: Int -> Op
$cfromEnum :: Op -> Int
fromEnum :: Op -> Int
$cenumFrom :: Op -> [Op]
enumFrom :: Op -> [Op]
$cenumFromThen :: Op -> Op -> [Op]
enumFromThen :: Op -> Op -> [Op]
$cenumFromTo :: Op -> Op -> [Op]
enumFromTo :: Op -> Op -> [Op]
$cenumFromThenTo :: Op -> Op -> Op -> [Op]
enumFromThenTo :: Op -> Op -> Op -> [Op]
Enum, Op
Op -> Op -> Bounded Op
forall a. a -> a -> Bounded a
$cminBound :: Op
minBound :: Op
$cmaxBound :: Op
maxBound :: Op
Bounded, Typeable, Typeable Op
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 -> Constr
Op -> DataType
(forall b. Data b => b -> b) -> Op -> 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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Op -> c Op
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Op -> c Op
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Op
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Op
$ctoConstr :: Op -> Constr
toConstr :: Op -> Constr
$cdataTypeOf :: Op -> DataType
dataTypeOf :: Op -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Op)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Op)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Op)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Op)
$cgmapT :: (forall b. Data b => b -> b) -> Op -> Op
gmapT :: (forall b. Data b => b -> b) -> Op -> Op
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r
gmapQl :: forall r r'.
(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
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Op -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Op -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Op -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Op -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Op -> m Op
gmapM :: forall (m :: * -> *).
Monad m =>
(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
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(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
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Op -> m 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
$cfrom :: forall x. Op -> Rep Op x
from :: forall x. Op -> Rep Op x
$cto :: forall x. Rep Op x -> Op
to :: forall x. Rep Op x -> Op
Generic)
instance NFData Op
instance Hashable Op
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
$c== :: SoftFormula -> SoftFormula -> Bool
== :: SoftFormula -> SoftFormula -> Bool
$c/= :: SoftFormula -> SoftFormula -> Bool
/= :: 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
$ccompare :: SoftFormula -> SoftFormula -> Ordering
compare :: SoftFormula -> SoftFormula -> Ordering
$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
>= :: SoftFormula -> SoftFormula -> Bool
$cmax :: SoftFormula -> SoftFormula -> SoftFormula
max :: SoftFormula -> SoftFormula -> SoftFormula
$cmin :: SoftFormula -> SoftFormula -> SoftFormula
min :: SoftFormula -> SoftFormula -> 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
$cshowsPrec :: Int -> SoftFormula -> ShowS
showsPrec :: Int -> SoftFormula -> ShowS
$cshow :: SoftFormula -> String
show :: SoftFormula -> String
$cshowList :: [SoftFormula] -> ShowS
showList :: [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
$creadsPrec :: Int -> ReadS SoftFormula
readsPrec :: Int -> ReadS SoftFormula
$creadList :: ReadS [SoftFormula]
readList :: ReadS [SoftFormula]
$creadPrec :: ReadPrec SoftFormula
readPrec :: ReadPrec SoftFormula
$creadListPrec :: ReadPrec [SoftFormula]
readListPrec :: ReadPrec [SoftFormula]
Read, Typeable, Typeable SoftFormula
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 -> Constr
SoftFormula -> DataType
(forall b. Data b => b -> b) -> SoftFormula -> 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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SoftFormula -> c SoftFormula
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SoftFormula -> c SoftFormula
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SoftFormula
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SoftFormula
$ctoConstr :: SoftFormula -> Constr
toConstr :: SoftFormula -> Constr
$cdataTypeOf :: SoftFormula -> DataType
dataTypeOf :: SoftFormula -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SoftFormula)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SoftFormula)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SoftFormula)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SoftFormula)
$cgmapT :: (forall b. Data b => b -> b) -> SoftFormula -> SoftFormula
gmapT :: (forall b. Data b => b -> b) -> SoftFormula -> SoftFormula
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SoftFormula -> r
gmapQl :: forall r r'.
(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
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SoftFormula -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SoftFormula -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> SoftFormula -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SoftFormula -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SoftFormula -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SoftFormula -> m SoftFormula
gmapM :: forall (m :: * -> *).
Monad m =>
(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
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(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
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SoftFormula -> m 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
$cfrom :: forall x. SoftFormula -> Rep SoftFormula x
from :: forall x. SoftFormula -> Rep SoftFormula x
$cto :: forall x. Rep SoftFormula x -> SoftFormula
to :: forall x. Rep SoftFormula x -> SoftFormula
Generic)
instance NFData SoftFormula
instance Hashable SoftFormula
type SoftConstraint = (Maybe Integer, Constraint)
type Sum = [WeightedTerm]
type WeightedTerm = (Integer, Term)
type Term = [Lit]
type Lit = Int
type Var = Int
pbComputeNumVars :: Maybe Sum -> [Constraint] -> Int
pbComputeNumVars :: Maybe Sum -> [Constraint] -> Int
pbComputeNumVars Maybe Sum
obj [Constraint]
cs = Term -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 Int -> Term -> Term
forall a. a -> [a] -> [a]
: Term
vs)
where
vs :: Term
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
_, Term
tm) <- Sum
s
Int
lit <- Term
tm
Int -> Term
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ Int -> Int
forall a. Num a => a -> a
abs Int
lit
wboComputeNumVars :: [SoftConstraint] -> Int
wboComputeNumVars :: [SoftConstraint] -> Int
wboComputeNumVars [SoftConstraint]
cs = Term -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 Int -> Term -> Term
forall a. a -> [a] -> [a]
: Term
vs)
where
vs :: Term
vs = do
Sum
s <- [Sum
s | (Maybe Integer
_, (Sum
s,Op
_,Integer
_)) <- [SoftConstraint]
cs]
(Integer
_, Term
tm) <- Sum
s
Int
lit <- Term
tm
Int -> Term
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Term) -> Int -> Term
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
_, Term
tm) <- Sum
s
let tm2 :: IntSet
tm2 = Term -> IntSet
IntSet.fromList Term
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 a. a -> [a]
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
_, Term
tm) <- Sum
s
let tm2 :: IntSet
tm2 = Term -> IntSet
IntSet.fromList Term
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 a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return IntSet
tm2
wboNumSoft :: SoftFormula -> Int
wboNumSoft :: SoftFormula -> Int
wboNumSoft SoftFormula
softformula = [()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [() | (Just Integer
_, Constraint
_) <- SoftFormula -> [SoftConstraint]
wboConstraints SoftFormula
softformula]