{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE OverloadedStrings #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.FileFormat.CNF
-- Copyright   :  (c) Masahiro Sakai 2016-2018
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Reader and Writer for DIMACS CNF and family of similar formats.
--
-----------------------------------------------------------------------------
module ToySolver.FileFormat.CNF
  (
  -- * FileFormat class
    module ToySolver.FileFormat.Base

  -- * CNF format
  , CNF (..)

  -- * WCNF formats

  -- ** (Old) WCNF format
  , WCNF (..)
  , WeightedClause
  , Weight

  -- ** New WCNF format
  , NewWCNF (..)

  -- ** Old or new WCNF
  , SomeWCNF (..)

  -- * GCNF format
  , GCNF (..)
  , GroupIndex
  , GClause

  -- * QDIMACS format
  , QDimacs (..)
  , Quantifier (..)
  , QuantSet
  , Atom

  -- * Re-exports
  , Lit
  , Clause
  , PackedClause
  , packClause
  , unpackClause
  ) where

import Prelude hiding (readFile, writeFile)
import Control.DeepSeq
import Control.Monad
import qualified Data.ByteString.Lazy.Char8 as BS
import Data.ByteString.Builder
import Data.Char
import Data.Maybe

import ToySolver.FileFormat.Base
import qualified ToySolver.SAT.Types as SAT
import ToySolver.SAT.Types (Lit, Clause, PackedClause, packClause, unpackClause)

-- -------------------------------------------------------------------

-- | DIMACS CNF format
data CNF
  = CNF
  { CNF -> Int
cnfNumVars :: !Int
    -- ^ Number of variables
  , CNF -> Int
cnfNumClauses :: !Int
    -- ^ Number of clauses
  , CNF -> [PackedClause]
cnfClauses :: [SAT.PackedClause]
    -- ^ Clauses
  }
  deriving (CNF -> CNF -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CNF -> CNF -> Bool
$c/= :: CNF -> CNF -> Bool
== :: CNF -> CNF -> Bool
$c== :: CNF -> CNF -> Bool
Eq, Eq CNF
CNF -> CNF -> Bool
CNF -> CNF -> Ordering
CNF -> CNF -> CNF
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CNF -> CNF -> CNF
$cmin :: CNF -> CNF -> CNF
max :: CNF -> CNF -> CNF
$cmax :: CNF -> CNF -> CNF
>= :: CNF -> CNF -> Bool
$c>= :: CNF -> CNF -> Bool
> :: CNF -> CNF -> Bool
$c> :: CNF -> CNF -> Bool
<= :: CNF -> CNF -> Bool
$c<= :: CNF -> CNF -> Bool
< :: CNF -> CNF -> Bool
$c< :: CNF -> CNF -> Bool
compare :: CNF -> CNF -> Ordering
$ccompare :: CNF -> CNF -> Ordering
Ord, Int -> CNF -> ShowS
[CNF] -> ShowS
CNF -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CNF] -> ShowS
$cshowList :: [CNF] -> ShowS
show :: CNF -> String
$cshow :: CNF -> String
showsPrec :: Int -> CNF -> ShowS
$cshowsPrec :: Int -> CNF -> ShowS
Show, ReadPrec [CNF]
ReadPrec CNF
Int -> ReadS CNF
ReadS [CNF]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [CNF]
$creadListPrec :: ReadPrec [CNF]
readPrec :: ReadPrec CNF
$creadPrec :: ReadPrec CNF
readList :: ReadS [CNF]
$creadList :: ReadS [CNF]
readsPrec :: Int -> ReadS CNF
$creadsPrec :: Int -> ReadS CNF
Read)

instance FileFormat CNF where
  parse :: ByteString -> Either String CNF
parse ByteString
s =
    case ByteString -> [ByteString]
BS.words ByteString
l of
      ([ByteString
"p",ByteString
"cnf", ByteString
nvar, ByteString
nclause]) ->
        forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$
          CNF
          { cnfNumVars :: Int
cnfNumVars    = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nvar
          , cnfNumClauses :: Int
cnfNumClauses = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nclause
          , cnfClauses :: [PackedClause]
cnfClauses    = forall a b. (a -> b) -> [a] -> [b]
map ByteString -> PackedClause
parseClauseBS [ByteString]
ls
          }
      [ByteString]
_ ->
        forall a b. a -> Either a b
Left String
"cannot find cnf header"
    where
      l :: BS.ByteString
      ls :: [BS.ByteString]
      (ByteString
l:[ByteString]
ls) = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Bool
isCommentBS) (ByteString -> [ByteString]
BS.lines ByteString
s)

  render :: CNF -> Builder
render CNF
cnf = Builder
header forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map PackedClause -> Builder
f (CNF -> [PackedClause]
cnfClauses CNF
cnf))
    where
      header :: Builder
header = forall a. Monoid a => [a] -> a
mconcat
        [ ByteString -> Builder
byteString ByteString
"p cnf "
        , Int -> Builder
intDec (CNF -> Int
cnfNumVars CNF
cnf), Char -> Builder
char7 Char
' '
        , Int -> Builder
intDec (CNF -> Int
cnfNumClauses CNF
cnf), Char -> Builder
char7 Char
'\n'
        ]
      f :: PackedClause -> Builder
f PackedClause
c = forall a. Monoid a => [a] -> a
mconcat [Int -> Builder
intDec Int
lit forall a. Semigroup a => a -> a -> a
<> Char -> Builder
char7 Char
' '| Int
lit <- PackedClause -> Clause
SAT.unpackClause PackedClause
c] forall a. Semigroup a => a -> a -> a
<> ByteString -> Builder
byteString ByteString
"0\n"

readInts :: BS.ByteString -> [Int]
readInts :: ByteString -> Clause
readInts ByteString
s =
  case ByteString -> Maybe (Int, ByteString)
