{-# LANGUAGE BangPatterns, FlexibleInstances, ViewPatterns, UndecidableInstances #-}
{-# LANGUAGE Safe #-}
module SAT.Mios.Util.BoolExp
(
BoolComponent (..)
, BoolForm (..)
, (-|-)
, (-&-)
, (-=-)
, (-!-)
, (->-)
, neg
, disjunctionOf
, (-|||-)
, conjunctionOf
, (-&&&-)
, asList
, asList_
, asLatex
, asLatex_
, numberOfVariables
, numberOfClauses
, tseitinBase
)
where
import Data.List (foldl', intercalate)
tseitinBase :: Int
tseitinBase = 1600000
data L = L Int
class BoolComponent a where
toBF :: a -> BoolForm
data BoolForm = Cnf (Int, Int) [[Int]]
deriving (Eq, Show)
instance BoolComponent Int where
toBF a = Cnf (abs a, max tseitinBase (abs a)) [[a]]
instance BoolComponent L where
toBF (L a) = Cnf (abs a, max tseitinBase (abs a)) [[a]]
instance BoolComponent [Char] where
toBF (read -> a) = Cnf (abs a, max tseitinBase (abs a)) [[a]]
instance BoolComponent BoolForm where
toBF = id
numberOfVariables :: BoolForm -> Int
numberOfVariables (Cnf (a, b) _) = a + b - tseitinBase
numberOfClauses :: BoolForm -> Int
numberOfClauses (Cnf _ l) = length l
boolFormTrue :: BoolForm
boolFormTrue = Cnf (-1, 1) []
boolFormFalse :: BoolForm
boolFormFalse = Cnf (-1, -1) []
instance BoolComponent Bool where
toBF True = boolFormTrue
toBF False = boolFormFalse
isTrue :: BoolForm -> Bool
isTrue = (== boolFormTrue)
isFalse :: BoolForm -> Bool
isFalse = (== boolFormFalse)
clausesOf :: BoolForm -> [[Int]]
clausesOf cnf@(Cnf _ [[]]) = []
clausesOf cnf@(Cnf _ [[x]]) = []
clausesOf cnf@(Cnf _ l) = l
maxRank :: BoolForm -> Int
maxRank (Cnf (n, _) _) = n
tseitinNumber :: BoolForm -> Int
tseitinNumber (Cnf (m, n) [[x]]) = x
tseitinNumber (Cnf (_, n) _) = n
renumber :: Int -> BoolForm -> (BoolForm, Int)
renumber base (Cnf (m, n) l)
| l == [] = (Cnf (m, n) l, 0)
| tseitinBase < base = (Cnf (m, n') l', n')
| otherwise = (Cnf (n', tseitinBase) l', n')
where
l' = map (map f) l
n' = maximum $ map maximum l'
offset = base - tseitinBase - 1
f x = if abs x < tseitinBase then x else signum x * (abs x + offset)
instance Ord BoolForm where
compare (Cnf _ a) (Cnf _ b) = compare a b
(-|-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm
(toBF -> e1) -|- (toBF -> e2')
| isTrue e1 || isTrue e2' = boolFormTrue
| isFalse e1 && isFalse e2' = boolFormFalse
| isFalse e1 = e2'
| isFalse e2' = e1
| otherwise = Cnf (m, c) $ clausesOf e1 ++ clausesOf e2 ++ [[a, b, - c], [- a, c], [- b, c]]
where
a = tseitinNumber e1
(e2, b) = renumber (1 + max tseitinBase a) e2'
m = max (maxRank e1) (maxRank e2)
c = 1 + max tseitinBase (max a b)
(-&-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm
(toBF -> e1) -&- (toBF -> e2')
| isTrue e1 && isTrue e2' = boolFormTrue
| isFalse e1 || isFalse e2' = boolFormFalse
| isTrue e1 = e2'
| isTrue e2' = e1
| otherwise = Cnf (m, c) $ clausesOf e1 ++ clausesOf e2 ++ [[- a, - b, c], [a, - c], [b, - c]]
where
a = tseitinNumber e1
(e2, b) = renumber (1 + max tseitinBase a) e2'
m = max (maxRank e1) (maxRank e2)
c = 1 + max tseitinBase (max a b)
neg :: (BoolComponent a) => a -> BoolForm
neg (toBF -> e) =
Cnf (m, c) $ clausesOf e ++ [[- a, - c], [a, c]]
where
a = tseitinNumber e
m = maxRank e
c = 1 + max tseitinBase a
(-=-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm
(toBF -> e1) -=- (toBF -> e2) = (e1 -&- e2) -|- (neg e1 -&- neg e2)
(-!-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm
(toBF -> e1) -!- (toBF -> e2) = (neg e1 -&- e2) -|- (e1 -&- neg e2)
(->-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm
(toBF -> a) ->- (toBF -> b) = (neg a) -|- b
disjunctionOf :: [BoolForm] -> BoolForm
disjunctionOf [] = boolFormFalse
disjunctionOf (x:l) = foldl' (-|-) x l
(-|||-) :: [BoolForm] -> BoolForm
(-|||-) = disjunctionOf
conjunctionOf :: [BoolForm] -> BoolForm
conjunctionOf [] = boolFormTrue
conjunctionOf (x:l) = foldl' (-&-) x l
(-&&&-) :: [BoolForm] -> BoolForm
(-&&&-) = conjunctionOf
asList_ :: BoolForm -> [[Int]]
asList_ cnf@(Cnf (m,_) _)
| isTrue cnf = []
| isFalse cnf = [[]]
| otherwise = l'
where
(Cnf _ l', _) = renumber (m + 1) cnf
asList :: BoolForm -> [[Int]]
asList cnf@(Cnf (m,n) l)
| isTrue cnf = []
| isFalse cnf = [[]]
| n <= tseitinBase = l
| otherwise = [m'] : l'
where
(Cnf (m', _) l', _) = renumber (m + 1) cnf
asLatex_ :: BoolForm -> String
asLatex_ b = beg ++ s ++ end
where
beg = "\\begin{displaymath}\n"
end = "\n\\end{displaymath}\n"
s = intercalate " \\wedge " [ makeClause c | c <- asList_ b]
makeClause c = "(" ++ intercalate "\\vee" [makeLiteral l | l <- c] ++ ")"
makeLiteral l
| 0 < l = " x_{" ++ show l ++ "} "
| otherwise = " \\neg " ++ "x_{" ++ show (negate l) ++ "} "
asLatex :: BoolForm -> String
asLatex b = beg ++ s ++ end
where
beg = "\\begin{displaymath}\n"
end = "\n\\end{displaymath}\n"
s = intercalate " \\wedge " [ makeClause c | c <- asList b]
makeClause c = "(" ++ intercalate "\\vee" [makeLiteral l | l <- c] ++ ")"
makeLiteral l
| 0 < l = " x_{" ++ show l ++ "} "
| otherwise = " \\neg " ++ "x_{" ++ show (negate l) ++ "} "