{-# LANGUAGE CPP #-}
module PureSAT.DIMACS (
parseDimacsFile,
parseDimacs,
demo,
) where
import Control.Applicative ((<|>))
import Data.Foldable (foldl')
import Data.Maybe (catMaybes)
#if MIN_VERSION_parsec(3,1,17)
import Control.Exception (throwIO)
#endif
import qualified Text.Parsec as P
import qualified Text.Parsec.ByteString as P
import qualified Data.ByteString as BS
import Control.Monad (forM_, forM)
import Control.Monad.ST (runST)
import qualified PureSAT.Main as PureSAT
import PureSAT.Prim
demo :: [[Int]] -> [Int]
demo :: [[Int]] -> [Int]
demo [[Int]]
clauses = (forall s. ST s [Int]) -> [Int]
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s [Int]) -> [Int])
-> (forall s. ST s [Int]) -> [Int]
forall a b. (a -> b) -> a -> b
$ do
Solver s
s <- ST s (Solver s)
forall s. ST s (Solver s)
PureSAT.newSolver
MutablePrimArray s Lit
literals <- Int -> ST s (MutablePrimArray (PrimState (ST s)) Lit)
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
Int -> m (MutablePrimArray (PrimState m) a)
newPrimArray Int
maxLiteral
[Int] -> (Int -> ST s ()) -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int
1..Int
maxLiteral] ((Int -> ST s ()) -> ST s ()) -> (Int -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \Int
i -> do
Lit
l <- Solver s -> ST s Lit
forall s. Solver s -> ST s Lit
PureSAT.newLit Solver s
s
MutablePrimArray s Lit -> Int -> Lit -> ST s ()
forall a s.
(HasCallStack, Prim a) =>
MutablePrimArray s a -> Int -> a -> ST s ()
writePrimArray MutablePrimArray s Lit
literals (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Lit
l
[[Int]] -> ([Int] -> ST s Bool) -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [[Int]]
clauses (([Int] -> ST s Bool) -> ST s ())
-> ([Int] -> ST s Bool) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \[Int]
clause -> do
[Lit]
clause' <- [Int] -> (Int -> ST s Lit) -> ST s [Lit]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int]
clause ((Int -> ST s Lit) -> ST s [Lit])
-> (Int -> ST s Lit) -> ST s [Lit]
forall a b. (a -> b) -> a -> b
$ \Int
i -> do
Lit
l <- MutablePrimArray s Lit -> Int -> ST s Lit
forall a s.
(HasCallStack, Prim a) =>
MutablePrimArray s a -> Int -> ST s a
readPrimArray MutablePrimArray s Lit
literals (Int -> Int
forall a. Num a => a -> a
abs Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
Lit -> ST s Lit
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Lit -> ST s Lit) -> Lit -> ST s Lit
forall a b. (a -> b) -> a -> b
$ if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 then Lit -> Lit
PureSAT.neg Lit
l else Lit
l
Solver s -> [Lit] -> ST s Bool
forall s. Solver s -> [Lit] -> ST s Bool
PureSAT.addClause Solver s
s [Lit]
clause'
Bool
res <- Solver s -> ST s Bool
forall s. Solver s -> ST s Bool
PureSAT.solve Solver s
s
if Bool
res
then do
[Int] -> (Int -> ST s Int) -> ST s [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int
1..Int
maxLiteral] ((Int -> ST s Int) -> ST s [Int])
-> (Int -> ST s Int) -> ST s [Int]
forall a b. (a -> b) -> a -> b
$ \Int
i -> do
Lit
l <- MutablePrimArray s Lit -> Int -> ST s Lit
forall a s.
(HasCallStack, Prim a) =>
MutablePrimArray s a -> Int -> ST s a
readPrimArray MutablePrimArray s Lit
literals (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
Bool
x <- Solver s -> Lit -> ST s Bool
forall s. Solver s -> Lit -> ST s Bool
PureSAT.modelValue Solver s
s Lit
l
Int -> ST s Int
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> ST s Int) -> Int -> ST s Int
forall a b. (a -> b) -> a -> b
$ if Bool
x then Int
i else Int -> Int
forall a. Num a => a -> a
negate Int
i
else [Int] -> ST s [Int]
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return []
where
maxLiteral :: Int
maxLiteral = (Int -> [Int] -> Int) -> Int -> [[Int]] -> Int
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Int
acc [Int]
clause -> (Int -> Int -> Int) -> Int -> [Int] -> Int
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Int
x Int
y -> Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
x (Int -> Int
forall a. Num a => a -> a
abs Int
y)) Int
acc [Int]
clause) Int
0 [[Int]]
clauses
parseDimacsFile :: FilePath -> IO [[Int]]
parseDimacsFile :: FilePath -> IO [[Int]]
parseDimacsFile FilePath
fn = do
ByteString
contents <- FilePath -> IO ByteString
BS.readFile FilePath
fn
#if MIN_VERSION_parsec(3,1,17)
(ParseError -> IO [[Int]])
-> ([[Int]] -> IO [[Int]])
-> Either ParseError [[Int]]
-> IO [[Int]]
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ParseError -> IO [[Int]]
forall e a. Exception e => e -> IO a
throwIO [[Int]] -> IO [[Int]]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either ParseError [[Int]] -> IO [[Int]])
-> Either ParseError [[Int]] -> IO [[Int]]
forall a b. (a -> b) -> a -> b
$
#else
either (fail . show) return $
#endif
FilePath -> ByteString -> Either ParseError [[Int]]
parseDimacs FilePath
fn ByteString
contents
parseDimacs :: FilePath -> BS.ByteString -> Either P.ParseError [[Int]]
parseDimacs :: FilePath -> ByteString -> Either ParseError [[Int]]
parseDimacs FilePath
fn ByteString
contents = Parsec ByteString () [[Int]]
-> FilePath -> ByteString -> Either ParseError [[Int]]
forall s t a.
Stream s Identity t =>
Parsec s () a -> FilePath -> s -> Either ParseError a
P.parse (Parser ()
skipSpace Parser ()
-> Parsec ByteString () [[Int]] -> Parsec ByteString () [[Int]]
forall a b.
ParsecT ByteString () Identity a
-> ParsecT ByteString () Identity b
-> ParsecT ByteString () Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parsec ByteString () [[Int]]
dimacs Parsec ByteString () [[Int]]
-> Parser () -> Parsec ByteString () [[Int]]
forall a b.
ParsecT ByteString () Identity a
-> ParsecT ByteString () Identity b
-> ParsecT ByteString () Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
P.eof) FilePath
fn ByteString
contents
dimacs :: P.Parser [[Int]]
dimacs :: Parsec ByteString () [[Int]]
dimacs = do
[Maybe [Int]]
es <- ParsecT ByteString () Identity (Maybe [Int])
-> ParsecT ByteString () Identity [Maybe [Int]]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
P.many ParsecT ByteString () Identity (Maybe [Int])
entry
[[Int]] -> Parsec ByteString () [[Int]]
forall a. a -> ParsecT ByteString () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Maybe [Int]] -> [[Int]]
forall a. [Maybe a] -> [a]
catMaybes [Maybe [Int]]
es)
entry :: P.Parser (Maybe [Int])
entry :: ParsecT ByteString () Identity (Maybe [Int])
entry = do
Char
c <- ParsecT ByteString () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
P.anyChar
case Char
c of
Char
'p' -> Maybe [Int]
forall a. Maybe a
Nothing Maybe [Int]
-> Parser () -> ParsecT ByteString () Identity (Maybe [Int])
forall a b.
a
-> ParsecT ByteString () Identity b
-> ParsecT ByteString () Identity a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Parser ()
skipLine
Char
'c' -> Maybe [Int]
forall a. Maybe a
Nothing Maybe [Int]
-> Parser () -> ParsecT ByteString () Identity (Maybe [Int])
forall a b.
a
-> ParsecT ByteString () Identity b
-> ParsecT ByteString () Identity a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Parser ()
skipLine
Char
'-' -> [Int] -> Maybe [Int]
forall a. a -> Maybe a
Just ([Int] -> Maybe [Int])
-> ParsecT ByteString () Identity [Int]
-> ParsecT ByteString () Identity (Maybe [Int])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT ByteString () Identity [Int]
negativeClause
Char
_ | Char
'0' Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
c Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
'9'
-> [Int] -> Maybe [Int]
forall a. a -> Maybe a
Just ([Int] -> Maybe [Int])
-> ParsecT ByteString () Identity [Int]
-> ParsecT ByteString () Identity (Maybe [Int])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Char -> ParsecT ByteString () Identity [Int]
positiveClause Char
c
Char
_ -> FilePath -> ParsecT ByteString () Identity (Maybe [Int])
forall a. FilePath -> ParsecT ByteString () Identity a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> ParsecT ByteString () Identity (Maybe [Int]))
-> FilePath -> ParsecT ByteString () Identity (Maybe [Int])
forall a b. (a -> b) -> a -> b
$ FilePath
"unexpecter character: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Char -> FilePath
forall a. Show a => a -> FilePath
show Char
c
skipLine :: P.Parser ()
skipLine :: Parser ()
skipLine = Parser ()
aux Parser () -> Parser () -> Parser ()
forall a.
ParsecT ByteString () Identity a
-> ParsecT ByteString () Identity a
-> ParsecT ByteString () Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
P.eof
where
aux :: Parser ()
aux = do
Char
c <- ParsecT ByteString () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
P.anyChar
if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\n'
then Parser ()
skipSpace
else Parser ()
skipLine
skipSpace :: P.Parser ()
skipSpace :: Parser ()
skipSpace = ParsecT ByteString () Identity Char -> Parser ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
P.skipMany (ParsecT ByteString () Identity Char -> Parser ())
-> ParsecT ByteString () Identity Char -> Parser ()
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> ParsecT ByteString () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
P.satisfy (\Char
c -> Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
' ' Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\n' Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\r' Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\t')
negativeClause :: P.Parser [Int]
negativeClause :: ParsecT ByteString () Identity [Int]
negativeClause = do
Int
l <- Parser Int
variable
if Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
then [Int] -> ParsecT ByteString () Identity [Int]
forall a. a -> ParsecT ByteString () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return []
else ([Int] -> [Int]) -> ParsecT ByteString () Identity [Int]
go (Int -> Int
forall a. Num a => a -> a
negate Int
l Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:)
where
go :: ([Int] -> [Int]) -> P.Parser [Int]
go :: ([Int] -> [Int]) -> ParsecT ByteString () Identity [Int]
go ![Int] -> [Int]
acc = do
Int
l <- Parser Int
literal
if Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
then [Int] -> ParsecT ByteString () Identity [Int]
forall a. a -> ParsecT ByteString () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Int] -> [Int]
acc [])
else ([Int] -> [Int]) -> ParsecT ByteString () Identity [Int]
go ([Int] -> [Int]
acc ([Int] -> [Int]) -> ([Int] -> [Int]) -> [Int] -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int
l Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:))
positiveClause :: Char -> P.Parser [Int]
positiveClause :: Char -> ParsecT ByteString () Identity [Int]
positiveClause Char
d = do
Int
l <- Char -> Parser Int
variable' Char
d
if Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
then [Int] -> ParsecT ByteString () Identity [Int]
forall a. a -> ParsecT ByteString () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return []
else ([Int] -> [Int]) -> ParsecT ByteString () Identity [Int]
go (Int
l Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:)
where
go :: ([Int] -> [Int]) -> P.Parser [Int]
go :: ([Int] -> [Int]) -> ParsecT ByteString () Identity [Int]
go ![Int] -> [Int]
acc = do
Int
l <- Parser Int
literal
if Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
then [Int] -> ParsecT ByteString () Identity [Int]
forall a. a -> ParsecT ByteString () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Int] -> [Int]
acc [])
else ([Int] -> [Int]) -> ParsecT ByteString () Identity [Int]
go ([Int] -> [Int]
acc ([Int] -> [Int]) -> ([Int] -> [Int]) -> [Int] -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int
l Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:))
literal :: P.Parser Int
literal :: Parser Int
literal = do
Char
c <- ParsecT ByteString () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
P.anyChar
case Char
c of
Char
'-' -> Int -> Int
forall a. Num a => a -> a
negate (Int -> Int) -> Parser Int -> Parser Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Int
literal
Char
_ | Char
'0' Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
c Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
'9'
-> Char -> Parser Int
variable' Char
c
Char
_ -> FilePath -> Parser Int
forall a. FilePath -> ParsecT ByteString () Identity a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> Parser Int) -> FilePath -> Parser Int
forall a b. (a -> b) -> a -> b
$ FilePath
"unexpecter character: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Char -> FilePath
forall a. Show a => a -> FilePath
show Char
c
variable :: P.Parser Int
variable :: Parser Int
variable = do
Char
d <- (Char -> Bool) -> ParsecT ByteString () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
P.satisfy (\Char
x -> Char
'0' Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
x Bool -> Bool -> Bool
&& Char
x Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
'9')
Char -> Parser Int
variable' Char
d
variable' :: Char -> P.Parser Int
variable' :: Char -> Parser Int
variable' Char
d = do
FilePath
ds <- ParsecT ByteString () Identity Char
-> ParsecT ByteString () Identity FilePath
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
P.many (ParsecT ByteString () Identity Char
-> ParsecT ByteString () Identity FilePath)
-> ParsecT ByteString () Identity Char
-> ParsecT ByteString () Identity FilePath
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> ParsecT ByteString () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
P.satisfy (\Char
x -> Char
'0' Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
x Bool -> Bool -> Bool
&& Char
x Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
'9')
Parser ()
skipSpace
Int -> Parser Int
forall a. a -> ParsecT ByteString () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Parser Int) -> Int -> Parser Int
forall a b. (a -> b) -> a -> b
$ (Int -> Char -> Int) -> Int -> FilePath -> Int
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Int
acc Char
x -> Int
acc Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
10 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Char -> Int
toInt Char
x) Int
0 (Char
dChar -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
ds)
where
toInt :: Char -> Int
toInt :: Char -> Int
toInt Char
x = Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
'0'