BS.readInt ((Char -> Bool) -> ByteString -> ByteString
BS.dropWhile Char -> Bool
isSpace ByteString
s) of
    Just (Int
0,ByteString
_) -> []
    Just (Int
z,ByteString
s') -> Int
z forall a. a -> [a] -> [a]
: ByteString -> Clause
readInts ByteString
s'
    Maybe (Int, ByteString)
Nothing -> forall a. HasCallStack => String -> a
error String
"ToySolver.FileFormat.CNF.readInts: 0 is missing"

parseClauseBS :: BS.ByteString -> SAT.PackedClause
parseClauseBS :: ByteString -> PackedClause
parseClauseBS = Clause -> PackedClause
SAT.packClause forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Clause
readInts

isCommentBS :: BS.ByteString -> Bool
isCommentBS :: ByteString -> Bool
isCommentBS ByteString
s =
  case ByteString -> Maybe (Char, ByteString)
BS.uncons ByteString
s of
    Just (Char
'c',ByteString
_) ->  Bool
True
    Maybe (Char, ByteString)
_ -> Bool
False

-- -------------------------------------------------------------------

-- | WCNF format for representing partial weighted Max-SAT problems.
--
-- This format is used for for MAX-SAT evaluations.
--
-- References:
--
-- * <http://maxsat.ia.udl.cat/requirements/>
data WCNF
  = WCNF
  { WCNF -> Int
wcnfNumVars    :: !Int
    -- ^ Number of variables
  , WCNF -> Int
wcnfNumClauses :: !Int
    -- ^ Number of (weighted) clauses
  , WCNF -> Weight
wcnfTopCost    :: !Weight
    -- ^ Hard clauses have weight equal or greater than "top".
    -- We assure that "top" is a weight always greater than the sum of the weights of violated soft clauses in the solution.
  , WCNF -> [WeightedClause]
wcnfClauses    :: [WeightedClause]
    -- ^ Weighted clauses
  }
  deriving (WCNF -> WCNF -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WCNF -> WCNF -> Bool
$c/= :: WCNF -> WCNF -> Bool
== :: WCNF -> WCNF -> Bool
$c== :: WCNF -> WCNF -> Bool
Eq, Eq WCNF
WCNF -> WCNF -> Bool
WCNF -> WCNF -> Ordering
WCNF -> WCNF -> WCNF
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: WCNF -> WCNF -> WCNF
$cmin :: WCNF -> WCNF -> WCNF
max :: WCNF -> WCNF -> WCNF
$cmax :: WCNF -> WCNF -> WCNF
>= :: WCNF -> WCNF -> Bool
$c>= :: WCNF -> WCNF -> Bool
> :: WCNF -> WCNF -> Bool
$c> :: WCNF -> WCNF -> Bool
<= :: WCNF -> WCNF -> Bool
$c<= :: WCNF -> WCNF -> Bool
< :: WCNF -> WCNF -> Bool
$c< :: WCNF -> WCNF -> Bool
compare :: WCNF -> WCNF -> Ordering
$ccompare :: WCNF -> WCNF -> Ordering
Ord, Int -> WCNF -> ShowS
[WCNF] -> ShowS
WCNF -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [WCNF] -> ShowS
$cshowList :: [WCNF] -> ShowS
show :: WCNF -> String
$cshow :: WCNF -> String
showsPrec :: Int -> WCNF -> ShowS
$cshowsPrec :: Int -> WCNF -> ShowS
Show, ReadPrec [WCNF]
ReadPrec WCNF
Int -> ReadS WCNF
ReadS [WCNF]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [WCNF]
$creadListPrec :: ReadPrec [WCNF]
readPrec :: ReadPrec WCNF
$creadPrec :: ReadPrec WCNF
readList :: ReadS [WCNF]
$creadList :: ReadS [WCNF]
readsPrec :: Int -> ReadS WCNF
$creadsPrec :: Int -> ReadS WCNF
Read)

-- | Weighted clauses
type WeightedClause = (Weight, SAT.PackedClause)

-- | Weigths must be greater than or equal to 1, and smaller than 2^63.
type Weight = Integer

-- | Note that 'parse' also accepts new WCNF files and (unweighted) CNF files and converts them into 'WCNF'.
instance FileFormat WCNF where
  parse :: ByteString -> Either String WCNF
parse = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM SomeWCNF -> WCNF
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FileFormat a => ByteString -> Either String a
parse
    where
      f :: SomeWCNF -> WCNF
f (SomeWCNFNew NewWCNF
x) = NewWCNF -> WCNF
toOldWCNF NewWCNF
x
      f (SomeWCNFOld WCNF
x) = WCNF
x

  render :: WCNF -> Builder
render WCNF
wcnf = Builder
header forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map WeightedClause -> Builder
f (WCNF -> [WeightedClause]
wcnfClauses WCNF
wcnf))
    where
      header :: Builder
header = forall a. Monoid a => [a] -> a
mconcat
        [ ByteString -> Builder
byteString ByteString
"p wcnf "
        , Int -> Builder
intDec (WCNF -> Int
wcnfNumVars WCNF
wcnf), Char -> Builder
char7 Char
' '
        , Int -> Builder
intDec (WCNF -> Int
wcnfNumClauses WCNF
wcnf), Char -> Builder
char7 Char
' '
        , Weight -> Builder
integerDec (WCNF -> Weight
wcnfTopCost WCNF
wcnf), Char -> Builder
char7 Char
'\n'
        ]
      f :: WeightedClause -> Builder
f (Weight
w,PackedClause
c) = Weight -> Builder
integerDec Weight
w forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat [Char -> Builder
char7 Char
' ' forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
lit | Int
lit <- PackedClause -> Clause
SAT.unpackClause PackedClause
c] forall a. Semigroup a => a -> a -> a
<> ByteString -> Builder
byteString ByteString
" 0\n"

parseWCNFLineBS :: BS.ByteString -> WeightedClause
parseWCNFLineBS :: ByteString -> WeightedClause
parseWCNFLineBS ByteString
s =
  case ByteString -> Maybe (Weight, ByteString)
BS.readInteger ((Char -> Bool) -> ByteString -> ByteString
BS.dropWhile Char -> Bool
isSpace ByteString
s) of
    Maybe (Weight, ByteString)
