-- | 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
(Literal -> Literal -> Bool)
-> (Literal -> Literal -> Bool) -> Eq Literal
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Literal -> Literal -> Bool
== :: Literal -> Literal -> Bool
$c/= :: Literal -> Literal -> Bool
/= :: Literal -> Literal -> Bool
Eq, Eq Literal
Eq Literal =>
(Literal -> Literal -> Ordering)
-> (Literal -> Literal -> Bool)
-> (Literal -> Literal -> Bool)
-> (Literal -> Literal -> Bool)
-> (Literal -> Literal -> Bool)
-> (Literal -> Literal -> Literal)
-> (Literal -> Literal -> Literal)
-> Ord 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
$ccompare :: Literal -> Literal -> Ordering
compare :: Literal -> Literal -> Ordering
$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
>= :: Literal -> Literal -> Bool
$cmax :: Literal -> Literal -> Literal
max :: Literal -> Literal -> Literal
$cmin :: Literal -> Literal -> Literal
min :: Literal -> Literal -> Literal
Ord, (forall x. Literal -> Rep Literal x)
-> (forall x. Rep Literal x -> Literal) -> Generic Literal
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
$cfrom :: forall x. Literal -> Rep Literal x
from :: forall x. Literal -> Rep Literal x
$cto :: forall x. Rep Literal x -> Literal
to :: forall x. Rep Literal x -> Literal
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
"-" )
             String -> ShowS
forall a. [a] -> [a] -> [a]
++ Variable -> String
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 = not $ positive x }

-- * clauses

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

instance Show ( Clause ) where
  show :: Clause -> String
show Clause
c = [String] -> String
unwords ( (Literal -> String) -> [Literal] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Literal -> String
forall a. Show a => a -> String
show (Clause -> [Literal]
literals Clause
c) [String] -> [String] -> [String]
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) = [Clause] -> Variable
forall a. [a] -> Variable
forall (t :: * -> *) a. Foldable t => t a -> Variable
length [Clause]
s
                   
instance Show CNF  where
    show :: CNF -> String
show CNF
cnf = [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Clause -> String) -> [Clause] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> String
forall a. Show a => a -> String
show ([Clause] -> [String]) -> [Clause] -> [String]
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