module Satchmo.Data
( CNF, cnf, clauses
, Clause(..), clause, literals
, Literal(..), literal, nicht
, Variable, variable, positive
)
where
import Control.Monad.State.Strict
newtype CNF = CNF { clauses :: [ Clause ] }
instance Show CNF where
show ( CNF cs ) = unlines $ map show cs
cnf :: [ Clause ] -> CNF
cnf cs = CNF cs
newtype Clause = Clause { literals :: [ Literal ] }
instance Show Clause where
show ( Clause xs ) = unwords ( map show xs ++ [ "0" ] )
clause :: [ Literal ] -> Clause
clause ls = Clause { literals = ls }
newtype Literal = Literal Int
deriving ( Eq, Ord )
instance Show Literal where
show ( Literal i ) = show i
instance Read Literal where
readsPrec p = \ cs -> do
( i, cs') <- readsPrec p cs
return ( Literal i , cs' )
literal :: Bool -> Variable -> Literal
literal p v | v /= 0 =
Literal $ if p then v else negate v
nicht :: Literal -> Literal
nicht ( Literal i ) = Literal $ negate i
type Variable = Int
variable :: Literal -> Variable
variable ( Literal v ) = abs v
positive :: Literal -> Bool
positive ( Literal v ) = 0 < v