Nothing -> forall a. HasCallStack => String -> a
error String
"ToySolver.FileFormat.CNF: no weight"
    Just (Weight
w, ByteString
s') -> seq :: forall a b. a -> b -> b
seq Weight
w forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq PackedClause
xs forall a b. (a -> b) -> a -> b
$ (Weight
w, PackedClause
xs)
      where
        xs :: PackedClause
xs = ByteString -> PackedClause
parseClauseBS ByteString
s'

-- -------------------------------------------------------------------

-- | New WCNF file format
--
-- This format is used for for MAX-SAT evaluations >=2020.
--
-- References:
--
-- * <https://maxsat-evaluations.github.io/2021/format.html>
newtype NewWCNF
  = NewWCNF
  { NewWCNF -> [NewWeightedClause]
nwcnfClauses :: [NewWeightedClause]
    -- ^ Weighted clauses
  }
  deriving (NewWCNF -> NewWCNF -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NewWCNF -> NewWCNF -> Bool
$c/= :: NewWCNF -> NewWCNF -> Bool
== :: NewWCNF -> NewWCNF -> Bool
$c== :: NewWCNF -> NewWCNF -> Bool
Eq, Eq NewWCNF
NewWCNF -> NewWCNF -> Bool
NewWCNF -> NewWCNF -> Ordering
NewWCNF -> NewWCNF -> NewWCNF
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: NewWCNF -> NewWCNF -> NewWCNF
$cmin :: NewWCNF -> NewWCNF -> NewWCNF
max :: NewWCNF -> NewWCNF -> NewWCNF
$cmax :: NewWCNF -> NewWCNF -> NewWCNF
>= :: NewWCNF -> NewWCNF -> Bool
$c>= :: NewWCNF -> NewWCNF -> Bool
> :: NewWCNF -> NewWCNF -> Bool
$c> :: NewWCNF -> NewWCNF -> Bool
<= :: NewWCNF -> NewWCNF -> Bool
$c<= :: NewWCNF -> NewWCNF -> Bool
< :: NewWCNF -> NewWCNF -> Bool
$c< :: NewWCNF -> NewWCNF -> Bool
compare :: NewWCNF -> NewWCNF -> Ordering
$ccompare :: NewWCNF -> NewWCNF -> Ordering
Ord, Int -> NewWCNF -> ShowS
[NewWCNF] -> ShowS
NewWCNF -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NewWCNF] -> ShowS
$cshowList :: [NewWCNF] -> ShowS
show :: NewWCNF -> String
$cshow :: NewWCNF -> String
showsPrec :: Int -> NewWCNF -> ShowS
$cshowsPrec :: Int -> NewWCNF -> ShowS
Show, ReadPrec [NewWCNF]
ReadPrec NewWCNF
Int -> ReadS NewWCNF
ReadS [NewWCNF]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [NewWCNF]
$creadListPrec :: ReadPrec [NewWCNF]
readPrec :: ReadPrec NewWCNF
$creadPrec :: ReadPrec NewWCNF
readList :: ReadS [NewWCNF]
$creadList :: ReadS [NewWCNF]
readsPrec :: Int -> ReadS NewWCNF
$creadsPrec :: Int -> ReadS NewWCNF
Read)

type NewWeightedClause = (Maybe Weight, SAT.PackedClause)

-- | Note that 'parse' also accepts (old) WCNF files and (unweighted) CNF files and converts them into 'NewWCNF'.
instance FileFormat NewWCNF where
  parse :: ByteString -> Either String NewWCNF
parse = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM SomeWCNF -> NewWCNF
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FileFormat a => ByteString -> Either String a
parse
    where
      f :: SomeWCNF -> NewWCNF
f (SomeWCNFNew NewWCNF
x) = NewWCNF
x
      f (SomeWCNFOld WCNF
x) = WCNF -> NewWCNF
toNewWCNF WCNF
x

  render :: NewWCNF -> Builder
render NewWCNF
nwcnf = forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map NewWeightedClause -> Builder
f (NewWCNF -> [NewWeightedClause]
nwcnfClauses NewWCNF
nwcnf))
    where
      f :: NewWeightedClause -> Builder
f (Maybe Weight
Nothing, PackedClause
c) = Char -> Builder
char7 Char
'h' forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat [Char -> Builder
char7 Char
' ' forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
lit | Int
lit <- PackedClause -> Clause
SAT.unpackClause PackedClause
c] forall a. Semigroup a => a -> a -> a
<> ByteString -> Builder
byteString ByteString
" 0\n"
      f (Just Weight
w, PackedClause
c) = Weight -> Builder
integerDec Weight
w forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat [Char -> Builder
char7 Char
' ' forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
lit | Int
lit <- PackedClause -> Clause
SAT.unpackClause PackedClause
c] forall a. Semigroup a => a -> a -> a
<> ByteString -> Builder
byteString ByteString
" 0\n"

parseNewWCNFLineBS :: BS.ByteString -> NewWeightedClause
parseNewWCNFLineBS :: ByteString -> NewWeightedClause
parseNewWCNFLineBS ByteString
s =
  case ByteString -> Maybe (Char, ByteString)
BS.uncons ByteString
s' of
    Maybe (Char, ByteString)
Nothing -> forall a. HasCallStack => String -> a
error String
"ToySolver.FileFormat.CNF: no weight"
    Just (Char
'h', ByteString
s'') ->
      let xs :: PackedClause
xs = ByteString -> PackedClause
parseClauseBS ByteString
s''
       in seq :: forall a b. a -> b -> b
seq PackedClause
xs forall a b. (a -> b) -> a -> b
$ (forall a. Maybe a
Nothing, PackedClause
xs)
    Just (Char, ByteString)
_ ->
      case ByteString -> Maybe (Weight, ByteString)
BS.readInteger ByteString
s' of
        Maybe (Weight, ByteString)
Nothing -> forall a. HasCallStack => String -> a
error String
"ToySolver.FileFormat.CNF: no weight"
        Just (Weight
w, ByteString
s'') ->
          let xs :: PackedClause
