{-# 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
/= :: 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
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
/= :: 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
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
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 = [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
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]