-- | Parser for DIMACS CNF format
--
-- explained in e.g. https://jix.github.io/varisat/manual/0.2.0/formats/dimacs.html and
-- https://users.aalto.fi/~tjunttil/2021-DP-AUT/notes-sat/solving.html#the-dimacs-cnf-file-format
--
{-# 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

    -- create literal
    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

    -- addClauses
    [[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'

    -- solve
    Bool
res <- Solver s -> ST s Bool
forall s. Solver s -> ST s Bool
PureSAT.solve Solver s
s

    -- read back the solution
    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

-- | Parse DIMACS file
--
-- with parsec >= 3.1.17 the 'P.ParseError' is thrown on parse failure , otherwise @UserError@.
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 -- we omit header
        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'