xs = ByteString -> PackedClause
parseClauseBS ByteString
s''
           in seq :: forall a b. a -> b -> b
seq Weight
w forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq PackedClause
xs forall a b. (a -> b) -> a -> b
$ (forall a. a -> Maybe a
Just Weight
w, PackedClause
xs)
  where
    s' :: ByteString
s' = (Char -> Bool) -> ByteString -> ByteString
BS.dropWhile Char -> Bool
isSpace ByteString
s

-- -------------------------------------------------------------------

data SomeWCNF
  = SomeWCNFOld WCNF
  | SomeWCNFNew NewWCNF
  deriving (SomeWCNF -> SomeWCNF -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SomeWCNF -> SomeWCNF -> Bool
$c/= :: SomeWCNF -> SomeWCNF -> Bool
== :: SomeWCNF -> SomeWCNF -> Bool
$c== :: SomeWCNF -> SomeWCNF -> Bool
Eq, Eq SomeWCNF
SomeWCNF -> SomeWCNF -> Bool
SomeWCNF -> SomeWCNF -> Ordering
SomeWCNF -> SomeWCNF -> SomeWCNF
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SomeWCNF -> SomeWCNF -> SomeWCNF
$cmin :: SomeWCNF -> SomeWCNF -> SomeWCNF
max :: SomeWCNF -> SomeWCNF -> SomeWCNF
$cmax :: SomeWCNF -> SomeWCNF -> SomeWCNF
>= :: SomeWCNF -> SomeWCNF -> Bool
$c>= :: SomeWCNF -> SomeWCNF -> Bool
> :: SomeWCNF -> SomeWCNF -> Bool
$c> :: SomeWCNF -> SomeWCNF -> Bool
<= :: SomeWCNF -> SomeWCNF -> Bool
$c<= :: SomeWCNF -> SomeWCNF -> Bool
< :: SomeWCNF -> SomeWCNF -> Bool
$c< :: SomeWCNF -> SomeWCNF -> Bool
compare :: SomeWCNF -> SomeWCNF -> Ordering
$ccompare :: SomeWCNF -> SomeWCNF -> Ordering
Ord, Int -> SomeWCNF -> ShowS
[SomeWCNF] -> ShowS
SomeWCNF -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SomeWCNF] -> ShowS
$cshowList :: [SomeWCNF] -> ShowS
show :: SomeWCNF -> String
$cshow :: SomeWCNF -> String
showsPrec :: Int -> SomeWCNF -> ShowS
$cshowsPrec :: Int -> SomeWCNF -> ShowS
Show, ReadPrec [SomeWCNF]
ReadPrec SomeWCNF
Int -> ReadS SomeWCNF
ReadS [SomeWCNF]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [SomeWCNF]
$creadListPrec :: ReadPrec [SomeWCNF]
readPrec :: ReadPrec SomeWCNF
$creadPrec :: ReadPrec SomeWCNF
readList :: ReadS [SomeWCNF]
$creadList :: ReadS [SomeWCNF]
readsPrec :: Int -> ReadS SomeWCNF
$creadsPrec :: Int -> ReadS SomeWCNF
Read)

toOldWCNF :: NewWCNF -> WCNF
toOldWCNF :: NewWCNF -> WCNF
toOldWCNF (NewWCNF [NewWeightedClause]
cs)
  = WCNF
  { wcnfNumVars :: Int
wcnfNumVars = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 forall a. a -> [a] -> [a]
: [forall a. Num a => a -> a
abs Int
l | (Maybe Weight
_, PackedClause
c) <- [NewWeightedClause]
cs, Int
l <- PackedClause -> Clause
unpackClause PackedClause
c])
  , wcnfNumClauses :: Int
wcnfNumClauses = forall (t :: * -> *) a. Foldable t => t a -> Int
length [NewWeightedClause]
cs
  , wcnfTopCost :: Weight
wcnfTopCost = Weight
top
  , wcnfClauses :: [WeightedClause]
wcnfClauses = [(forall a. a -> Maybe a -> a
fromMaybe Weight
top Maybe Weight
w, PackedClause
c) | (Maybe Weight
w, PackedClause
c) <- [NewWeightedClause]
cs]
  }
  where
    top :: Weight
top = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Weight
w | (Just Weight
w, PackedClause
c) <- [NewWeightedClause]
cs] forall a. Num a => a -> a -> a
+ Weight
1

toNewWCNF :: WCNF -> NewWCNF
toNewWCNF :: WCNF -> NewWCNF
toNewWCNF WCNF
wcnf = [NewWeightedClause] -> NewWCNF
NewWCNF [(if Weight
w forall a. Ord a => a -> a -> Bool
>= WCNF -> Weight
wcnfTopCost WCNF
wcnf then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just Weight
w, PackedClause
c) | (Weight
w, PackedClause
c) <- WCNF -> [WeightedClause]
wcnfClauses WCNF
wcnf]

instance FileFormat SomeWCNF where
  parse :: ByteString -> Either String SomeWCNF
parse ByteString
s =
    case forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Bool
isCommentBS) (ByteString -> [ByteString]
BS.lines ByteString
s) of
      [] -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ NewWCNF -> SomeWCNF
SomeWCNFNew forall a b. (a -> b) -> a -> b
$ [NewWeightedClause] -> NewWCNF
NewWCNF []
      lls :: [ByteString]
lls@(ByteString
l : [ByteString]
ls) ->
        case ByteString -> [ByteString]
BS.words ByteString
l of
          ([ByteString
"p",ByteString
"wcnf", ByteString
nvar, ByteString
nclause, ByteString
top]) ->
            forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ WCNF -> SomeWCNF
SomeWCNFOld forall a b. (a -> b) -> a -> b
$
              WCNF
              { wcnfNumVars :: Int
wcnfNumVars    = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nvar
              , wcnfNumClauses :: Int
wcnfNumClauses = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nclause
              , wcnfTopCost :: Weight
wcnfTopCost    = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
top
              , wcnfClauses :: [WeightedClause]
wcnfClauses    = forall a b. (a -> b) -> [a] -> [b]
map ByteString -> WeightedClause
parseWCNFLineBS [ByteString]
ls
              }
          ([ByteString
"p",ByteString
"wcnf", ByteString
nvar, ByteString
nclause]) ->
            forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ WCNF -> SomeWCNF
