{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TemplateHaskell #-}
module Satyros.CNF.Formula
  ( FormulaLike(Formula, FormulaLike)
  , Formula
  , clauseLikesOfFormulaLike
  , clausesOfFormula
  , maxVariableInFormula
  ) where

import           Control.Lens         (Iso', _Wrapped, makeWrapped)
import           GHC.Generics         (Generic, Generic1)
import           Satyros.CNF.Clause   (Clause, ClauseLike, maxVariableInClause)
import           Satyros.CNF.Literal  (Literal)
import           Satyros.CNF.Variable (Variable)

newtype FormulaLike a = FormulaLike { FormulaLike a -> [ClauseLike a]
_clausesOfFormula :: [ClauseLike a] }
  deriving stock ((forall x. FormulaLike a -> Rep (FormulaLike a) x)
-> (forall x. Rep (FormulaLike a) x -> FormulaLike a)
-> Generic (FormulaLike a)
forall x. Rep (FormulaLike a) x -> FormulaLike a
forall x. FormulaLike a -> Rep (FormulaLike a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (FormulaLike a) x -> FormulaLike a
forall a x. FormulaLike a -> Rep (FormulaLike a) x
$cto :: forall a x. Rep (FormulaLike a) x -> FormulaLike a
$cfrom :: forall a x. FormulaLike a -> Rep (FormulaLike a) x
Generic, (forall a. FormulaLike a -> Rep1 FormulaLike a)
-> (forall a. Rep1 FormulaLike a -> FormulaLike a)
-> Generic1 FormulaLike
forall a. Rep1 FormulaLike a -> FormulaLike a
forall a. FormulaLike a -> Rep1 FormulaLike 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 FormulaLike a -> FormulaLike a
$cfrom1 :: forall a. FormulaLike a -> Rep1 FormulaLike a
Generic1, FormulaLike a -> FormulaLike a -> Bool
(FormulaLike a -> FormulaLike a -> Bool)
-> (FormulaLike a -> FormulaLike a -> Bool) -> Eq (FormulaLike a)
forall a. Eq a => FormulaLike a -> FormulaLike a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FormulaLike a -> FormulaLike a -> Bool
$c/= :: forall a. Eq a => FormulaLike a -> FormulaLike a -> Bool
== :: FormulaLike a -> FormulaLike a -> Bool
$c== :: forall a. Eq a => FormulaLike a -> FormulaLike a -> Bool
Eq, Eq (FormulaLike a)
Eq (FormulaLike a)
-> (FormulaLike a -> FormulaLike a -> Ordering)
-> (FormulaLike a -> FormulaLike a -> Bool)
-> (FormulaLike a -> FormulaLike a -> Bool)
-> (FormulaLike a -> FormulaLike a -> Bool)
-> (FormulaLike a -> FormulaLike a -> Bool)
-> (FormulaLike a -> FormulaLike a -> FormulaLike a)
-> (FormulaLike a -> FormulaLike a -> FormulaLike a)
-> Ord (FormulaLike a)
FormulaLike a -> FormulaLike a -> Bool
FormulaLike a -> FormulaLike a -> Ordering
FormulaLike a -> FormulaLike a -> FormulaLike 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 (FormulaLike a)
forall a. Ord a => FormulaLike a -> FormulaLike a -> Bool
forall a. Ord a => FormulaLike a -> FormulaLike a -> Ordering
forall a. Ord a => FormulaLike a -> FormulaLike a -> FormulaLike a
min :: FormulaLike a -> FormulaLike a -> FormulaLike a
$cmin :: forall a. Ord a => FormulaLike a -> FormulaLike a -> FormulaLike a
max :: FormulaLike a -> FormulaLike a -> FormulaLike a
$cmax :: forall a. Ord a => FormulaLike a -> FormulaLike a -> FormulaLike a
>= :: FormulaLike a -> FormulaLike a -> Bool
$c>= :: forall a. Ord a => FormulaLike a -> FormulaLike a -> Bool
> :: FormulaLike a -> FormulaLike a -> Bool
$c> :: forall a. Ord a => FormulaLike a -> FormulaLike a -> Bool
<= :: FormulaLike a -> FormulaLike a -> Bool
$c<= :: forall a. Ord a => FormulaLike a -> FormulaLike a -> Bool
< :: FormulaLike a -> FormulaLike a -> Bool
$c< :: forall a. Ord a => FormulaLike a -> FormulaLike a -> Bool
compare :: FormulaLike a -> FormulaLike a -> Ordering
$ccompare :: forall a. Ord a => FormulaLike a -> FormulaLike a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (FormulaLike a)
Ord)
  deriving newtype (Int -> FormulaLike a -> ShowS
[FormulaLike a] -> ShowS
FormulaLike a -> String
(Int -> FormulaLike a -> ShowS)
-> (FormulaLike a -> String)
-> ([FormulaLike a] -> ShowS)
-> Show (FormulaLike a)
forall a. Show a => Int -> FormulaLike a -> ShowS
forall a. Show a => [FormulaLike a] -> ShowS
forall a. Show a => FormulaLike a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FormulaLike a] -> ShowS
$cshowList :: forall a. Show a => [FormulaLike a] -> ShowS
show :: FormulaLike a -> String
$cshow :: forall a. Show a => FormulaLike a -> String
showsPrec :: Int -> FormulaLike a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> FormulaLike a -> ShowS
Show, b -> FormulaLike a -> FormulaLike a
NonEmpty (FormulaLike a) -> FormulaLike a
FormulaLike a -> FormulaLike a -> FormulaLike a
(FormulaLike a -> FormulaLike a -> FormulaLike a)
-> (NonEmpty (FormulaLike a) -> FormulaLike a)
-> (forall b. Integral b => b -> FormulaLike a -> FormulaLike a)
-> Semigroup (FormulaLike a)
forall b. Integral b => b -> FormulaLike a -> FormulaLike a
forall a. NonEmpty (FormulaLike a) -> FormulaLike a
forall a. FormulaLike a -> FormulaLike a -> FormulaLike a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall a b. Integral b => b -> FormulaLike a -> FormulaLike a
stimes :: b -> FormulaLike a -> FormulaLike a
$cstimes :: forall a b. Integral b => b -> FormulaLike a -> FormulaLike a
sconcat :: NonEmpty (FormulaLike a) -> FormulaLike a
$csconcat :: forall a. NonEmpty (FormulaLike a) -> FormulaLike a
<> :: FormulaLike a -> FormulaLike a -> FormulaLike a
$c<> :: forall a. FormulaLike a -> FormulaLike a -> FormulaLike a
Semigroup, Semigroup (FormulaLike a)
FormulaLike a
Semigroup (FormulaLike a)
-> FormulaLike a
-> (FormulaLike a -> FormulaLike a -> FormulaLike a)
-> ([FormulaLike a] -> FormulaLike a)
-> Monoid (FormulaLike a)
[FormulaLike a] -> FormulaLike a
FormulaLike a -> FormulaLike a -> FormulaLike a
forall a. Semigroup (FormulaLike a)
forall a. FormulaLike a
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall a. [FormulaLike a] -> FormulaLike a
forall a. FormulaLike a -> FormulaLike a -> FormulaLike a
mconcat :: [FormulaLike a] -> FormulaLike a
$cmconcat :: forall a. [FormulaLike a] -> FormulaLike a
mappend :: FormulaLike a -> FormulaLike a -> FormulaLike a
$cmappend :: forall a. FormulaLike a -> FormulaLike a -> FormulaLike a
mempty :: FormulaLike a
$cmempty :: forall a. FormulaLike a
$cp1Monoid :: forall a. Semigroup (FormulaLike a)
Monoid)

makeWrapped ''FormulaLike

type Formula = FormulaLike Literal

pattern Formula :: [Clause] -> Formula
pattern $bFormula :: [Clause] -> Formula
$mFormula :: forall r. Formula -> ([Clause] -> r) -> (Void# -> r) -> r
Formula v = FormulaLike v
{-# COMPLETE Formula #-}

clauseLikesOfFormulaLike :: Iso' (FormulaLike a) [ClauseLike a]
clauseLikesOfFormulaLike :: p [ClauseLike a] (f [ClauseLike a])
-> p (FormulaLike a) (f (FormulaLike a))
clauseLikesOfFormulaLike = p [ClauseLike a] (f [ClauseLike a])
-> p (FormulaLike a) (f (FormulaLike a))
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped
{-# INLINE clauseLikesOfFormulaLike #-}

clausesOfFormula :: Iso' Formula [Clause]
clausesOfFormula :: p [Clause] (f [Clause]) -> p Formula (f Formula)
clausesOfFormula = p [Clause] (f [Clause]) -> p Formula (f Formula)
forall a. Iso' (FormulaLike a) [ClauseLike a]
clauseLikesOfFormulaLike
{-# INLINE clausesOfFormula #-}

maxVariableInFormula :: Formula -> Variable
maxVariableInFormula :: Formula -> Variable
maxVariableInFormula = [Variable] -> Variable
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Variable] -> Variable)
-> (Formula -> [Variable]) -> Formula -> Variable
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Clause -> Variable) -> [Clause] -> [Variable]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Clause -> Variable
maxVariableInClause ([Clause] -> [Variable])
-> (Formula -> [Clause]) -> Formula -> [Variable]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula -> [Clause]
forall a. FormulaLike a -> [ClauseLike a]
_clausesOfFormula
{-# INLINE maxVariableInFormula #-}