{-# 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 Satyros.CNF.Literal (Literal, literalToVariable) import Satyros.CNF.Variable (Variable) newtype ClauseLike a = ClauseLike { ClauseLike a -> [a] _literalsOfClause :: [a] } 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 #-}