SomeWCNFOld forall a b. (a -> b) -> a -> b
$
              WCNF
              { wcnfNumVars :: Int
wcnfNumVars    = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nvar
              , wcnfNumClauses :: Int
wcnfNumClauses = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nclause
                -- top must be greater than the sum of the weights of violated soft clauses.
              , wcnfTopCost :: Weight
wcnfTopCost    = forall a. Num a => Weight -> a
fromInteger forall a b. (a -> b) -> a -> b
$ Weight
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
63::Int) forall a. Num a => a -> a -> a
- Weight
1
              , wcnfClauses :: [WeightedClause]
wcnfClauses    = forall a b. (a -> b) -> [a] -> [b]
map ByteString -> WeightedClause
parseWCNFLineBS [ByteString]
ls
              }
          ([ByteString
"p",ByteString
"cnf", ByteString
nvar, ByteString
nclause]) ->
            forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ WCNF -> SomeWCNF
SomeWCNFOld forall a b. (a -> b) -> a -> b
$
              WCNF
              { wcnfNumVars :: Int
wcnfNumVars    = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nvar
              , wcnfNumClauses :: Int
wcnfNumClauses = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nclause
                -- top must be greater than the sum of the weights of violated soft clauses.
              , wcnfTopCost :: Weight
wcnfTopCost    = forall a. Num a => Weight -> a
fromInteger forall a b. (a -> b) -> a -> b
$ Weight
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
63::Int) forall a. Num a => a -> a -> a
- Weight
1
              , wcnfClauses :: [WeightedClause]
wcnfClauses    = forall a b. (a -> b) -> [a] -> [b]
map ((\PackedClause
c -> seq :: forall a b. a -> b -> b
seq PackedClause
c (Weight
1,PackedClause
c)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> PackedClause
parseClauseBS) [ByteString]
ls
              }
          (ByteString
"h" : [ByteString]
_) ->
            forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ NewWCNF -> SomeWCNF
SomeWCNFNew forall a b. (a -> b) -> a -> b
$ [NewWeightedClause] -> NewWCNF
NewWCNF forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ByteString -> NewWeightedClause
parseNewWCNFLineBS [ByteString]
lls
          (ByteString
s : [ByteString]
_) | Just (Weight, ByteString)
_ <- ByteString -> Maybe (Weight, ByteString)
BS.readInteger ByteString
s ->
            forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ NewWCNF -> SomeWCNF
SomeWCNFNew forall a b. (a -> b) -> a -> b
$ [NewWeightedClause] -> NewWCNF
NewWCNF forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ByteString -> NewWeightedClause
parseNewWCNFLineBS [ByteString]
lls
          [ByteString]
_ ->
            forall a b. a -> Either a b
Left String
"cannot find wcnf/cnf header"

  render :: SomeWCNF -> Builder
render (SomeWCNFOld WCNF
wcnf) = forall a. FileFormat a => a -> Builder
render WCNF
wcnf
  render (SomeWCNFNew NewWCNF
nwcnf) = forall a. FileFormat a => a -> Builder
render NewWCNF
nwcnf

-- -------------------------------------------------------------------

-- | Group oriented CNF Input Format
--
-- This format is used in Group oriented MUS track of the SAT Competition 2011.
--
-- References:
--
-- * <http://www.satcompetition.org/2011/rules.pdf>
data GCNF
  = GCNF
  { GCNF -> Int
gcnfNumVars        :: !Int
    -- ^ Nubmer of variables
  , GCNF -> Int
gcnfNumClauses     :: !Int
    -- ^ Number of clauses
  , GCNF -> Int
gcnfLastGroupIndex :: !GroupIndex
    -- ^ The last index of a group in the file number of components contained in the file.
  , GCNF -> [GClause]
gcnfClauses        :: [GClause]
  }
  deriving (GCNF -> GCNF -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GCNF -> GCNF -> Bool
$c/= :: GCNF -> GCNF -> Bool
== :: GCNF -> GCNF -> Bool
$c== :: GCNF -> GCNF -> Bool
Eq, Eq GCNF
GCNF -> GCNF -> Bool
GCNF -> GCNF -> Ordering
GCNF -> GCNF -> GCNF
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: GCNF -> GCNF -> GCNF
$cmin :: GCNF -> GCNF -> GCNF
max :: GCNF -> GCNF -> GCNF
$cmax :: GCNF -> GCNF -> GCNF
>= :: GCNF -> GCNF -> Bool
$c>= :: GCNF -> GCNF -> Bool
> :: GCNF -> GCNF -> Bool
$c> :: GCNF -> GCNF -> Bool
<= :: GCNF -> GCNF -> Bool
$c<= :: GCNF -> GCNF -> Bool
< :: GCNF -> GCNF -> Bool
$c< :: GCNF -> GCNF -> Bool
compare :: GCNF -> GCNF -> Ordering
$ccompare :: GCNF -> GCNF -> Ordering
Ord, Int -> GCNF -> ShowS
[GCNF] -> ShowS
GCNF -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GCNF] -> ShowS
$cshowList :: [GCNF] -> ShowS
show :: GCNF -> String
$cshow :: GCNF -> String
showsPrec :: Int -> GCNF -> ShowS
$cshowsPrec :: Int -> GCNF -> ShowS
Show, ReadPrec [GCNF]
ReadPrec GCNF
Int -> ReadS GCNF
ReadS [GCNF]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [GCNF]
$creadListPrec :: ReadPrec [GCNF]
readPrec :: ReadPrec GCNF
$creadPrec :: ReadPrec GCNF
readList :: ReadS [GCNF]
$creadList :: ReadS [GCNF]
readsPrec :: Int -> ReadS GCNF
$creadsPrec :: Int -> ReadS GCNF
Read)

