{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE TemplateHaskell #-} module Satyros.CNF.Clause ( ClauseLike(Clause, ClauseLike) , Clause , entriesOfClauseLike , literalsOfClause , emptyClause , unitClause , maxVariableInClause ) where import Control.Lens (Iso', _Wrapped, makeWrapped) import GHC.Generics (Generic, Generic1) import Satyros.CNF.Literal (Literal, literalToVariable) import Satyros.CNF.Variable (Variable) newtype ClauseLike a = ClauseLike { ClauseLike a -> [a] _literalsOfClause :: [a] } deriving stock ((forall x. ClauseLike a -> Rep (ClauseLike a) x) -> (forall x. Rep (ClauseLike a) x -> ClauseLike a) -> Generic (ClauseLike a) forall x. Rep (ClauseLike a) x -> ClauseLike a forall x. ClauseLike a -> Rep (ClauseLike a) x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a forall a x. Rep (ClauseLike a) x -> ClauseLike a forall a x. ClauseLike a -> Rep (ClauseLike a) x $cto :: forall a x. Rep (ClauseLike a) x -> ClauseLike a $cfrom :: forall a x. ClauseLike a -> Rep (ClauseLike a) x Generic, (forall a. ClauseLike a -> Rep1 ClauseLike a) -> (forall a. Rep1 ClauseLike a -> ClauseLike a) -> Generic1 ClauseLike forall a. Rep1 ClauseLike a -> ClauseLike a forall a. ClauseLike a -> Rep1 ClauseLike a forall k (f :: k -> *). (forall (a :: k). f a -> Rep1 f a) -> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f $cto1 :: forall a. Rep1 ClauseLike a -> ClauseLike a $cfrom1 :: forall a. ClauseLike a -> Rep1 ClauseLike a Generic1, ClauseLike a -> ClauseLike a -> Bool (ClauseLike a -> ClauseLike a -> Bool) -> (ClauseLike a -> ClauseLike a -> Bool) -> Eq (ClauseLike a) forall a. Eq a => ClauseLike a -> ClauseLike a -> Bool forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: ClauseLike a -> ClauseLike a -> Bool $c/= :: forall a. Eq a => ClauseLike a -> ClauseLike a -> Bool == :: ClauseLike a -> ClauseLike a -> Bool $c== :: forall a. Eq a => ClauseLike a -> ClauseLike a -> Bool Eq, Eq (ClauseLike a) Eq (ClauseLike a) -> (ClauseLike a -> ClauseLike a -> Ordering) -> (ClauseLike a -> ClauseLike a -> Bool) -> (ClauseLike a -> ClauseLike a -> Bool) -> (ClauseLike a -> ClauseLike a -> Bool) -> (ClauseLike a -> ClauseLike a -> Bool) -> (ClauseLike a -> ClauseLike a -> ClauseLike a) -> (ClauseLike a -> ClauseLike a -> ClauseLike a) -> Ord (ClauseLike a) ClauseLike a -> ClauseLike a -> Bool ClauseLike a -> ClauseLike a -> Ordering ClauseLike a -> ClauseLike a -> ClauseLike a 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 forall a. Ord a => Eq (ClauseLike a) forall a. Ord a => ClauseLike a -> ClauseLike a -> Bool forall a. Ord a => ClauseLike a -> ClauseLike a -> Ordering forall a. Ord a => ClauseLike a -> ClauseLike a -> ClauseLike a min :: ClauseLike a -> ClauseLike a -> ClauseLike a $cmin :: forall a. Ord a => ClauseLike a -> ClauseLike a -> ClauseLike a max :: ClauseLike a -> ClauseLike a -> ClauseLike a $cmax :: forall a. Ord a => ClauseLike a -> ClauseLike a -> ClauseLike a >= :: ClauseLike a -> ClauseLike a -> Bool $c>= :: forall a. Ord a => ClauseLike a -> ClauseLike a -> Bool > :: ClauseLike a -> ClauseLike a -> Bool $c> :: forall a. Ord a => ClauseLike a -> ClauseLike a -> Bool <= :: ClauseLike a -> ClauseLike a -> Bool $c<= :: forall a. Ord a => ClauseLike a -> ClauseLike a -> Bool < :: ClauseLike a -> ClauseLike a -> Bool $c< :: forall a. Ord a => ClauseLike a -> ClauseLike a -> Bool compare :: ClauseLike a -> ClauseLike a -> Ordering $ccompare :: forall a. Ord a => ClauseLike a -> ClauseLike a -> Ordering $cp1Ord :: forall a. Ord a => Eq (ClauseLike a) Ord) deriving newtype (Int -> ClauseLike a -> ShowS [ClauseLike a] -> ShowS ClauseLike a -> String (Int -> ClauseLike a -> ShowS) -> (ClauseLike a -> String) -> ([ClauseLike a] -> ShowS) -> Show (ClauseLike a) forall a. Show a => Int -> ClauseLike a -> ShowS forall a. Show a => [ClauseLike a] -> ShowS forall a. Show a => ClauseLike a -> String forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [ClauseLike a] -> ShowS $cshowList :: forall a. Show a => [ClauseLike a] -> ShowS show :: ClauseLike a -> String $cshow :: forall a. Show a => ClauseLike a -> String showsPrec :: Int -> ClauseLike a -> ShowS $cshowsPrec :: forall a. Show a => Int -> ClauseLike a -> ShowS Show, b -> ClauseLike a -> ClauseLike a NonEmpty (ClauseLike a) -> ClauseLike a ClauseLike a -> ClauseLike a -> ClauseLike a (ClauseLike a -> ClauseLike a -> ClauseLike a) -> (NonEmpty (ClauseLike a) -> ClauseLike a) -> (forall b. Integral b => b -> ClauseLike a -> ClauseLike a) -> Semigroup (ClauseLike a) forall b. Integral b => b -> ClauseLike a -> ClauseLike a forall a. NonEmpty (ClauseLike a) -> ClauseLike a forall a. ClauseLike a -> ClauseLike a -> ClauseLike a forall a. (a -> a -> a) -> (NonEmpty a -> a) -> (forall b. Integral b => b -> a -> a) -> Semigroup a forall a b. Integral b => b -> ClauseLike a -> ClauseLike a stimes :: b -> ClauseLike a -> ClauseLike a $cstimes :: forall a b. Integral b => b -> ClauseLike a -> ClauseLike a sconcat :: NonEmpty (ClauseLike a) -> ClauseLike a $csconcat :: forall a. NonEmpty (ClauseLike a) -> ClauseLike a <> :: ClauseLike a -> ClauseLike a -> ClauseLike a $c<> :: forall a. ClauseLike a -> ClauseLike a -> ClauseLike a Semigroup, Semigroup (ClauseLike a) ClauseLike a Semigroup (ClauseLike a) -> ClauseLike a -> (ClauseLike a -> ClauseLike a -> ClauseLike a) -> ([ClauseLike a] -> ClauseLike a) -> Monoid (ClauseLike a) [ClauseLike a] -> ClauseLike a ClauseLike a -> ClauseLike a -> ClauseLike a forall a. Semigroup (ClauseLike a) forall a. ClauseLike a forall a. Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a forall a. [ClauseLike a] -> ClauseLike a forall a. ClauseLike a -> ClauseLike a -> ClauseLike a mconcat :: [ClauseLike a] -> ClauseLike a $cmconcat :: forall a. [ClauseLike a] -> ClauseLike a mappend :: ClauseLike a -> ClauseLike a -> ClauseLike a $cmappend :: forall a. ClauseLike a -> ClauseLike a -> ClauseLike a mempty :: ClauseLike a $cmempty :: forall a. ClauseLike a $cp1Monoid :: forall a. Semigroup (ClauseLike a) Monoid) makeWrapped ''ClauseLike type Clause = ClauseLike Literal pattern Clause :: [Literal] -> Clause pattern $bClause :: [Literal] -> Clause $mClause :: forall r. Clause -> ([Literal] -> r) -> (Void# -> r) -> r Clause v = ClauseLike v {-# COMPLETE Clause #-} entriesOfClauseLike :: Iso' (ClauseLike a) [a] entriesOfClauseLike :: p [a] (f [a]) -> p (ClauseLike a) (f (ClauseLike a)) entriesOfClauseLike = p [a] (f [a]) -> p (ClauseLike a) (f (ClauseLike a)) forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t) _Wrapped {-# INLINE entriesOfClauseLike #-} literalsOfClause :: Iso' Clause [Literal] literalsOfClause :: p [Literal] (f [Literal]) -> p Clause (f Clause) literalsOfClause = p [Literal] (f [Literal]) -> p Clause (f Clause) forall a. Iso' (ClauseLike a) [a] entriesOfClauseLike {-# INLINE literalsOfClause #-} emptyClause :: Clause -> Bool emptyClause :: Clause -> Bool emptyClause (Clause []) = Bool True emptyClause Clause _ = Bool False {-# INLINE emptyClause #-} unitClause :: Clause -> Bool unitClause :: Clause -> Bool unitClause (Clause [Literal _]) = Bool True unitClause Clause _ = Bool False {-# INLINE unitClause #-} maxVariableInClause :: Clause -> Variable maxVariableInClause :: Clause -> Variable maxVariableInClause = [Variable] -> Variable forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a maximum ([Variable] -> Variable) -> (Clause -> [Variable]) -> Clause -> Variable forall b c a. (b -> c) -> (a -> b) -> a -> c . (Literal -> Variable) -> [Literal] -> [Variable] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap Literal -> Variable literalToVariable ([Literal] -> [Variable]) -> (Clause -> [Literal]) -> Clause -> [Variable] forall b c a. (b -> c) -> (a -> b) -> a -> c . Clause -> [Literal] forall a. ClauseLike a -> [a] _literalsOfClause {-# INLINE maxVariableInClause #-}