{-# 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 #-}