-- | Component number between 0 and `gcnfLastGroupIndex`
type GroupIndex = Int

-- | Clause together with component number
type GClause = (GroupIndex, SAT.PackedClause)

instance FileFormat GCNF where
  parse :: ByteString -> Either String GCNF
parse ByteString
s =
    case ByteString -> [ByteString]
BS.words ByteString
l of
      ([ByteString
"p",ByteString
"gcnf", ByteString
nbvar', ByteString
nbclauses', ByteString
lastGroupIndex']) ->
        forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$
          GCNF
          { gcnfNumVars :: Int
gcnfNumVars        = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nbvar'
          , gcnfNumClauses :: Int
gcnfNumClauses     = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nbclauses'
          , gcnfLastGroupIndex :: Int
gcnfLastGroupIndex = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
lastGroupIndex'
          , gcnfClauses :: [GClause]
gcnfClauses        = forall a b. (a -> b) -> [a] -> [b]
map ByteString -> GClause
parseGCNFLineBS [ByteString]
ls
          }
      ([ByteString
"p",ByteString
"cnf", ByteString
nbvar', ByteString
nbclause']) ->
        forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$
          GCNF
          { gcnfNumVars :: Int
gcnfNumVars        = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nbvar'
          , gcnfNumClauses :: Int
gcnfNumClauses     = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nbclause'
          , gcnfLastGroupIndex :: Int
gcnfLastGroupIndex = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nbclause'
          , gcnfClauses :: [GClause]
gcnfClauses        = forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ByteString -> PackedClause
parseClauseBS [ByteString]
ls
          }
      [ByteString]
_ ->
        forall a b. a -> Either a b
Left String
"cannot find gcnf header"
    where
      l :: BS.ByteString
      ls :: [BS.ByteString]
      (ByteString
l:[ByteString]
ls) = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Bool
isCommentBS) (ByteString -> [ByteString]
BS.lines ByteString
s)

  render :: GCNF -> Builder
render GCNF
gcnf = Builder
header forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map GClause -> Builder
f (GCNF -> [GClause]
gcnfClauses GCNF
gcnf))
    where
      header :: Builder
header = forall a. Monoid a => [a] -> a
mconcat
        [ ByteString -> Builder
byteString ByteString
"p gcnf "
        , Int -> Builder
intDec (GCNF -> Int
gcnfNumVars GCNF
gcnf), Char -> Builder
char7 Char
' '
        , Int -> Builder
intDec (GCNF -> Int
gcnfNumClauses GCNF
gcnf), Char -> Builder
char7 Char
' '
        , Int -> Builder
intDec (GCNF -> Int
gcnfLastGroupIndex GCNF
gcnf), Char -> Builder
char7 Char
'\n'
        ]
      f :: GClause -> Builder
f (Int
idx,PackedClause
c) = Char -> Builder
char7 Char
'{' forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
idx forall a. Semigroup a => a -> a -> a
<> Char -> Builder
char7 Char
'}' forall a. Semigroup a => a -> a -> a
<>
                  forall a. Monoid a => [a] -> a
mconcat [Char -> Builder
char7 Char
' ' forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
lit | Int
lit <- PackedClause -> Clause
SAT.unpackClause PackedClause
c] forall a. Semigroup a => a -> a -> a
<>
                  ByteString -> Builder
byteString ByteString
" 0\n"

parseGCNFLineBS :: BS.ByteString -> GClause
parseGCNFLineBS :: ByteString -> GClause
parseGCNFLineBS ByteString
s
  | Just (Char
'{', ByteString
s1) <- ByteString -> Maybe (Char, ByteString)
BS.uncons ((Char -> Bool) -> ByteString -> ByteString
BS.dropWhile Char -> Bool
isSpace ByteString
s)
  , Just (!Int
idx,ByteString
s2) <- ByteString -> Maybe (Int, ByteString)
BS.readInt ByteString
s1
  , Just (Char
'}', ByteString
s3) <- ByteString -> Maybe (Char, ByteString)
BS.uncons ByteString
s2 =
      let ys :: PackedClause
ys = ByteString -> PackedClause
parseClauseBS ByteString
s3
      in seq :: forall a b. a -> b -> b
seq PackedClause
ys forall a b. (a -> b) -> a -> b
$ (Int
idx, PackedClause
ys)
  | Bool
otherwise = forall a. HasCallStack => String -> a
error String
"ToySolver.FileFormat.CNF: parse error"

-- -------------------------------------------------------------------

{-
http://www.qbflib.org/qdimacs.html

<input> ::= <preamble> <prefix> <matrix> EOF

<preamble> ::= [<comment_lines>] <problem_line>
<comment_lines> ::= <comment_line> <comment_lines> | <comment_line>
<comment_line> ::= c <text> EOL
<problem_line> ::= p cnf <pnum> <pnum> EOL

<prefix> ::= [<quant_sets>]
<quant_sets> ::= <quant_set> <quant_sets> | <quant_set>
<quant_set> ::= <quantifier> <atom_set> 0 EOL
<quantifier> ::= e | a
<atom_set> ::= <pnum> <atom_set> | <pnum>

<matrix> ::= <clause_list>
<clause_list> ::= <clause> <clause_list> | <clause>
<clause> ::= <literal> <clause> | <literal> 0 EOL
<literal> ::= <num>

<text> ::= {A sequence of non-special ASCII characters}
<num> ::= {A 32-bit signed integer different from 0}
<pnum> ::= {A 32-bit signed integer greater than 0}
-}

-- | QDIMACS format
--
-- Quantified boolean expression in prenex normal form,
-- consisting of a sequence of quantifiers ('qdimacsPrefix') and
-- a quantifier-free CNF part ('qdimacsMatrix').
--
-- References:
--
-- * QDIMACS standard Ver. 1.1
--   <http://www.qbflib.org/qdimacs.html>
data QDimacs
  = QDimacs
  { QDimacs -> Int
qdimacsNumVars :: !Int
    -- ^ Number of variables
  , QDimacs -> Int
qdimacsNumClauses :: !Int
    -- ^ Number of clauses
  , QDimacs -> [QuantSet]
qdimacsPrefix :: [QuantSet]
    -- ^ Sequence of quantifiers
  , QDimacs -> [PackedClause]
qdimacsMatrix :: [SAT.PackedClause]
    -- ^ Clauses
  }
  deriving (QDimacs -> QDimacs -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: QDimacs -> QDimacs -> Bool
$c/= :: QDimacs -> QDimacs -> Bool
== :: QDimacs -> QDimacs -> Bool
$c== :: QDimacs -> QDimacs -> Bool
Eq, Eq QDimacs
QDimacs -> QDimacs -> Bool
QDimacs -> QDimacs -> Ordering
QDimacs -> QDimacs -> QDimacs
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: QDimacs -> QDimacs -> QDimacs
$cmin :: QDimacs -> QDimacs -> QDimacs
max :: QDimacs -> QDimacs -> QDimacs
$cmax :: QDimacs -> QDimacs -> QDimacs
>= :: QDimacs -> QDimacs -> Bool
$c>= :: QDimacs -> QDimacs -> Bool
> :: QDimacs -> QDimacs -> Bool
$c> :: QDimacs -> QDimacs -> Bool
<= :: QDimacs -> QDimacs -> Bool
$c<= :: QDimacs -> QDimacs -> Bool
< :: QDimacs -> QDimacs -> Bool
$c< :: QDimacs -> QDimacs -> Bool
compare :: QDimacs -> QDimacs -> Ordering
$ccompare :: QDimacs -> QDimacs -> Ordering
Ord, Int -> QDimacs -> ShowS
[QDimacs] -> ShowS
QDimacs -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [QDimacs] -> ShowS
$cshowList :: [QDimacs] -> ShowS
show :: QDimacs -> String
$cshow :: QDimacs -> String
showsPrec :: Int -> QDimacs -> ShowS
$cshowsPrec :: Int -> QDimacs -> ShowS
Show, ReadPrec [QDimacs]
ReadPrec QDimacs
Int -> ReadS QDimacs
ReadS [QDimacs]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [QDimacs]
$creadListPrec :: ReadPrec [QDimacs]
readPrec :: ReadPrec QDimacs
$creadPrec :: ReadPrec QDimacs
readList :: ReadS [QDimacs]
$creadList :: ReadS [QDimacs]
readsPrec :: Int -> ReadS QDimacs
$creadsPrec :: Int -> ReadS QDimacs
Read)

-- | Quantifier
data Quantifier
  = E -- ^ existential quantifier (∃)
  | A -- ^ universal quantifier (∀)
  deriving (Quantifier -> Quantifier -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Quantifier -> Quantifier -> Bool
$c/= :: Quantifier -> Quantifier -> Bool
== :: Quantifier -> Quantifier -> Bool
$c== :: Quantifier -> Quantifier -> Bool
Eq, Eq Quantifier
Quantifier -> Quantifier -> Bool
Quantifier -> Quantifier -> Ordering
Quantifier -> Quantifier -> Quantifier
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Quantifier -> Quantifier -> Quantifier
$cmin :: Quantifier -> Quantifier -> Quantifier
max :: Quantifier -> Quantifier -> Quantifier
$cmax :: Quantifier -> Quantifier -> Quantifier
>= :: Quantifier -> Quantifier -> Bool
$c>= :: Quantifier -> Quantifier -> Bool
> :: Quantifier -> Quantifier -> Bool
$c> :: Quantifier -> Quantifier -> Bool
<= :: Quantifier -> Quantifier -> Bool
$c<= :: Quantifier -> Quantifier -> Bool
< :: Quantifier -> Quantifier -> Bool
$c< :: Quantifier -> Quantifier -> Bool
compare :: Quantifier -> Quantifier -> Ordering
$ccompare :: Quantifier -> Quantifier -> Ordering
Ord, Int -> Quantifier -> ShowS
[Quantifier] -> ShowS
Quantifier -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Quantifier] -> ShowS
$cshowList :: [Quantifier] -> ShowS
show :: Quantifier -> String
$cshow :: Quantifier -> String
showsPrec :: Int -> Quantifier -> ShowS
$cshowsPrec :: Int -> Quantifier -> ShowS
Show, ReadPrec [Quantifier]
ReadPrec Quantifier
Int -> ReadS Quantifier
ReadS [Quantifier]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Quantifier]
$creadListPrec :: ReadPrec [Quantifier]
readPrec :: ReadPrec Quantifier
$creadPrec :: ReadPrec Quantifier
readList :: ReadS [Quantifier]
$creadList :: ReadS [Quantifier]
readsPrec :: Int -> ReadS Quantifier
$creadsPrec :: Int -> ReadS Quantifier
Read, Int -> Quantifier
Quantifier -> Int
Quantifier -> [Quantifier]
Quantifier -> Quantifier
Quantifier -> Quantifier -> [Quantifier]
Quantifier -> Quantifier -> Quantifier -> [Quantifier]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Quantifier -> Quantifier -> Quantifier -> [Quantifier]
$cenumFromThenTo :: Quantifier -> Quantifier -> Quantifier -> [Quantifier]
enumFromTo :: Quantifier -> Quantifier -> [Quantifier]
$cenumFromTo :: Quantifier -> Quantifier -> [Quantifier]
enumFromThen :: Quantifier -> Quantifier -> [Quantifier]
$cenumFromThen :: Quantifier -> Quantifier -> [Quantifier]
enumFrom :: Quantifier -> [Quantifier]
$cenumFrom :: Quantifier -> [Quantifier]
fromEnum :: Quantifier -> Int
$cfromEnum :: Quantifier -> Int
toEnum :: Int -> Quantifier
$ctoEnum :: Int -> Quantifier
pred :: Quantifier -> Quantifier
$cpred :: Quantifier -> Quantifier
succ :: Quantifier -> Quantifier
$csucc :: Quantifier -> Quantifier
Enum, Quantifier
forall a. a -> a -> Bounded a
maxBound :: Quantifier
$cmaxBound :: Quantifier
minBound :: Quantifier
$cminBound :: Quantifier
Bounded)

