-- 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 (Eq, 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 (Pos x) (Pos y) = compare x y
  compare (Neg x) (Neg y) = compare x y
  compare (Pos x) (Neg y) = compare (x,False) (y,True)
  compare (Neg x) (Pos y) = compare (x,True) (y,False)

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