-- | this module just defines types for formulas,
-- it is not meant to contain efficient implementations
-- for formula manipulation.

{-# language TypeFamilies #-}
{-# language GeneralizedNewtypeDeriving #-}
{-# language TemplateHaskell #-}
{-# language DeriveGeneric #-}

module Satchmo.Data 

( CNF, cnf, clauses, size
, Clause, clause, literals
, Literal, literal, nicht, positive, variable
, Variable 
)

where

import Prelude hiding ( foldr, filter )
import qualified Prelude
  
import qualified Data.Set as S
import qualified Data.Map as M
import qualified Data.Foldable as F
import Data.Monoid
import Data.List ( nub )
-- import Data.Function.Memoize

import GHC.Generics (Generic)
import Data.Hashable

-- * variables and literals

type Variable = Int

data Literal =
     Literal { Literal -> Variable
variable :: !Variable
             , Literal -> Bool
positive :: !Bool
             }
     deriving ( Literal -> Literal -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Literal -> Literal -> Bool
$c/= :: Literal -> Literal -> Bool
== :: Literal -> Literal -> Bool
$c== :: Literal -> Literal -> Bool
Eq, Eq Literal
Literal -> Literal -> Bool
Literal -> Literal -> Ordering
Literal -> Literal -> Literal
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 :: Literal -> Literal -> Literal
$cmin :: Literal -> Literal -> Literal
max :: Literal -> Literal -> Literal
$cmax :: Literal -> Literal -> Literal
>= :: Literal -> Literal -> Bool
$c>= :: Literal -> Literal -> Bool
> :: Literal -> Literal -> Bool
$c> :: Literal -> Literal -> Bool
<= :: Literal -> Literal -> Bool
$c<= :: Literal -> Literal -> Bool
< :: Literal -> Literal -> Bool
$c< :: Literal -> Literal -> Bool
compare :: Literal -> Literal -> Ordering
$ccompare :: Literal -> Literal -> Ordering
Ord, forall x. Rep Literal x -> Literal
forall x. Literal -> Rep Literal x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Literal x -> Literal
$cfrom :: forall x. Literal -> Rep Literal x
Generic )

instance Hashable Literal

--  $(deriveMemoizable ''Literal)

instance Show Literal where
    show :: Literal -> String
show Literal
l = ( if Literal -> Bool
positive Literal
l then String
"" else String
"-" )
             forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ( Literal -> Variable
variable Literal
l )

literal :: Bool -> Variable -> Literal
literal :: Bool -> Variable -> Literal
literal Bool
pos Variable
v  = Literal { positive :: Bool
positive = Bool
pos, variable :: Variable
variable = Variable
v }

nicht :: Literal -> Literal 
nicht :: Literal -> Literal
nicht Literal
x = Literal
x { positive :: Bool
positive = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Literal -> Bool
positive Literal
x }

-- * clauses

newtype Clause = Clause { Clause -> [Literal]
literals :: [Literal] }
   deriving ( Clause -> Clause -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Clause -> Clause -> Bool
$c/= :: Clause -> Clause -> Bool
== :: Clause -> Clause -> Bool
$c== :: Clause -> Clause -> Bool
Eq, Eq Clause
Clause -> Clause -> Bool
Clause -> Clause -> Ordering
Clause -> Clause -> Clause
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 :: Clause -> Clause -> Clause
$cmin :: Clause -> Clause -> Clause
max :: Clause -> Clause -> Clause
$cmax :: Clause -> Clause -> Clause
>= :: Clause -> Clause -> Bool
$c>= :: Clause -> Clause -> Bool
> :: Clause -> Clause -> Bool
$c> :: Clause -> Clause -> Bool
<= :: Clause -> Clause -> Bool
$c<= :: Clause -> Clause -> Bool
< :: Clause -> Clause -> Bool
$c< :: Clause -> Clause -> Bool
compare :: Clause -> Clause -> Ordering
$ccompare :: Clause -> Clause -> Ordering
Ord )

instance Show ( Clause ) where
  show :: Clause -> String
show Clause
c = [String] -> String
unwords ( forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show (Clause -> [Literal]
literals Clause
c) forall a. [a] -> [a] -> [a]
++ [ String
"0" ] )

clause ::  [ Literal ] -> Clause 
clause :: [Literal] -> Clause
clause [Literal]
ls = [Literal] -> Clause
Clause [Literal]
ls 

-- * formulas

newtype CNF  = CNF { CNF -> [Clause]
clauses :: [ Clause ] }

size :: CNF -> Variable
size (CNF [Clause]
s) = forall (t :: * -> *) a. Foldable t => t a -> Variable
length [Clause]
s
                   
instance Show CNF  where
    show :: CNF -> String
show CNF
cnf = [String] -> String
unlines forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ CNF -> [Clause]
clauses CNF
cnf

cnf :: [ Clause ] -> CNF 
cnf :: [Clause] -> CNF
cnf [Clause]
cs = [Clause] -> CNF
CNF [Clause]
cs