-- | Quantified set of variables
type QuantSet = (Quantifier, [Atom])

-- | Synonym of 'SAT.Var'
type Atom = SAT.Var

instance FileFormat QDimacs where
  parse :: ByteString -> Either String QDimacs
parse = [ByteString] -> Either String QDimacs
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> [ByteString]
BS.lines
    where
      f :: [ByteString] -> Either String QDimacs
f [] = forall a b. a -> Either a b
Left String
"ToySolver.FileFormat.CNF.parse: premature end of file"
      f (ByteString
l : [ByteString]
ls) =
        case ByteString -> Maybe (Char, ByteString)
BS.uncons ByteString
l of
          Maybe (Char, ByteString)
Nothing -> forall a b. a -> Either a b
Left String
"ToySolver.FileFormat.CNF.parse: no problem line"
          Just (Char
'c', ByteString
_) -> [ByteString] -> Either String QDimacs
f [ByteString]
ls
          Just (Char
'p', ByteString
s) ->
            case ByteString -> [ByteString]
BS.words ByteString
s of
              [ByteString
"cnf", ByteString
numVars', ByteString
numClauses'] ->
                case [ByteString] -> ([QuantSet], [ByteString])
parsePrefix [ByteString]
ls of
                  ([QuantSet]
prefix', [ByteString]
ls') -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$
                    QDimacs
                    { qdimacsNumVars :: Int
qdimacsNumVars = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
numVars'
                    , qdimacsNumClauses :: Int
qdimacsNumClauses = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
numClauses'
                    , qdimacsPrefix :: [QuantSet]
qdimacsPrefix = [QuantSet]
prefix'
                    , qdimacsMatrix :: [PackedClause]
qdimacsMatrix = forall a b. (a -> b) -> [a] -> [b]
map ByteString -> PackedClause
parseClauseBS [ByteString]
ls'
                    }
              [ByteString]
_ -> forall a b. a -> Either a b
Left String
"ToySolver.FileFormat.CNF.parse: invalid problem line"
          Just (Char
c, ByteString
_) -> forall a b. a -> Either a b
Left (String
"ToySolver.FileFormat.CNF.parse: invalid prefix " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Char
c)

  render :: QDimacs -> Builder
render QDimacs
qdimacs = Builder
problem_line forall a. Semigroup a => a -> a -> a
<> Builder
prefix' forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map PackedClause -> Builder
f (QDimacs -> [PackedClause]
qdimacsMatrix QDimacs
qdimacs))
    where
      problem_line :: Builder
problem_line = forall a. Monoid a => [a] -> a
mconcat
        [ ByteString -> Builder
byteString ByteString
"p cnf "
        , Int -> Builder
intDec (QDimacs -> Int
qdimacsNumVars QDimacs
qdimacs), Char -> Builder
char7 Char
' '
        , Int -> Builder
intDec (QDimacs -> Int
qdimacsNumClauses QDimacs
qdimacs), Char -> Builder
char7 Char
'\n'
        ]
      prefix' :: Builder
prefix' = forall a. Monoid a => [a] -> a
mconcat
        [ Char -> Builder
char7 (if Quantifier
q forall a. Eq a => a -> a -> Bool
== Quantifier
E then Char
'e' else Char
'a') forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat [Char -> Builder
char7 Char
' ' forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
atom | Int
atom <- Clause
atoms] forall a. Semigroup a => a -> a -> a
<> ByteString -> Builder
byteString ByteString
" 0\n"
        | (Quantifier
q, Clause
atoms) <- QDimacs -> [QuantSet]
qdimacsPrefix QDimacs
qdimacs
        ]
      f :: PackedClause -> Builder
f PackedClause
c = forall a. Monoid a => [a] -> a
mconcat [Int -> Builder
intDec Int
lit forall a. Semigroup a => a -> a -> a
<> Char -> Builder
char7 Char
' '| Int
lit <- PackedClause -> Clause
SAT.unpackClause PackedClause
c] forall a. Semigroup a => a -> a -> a
<> ByteString -> Builder
byteString ByteString
"0\n"

parsePrefix :: [BS.ByteString] -> ([QuantSet], [BS.ByteString])
parsePrefix :: [ByteString] -> ([QuantSet], [ByteString])
parsePrefix = [QuantSet] -> [ByteString] -> ([QuantSet], [ByteString])
go []
  where
    go :: [QuantSet] -> [ByteString] -> ([QuantSet], [ByteString])
go [QuantSet]
result [] = (forall a. [a] -> [a]
reverse [QuantSet]
result, [])
    go [QuantSet]
result lls :: [ByteString]
lls@(ByteString
l : [ByteString]
ls) =
      case ByteString -> Maybe (Char, ByteString)
BS.uncons ByteString
l of
        Just (Char
c,ByteString
s)
          | Char
cforall a. Eq a => a -> a -> Bool
==Char
'a' Bool -> Bool -> Bool
|| Char
cforall a. Eq a => a -> a -> Bool
==Char
'e' ->
              let atoms :: Clause
atoms = ByteString -> Clause
readInts ByteString
s
                  q :: Quantifier
q = if Char
cforall a. Eq a => a -> a -> Bool
==Char
'a' then Quantifier
A else Quantifier
E
              in seq :: forall a b. a -> b -> b
seq Quantifier
q forall a b. (a -> b) -> a -> b
$ forall a b. NFData a => a -> b -> b
deepseq Clause
atoms forall a b. (a -> b) -> a -> b
$ [QuantSet] -> [ByteString] -> ([QuantSet], [ByteString])
go ((Quantifier
q, Clause
atoms) forall a. a -> [a] -> [a]
: [QuantSet]
result) [ByteString]
ls
          | Bool
otherwise ->
              (forall a. [a] -> [a]
reverse [QuantSet]
result, [ByteString]
lls)
        Maybe (Char, ByteString)
_ -> forall a. HasCallStack => String -> a
error String
"ToySolver.FileFormat.CNF.parseProblem: invalid line"

-- -------------------------------------------------------------------