-- Copyright (C) 2016 Peter Selinger.
--
-- This file is free software and may be distributed under the terms
-- of the MIT license. Please see the file LICENSE for details.

-- | This module provides a type of literals. 

module SAT.MiniSat.Literals where

-- | A literal is a positive or negative atom.
data Lit a = Pos a | Neg a
           deriving (Lit a -> Lit a -> Bool
(Lit a -> Lit a -> Bool) -> (Lit a -> Lit a -> Bool) -> Eq (Lit a)
forall a. Eq a => Lit a -> Lit a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Lit a -> Lit a -> Bool
== :: Lit a -> Lit a -> Bool
$c/= :: forall a. Eq a => Lit a -> Lit a -> Bool
/= :: Lit a -> Lit a -> Bool
Eq, Int -> Lit a -> ShowS
[Lit a] -> ShowS
Lit a -> String
(Int -> Lit a -> ShowS)
-> (Lit a -> String) -> ([Lit a] -> ShowS) -> Show (Lit a)
forall a. Show a => Int -> Lit a -> ShowS
forall a. Show a => [Lit a] -> ShowS
forall a. Show a => Lit a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Lit a -> ShowS
showsPrec :: Int -> Lit a -> ShowS
$cshow :: forall a. Show a => Lit a -> String
show :: Lit a -> String
$cshowList :: forall a. Show a => [Lit a] -> ShowS
showList :: [Lit a] -> ShowS
Show)

-- | We order literals first by variable, then by sign, so that dual
-- literals are neighbors in the ordering.
instance (Ord a) => Ord (Lit a) where
  compare :: Lit a -> Lit a -> Ordering
compare (Pos a
x) (Pos a
y) = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
x a
y
  compare (Neg a
x) (Neg a
y) = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
x a
y
  compare (Pos a
x) (Neg a
y) = (a, Bool) -> (a, Bool) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (a
x,Bool
False) (a
y,Bool
True)
  compare (Neg a
x) (Pos a
y) = (a, Bool) -> (a, Bool) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (a
x,Bool
True) (a
y,Bool
False)

-- | Negate a literal.
neg :: Lit a -> Lit a
neg :: forall a. Lit a -> Lit a
neg (Pos a
a) = a -> Lit a
forall a. a -> Lit a
Neg a
a
neg (Neg a
a) = a -> Lit a
forall a. a -> Lit a
Pos a
a