{-# 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
(CNF -> CNF -> Bool) -> (CNF -> CNF -> Bool) -> Eq CNF
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
Eq CNF
-> (CNF -> CNF -> Ordering)
-> (CNF -> CNF -> Bool)
-> (CNF -> CNF -> Bool)
-> (CNF -> CNF -> Bool)
-> (CNF -> CNF -> Bool)
-> (CNF -> CNF -> CNF)
-> (CNF -> CNF -> CNF)
-> Ord 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
$cp1Ord :: Eq CNF
Ord, Int -> CNF -> ShowS
[CNF] -> ShowS
CNF -> String
(Int -> CNF -> ShowS)
-> (CNF -> String) -> ([CNF] -> ShowS) -> Show CNF
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]
(Int -> ReadS CNF)
-> ReadS [CNF] -> ReadPrec CNF -> ReadPrec [CNF] -> Read 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]) ->
        CNF -> Either String CNF
forall a b. b -> Either a b
Right (CNF -> Either String CNF) -> CNF -> Either String CNF
forall a b. (a -> b) -> a -> b
$
          CNF :: Int -> Int -> [PackedClause] -> CNF
CNF
          { cnfNumVars :: Int
cnfNumVars    = String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nvar
          , cnfNumClauses :: Int
cnfNumClauses = String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nclause
          , cnfClauses :: [PackedClause]
cnfClauses    = (ByteString -> PackedClause) -> [ByteString] -> [PackedClause]
forall a b. (a -> b) -> [a] -> [b]
map ByteString -> PackedClause
parseClauseBS [ByteString]
ls
          }
      [ByteString]
_ ->
        String -> Either String CNF
forall a b. a -> Either a b
Left String
"cannot find cnf header"
    where
      l :: BS.ByteString
      ls :: [BS.ByteString]
      (ByteString
l:[ByteString]
ls) = (ByteString -> Bool) -> [ByteString] -> [ByteString]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (ByteString -> Bool) -> ByteString -> Bool
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 Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat ((PackedClause -> Builder) -> [PackedClause] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
map PackedClause -> Builder
f (CNF -> [PackedClause]
cnfClauses CNF
cnf))
    where
      header :: Builder
header = [Builder] -> Builder
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 = [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat [Int -> Builder
intDec Int
lit Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Char -> Builder
char7 Char
' '| Int
lit <- PackedClause -> Clause
SAT.unpackClause PackedClause
c] Builder -> Builder -> Builder
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 Int -> Clause -> Clause
forall a. a -> [a] -> [a]
: ByteString -> Clause
readInts ByteString
s'
    Maybe (Int, ByteString)
Nothing -> String -> Clause
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 (Clause -> PackedClause)
-> (ByteString -> Clause) -> ByteString -> PackedClause
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
(WCNF -> WCNF -> Bool) -> (WCNF -> WCNF -> Bool) -> Eq WCNF
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
Eq WCNF
-> (WCNF -> WCNF -> Ordering)
-> (WCNF -> WCNF -> Bool)
-> (WCNF -> WCNF -> Bool)
-> (WCNF -> WCNF -> Bool)
-> (WCNF -> WCNF -> Bool)
-> (WCNF -> WCNF -> WCNF)
-> (WCNF -> WCNF -> WCNF)
-> Ord 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
$cp1Ord :: Eq WCNF
Ord, Int -> WCNF -> ShowS
[WCNF] -> ShowS
WCNF -> String
(Int -> WCNF -> ShowS)
-> (WCNF -> String) -> ([WCNF] -> ShowS) -> Show WCNF
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]
(Int -> ReadS WCNF)
-> ReadS [WCNF] -> ReadPrec WCNF -> ReadPrec [WCNF] -> Read 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 = (SomeWCNF -> WCNF) -> Either String SomeWCNF -> Either String WCNF
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM SomeWCNF -> WCNF
f (Either String SomeWCNF -> Either String WCNF)
-> (ByteString -> Either String SomeWCNF)
-> ByteString
-> Either String WCNF
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Either String SomeWCNF
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 Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat ((WeightedClause -> Builder) -> [WeightedClause] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
map WeightedClause -> Builder
f (WCNF -> [WeightedClause]
wcnfClauses WCNF
wcnf))
    where
      header :: Builder
header = [Builder] -> Builder
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 Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat [Char -> Builder
char7 Char
' ' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
lit | Int
lit <- PackedClause -> Clause
SAT.unpackClause PackedClause
c] Builder -> Builder -> Builder
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 -> String -> WeightedClause
forall a. HasCallStack => String -> a
error String
"ToySolver.FileFormat.CNF: no weight"
    Just (Weight
w, ByteString
s') -> Weight -> WeightedClause -> WeightedClause
seq Weight
w (WeightedClause -> WeightedClause)
-> WeightedClause -> WeightedClause
forall a b. (a -> b) -> a -> b
$ PackedClause -> WeightedClause -> WeightedClause
seq PackedClause
xs (WeightedClause -> WeightedClause)
-> WeightedClause -> WeightedClause
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
(NewWCNF -> NewWCNF -> Bool)
-> (NewWCNF -> NewWCNF -> Bool) -> Eq NewWCNF
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
Eq NewWCNF
-> (NewWCNF -> NewWCNF -> Ordering)
-> (NewWCNF -> NewWCNF -> Bool)
-> (NewWCNF -> NewWCNF -> Bool)
-> (NewWCNF -> NewWCNF -> Bool)
-> (NewWCNF -> NewWCNF -> Bool)
-> (NewWCNF -> NewWCNF -> NewWCNF)
-> (NewWCNF -> NewWCNF -> NewWCNF)
-> Ord 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
$cp1Ord :: Eq NewWCNF
Ord, Int -> NewWCNF -> ShowS
[NewWCNF] -> ShowS
NewWCNF -> String
(Int -> NewWCNF -> ShowS)
-> (NewWCNF -> String) -> ([NewWCNF] -> ShowS) -> Show NewWCNF
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]
(Int -> ReadS NewWCNF)
-> ReadS [NewWCNF]
-> ReadPrec NewWCNF
-> ReadPrec [NewWCNF]
-> Read 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 = (SomeWCNF -> NewWCNF)
-> Either String SomeWCNF -> Either String NewWCNF
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM SomeWCNF -> NewWCNF
f (Either String SomeWCNF -> Either String NewWCNF)
-> (ByteString -> Either String SomeWCNF)
-> ByteString
-> Either String NewWCNF
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Either String SomeWCNF
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 = [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat ((NewWeightedClause -> Builder) -> [NewWeightedClause] -> [Builder]
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' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat [Char -> Builder
char7 Char
' ' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
lit | Int
lit <- PackedClause -> Clause
SAT.unpackClause PackedClause
c] Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> ByteString -> Builder
byteString ByteString
" 0\n"
      f (Just Weight
w, PackedClause
c) = Weight -> Builder
integerDec Weight
w Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat [Char -> Builder
char7 Char
' ' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
lit | Int
lit <- PackedClause -> Clause
SAT.unpackClause PackedClause
c] Builder -> Builder -> Builder
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 -> String -> NewWeightedClause
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 PackedClause -> NewWeightedClause -> NewWeightedClause
seq PackedClause
xs (NewWeightedClause -> NewWeightedClause)
-> NewWeightedClause -> NewWeightedClause
forall a b. (a -> b) -> a -> b
$ (Maybe Weight
forall a. Maybe a
Nothing, PackedClause
xs)
    Just (Char, ByteString)
_ ->
      case ByteString -> Maybe (Weight, ByteString)
BS.readInteger ByteString
s' of
        Maybe (Weight, ByteString)
Nothing -> String -> NewWeightedClause
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 Weight -> NewWeightedClause -> NewWeightedClause
seq Weight
w (NewWeightedClause -> NewWeightedClause)
-> NewWeightedClause -> NewWeightedClause
forall a b. (a -> b) -> a -> b
$ PackedClause -> NewWeightedClause -> NewWeightedClause
seq PackedClause
xs (NewWeightedClause -> NewWeightedClause)
-> NewWeightedClause -> NewWeightedClause
forall a b. (a -> b) -> a -> b
$ (Weight -> Maybe Weight
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
(SomeWCNF -> SomeWCNF -> Bool)
-> (SomeWCNF -> SomeWCNF -> Bool) -> Eq SomeWCNF
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
Eq SomeWCNF
-> (SomeWCNF -> SomeWCNF -> Ordering)
-> (SomeWCNF -> SomeWCNF -> Bool)
-> (SomeWCNF -> SomeWCNF -> Bool)
-> (SomeWCNF -> SomeWCNF -> Bool)
-> (SomeWCNF -> SomeWCNF -> Bool)
-> (SomeWCNF -> SomeWCNF -> SomeWCNF)
-> (SomeWCNF -> SomeWCNF -> SomeWCNF)
-> Ord 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
$cp1Ord :: Eq SomeWCNF
Ord, Int -> SomeWCNF -> ShowS
[SomeWCNF] -> ShowS
SomeWCNF -> String
(Int -> SomeWCNF -> ShowS)
-> (SomeWCNF -> String) -> ([SomeWCNF] -> ShowS) -> Show SomeWCNF
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]
(Int -> ReadS SomeWCNF)
-> ReadS [SomeWCNF]
-> ReadPrec SomeWCNF
-> ReadPrec [SomeWCNF]
-> Read 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 :: Int -> Int -> Weight -> [WeightedClause] -> WCNF
WCNF
  { wcnfNumVars :: Int
wcnfNumVars = Clause -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 Int -> Clause -> Clause
forall a. a -> [a] -> [a]
: [Int -> Int
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 = [NewWeightedClause] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NewWeightedClause]
cs
  , wcnfTopCost :: Weight
wcnfTopCost = Weight
top
  , wcnfClauses :: [WeightedClause]
wcnfClauses = [(Weight -> Maybe Weight -> Weight
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 = [Weight] -> Weight
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Weight
w | (Just Weight
w, PackedClause
c) <- [NewWeightedClause]
cs] Weight -> Weight -> Weight
forall a. Num a => a -> a -> a
+ Weight
1

toNewWCNF :: WCNF -> NewWCNF
toNewWCNF :: WCNF -> NewWCNF
toNewWCNF WCNF
wcnf = [NewWeightedClause] -> NewWCNF
NewWCNF [(if Weight
w Weight -> Weight -> Bool
forall a. Ord a => a -> a -> Bool
>= WCNF -> Weight
wcnfTopCost WCNF
wcnf then Maybe Weight
forall a. Maybe a
Nothing else Weight -> Maybe Weight
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 (ByteString -> Bool) -> [ByteString] -> [ByteString]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (ByteString -> Bool) -> ByteString -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Bool
isCommentBS) (ByteString -> [ByteString]
BS.lines ByteString
s) of
      [] -> SomeWCNF -> Either String SomeWCNF
forall a b. b -> Either a b
Right (SomeWCNF -> Either String SomeWCNF)
-> SomeWCNF -> Either String SomeWCNF
forall a b. (a -> b) -> a -> b
$ NewWCNF -> SomeWCNF
SomeWCNFNew (NewWCNF -> SomeWCNF) -> NewWCNF -> SomeWCNF
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]) ->
            SomeWCNF -> Either String SomeWCNF
forall a b. b -> Either a b
Right (SomeWCNF -> Either String SomeWCNF)
-> SomeWCNF -> Either String SomeWCNF
forall a b. (a -> b) -> a -> b
$ WCNF -> SomeWCNF
SomeWCNFOld (WCNF -> SomeWCNF) -> WCNF -> SomeWCNF
forall a b. (a -> b) -> a -> b
$
              WCNF :: Int -> Int -> Weight -> [WeightedClause] -> WCNF
WCNF
              { wcnfNumVars :: Int
wcnfNumVars    = String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nvar
              , wcnfNumClauses :: Int
wcnfNumClauses = String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nclause
              , wcnfTopCost :: Weight
wcnfTopCost    = String -> Weight
forall a. Read a => String -> a
read (String -> Weight) -> String -> Weight
forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
top
              , wcnfClauses :: [WeightedClause]
wcnfClauses    = (ByteString -> WeightedClause) -> [ByteString] -> [WeightedClause]
forall a b. (a -> b) -> [a] -> [b]
map ByteString -> WeightedClause
parseWCNFLineBS [ByteString]
ls
              }
          ([ByteString
"p",ByteString
"wcnf", ByteString
nvar, ByteString
nclause]) ->
            SomeWCNF -> Either String SomeWCNF
forall a b. b -> Either a b
Right (SomeWCNF -> Either String SomeWCNF)
-> SomeWCNF -> Either String SomeWCNF
forall a b. (a -> b) -> a -> b
$ WCNF -> SomeWCNF
SomeWCNFOld (WCNF -> SomeWCNF) -> WCNF -> SomeWCNF
forall a b. (a -> b) -> a -> b
$
              WCNF :: Int -> Int -> Weight -> [WeightedClause] -> WCNF
WCNF
              { wcnfNumVars :: Int
wcnfNumVars    = String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nvar
              , wcnfNumClauses :: Int
wcnfNumClauses = String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
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    = Weight -> Weight
forall a. Num a => Weight -> a
fromInteger (Weight -> Weight) -> Weight -> Weight
forall a b. (a -> b) -> a -> b
$ Weight
2Weight -> Int -> Weight
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
63::Int) Weight -> Weight -> Weight
forall a. Num a => a -> a -> a
- Weight
1
              , wcnfClauses :: [WeightedClause]
wcnfClauses    = (ByteString -> WeightedClause) -> [ByteString] -> [WeightedClause]
forall a b. (a -> b) -> [a] -> [b]
map ByteString -> WeightedClause
parseWCNFLineBS [ByteString]
ls
              }
          ([ByteString
"p",ByteString
"cnf", ByteString
nvar, ByteString
nclause]) ->
            SomeWCNF -> Either String SomeWCNF
forall a b. b -> Either a b
Right (SomeWCNF -> Either String SomeWCNF)
-> SomeWCNF -> Either String SomeWCNF
forall a b. (a -> b) -> a -> b
$ WCNF -> SomeWCNF
SomeWCNFOld (WCNF -> SomeWCNF) -> WCNF -> SomeWCNF
forall a b. (a -> b) -> a -> b
$
              WCNF :: Int -> Int -> Weight -> [WeightedClause] -> WCNF
WCNF
              { wcnfNumVars :: Int
wcnfNumVars    = String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nvar
              , wcnfNumClauses :: Int
wcnfNumClauses = String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
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    = Weight -> Weight
forall a. Num a => Weight -> a
fromInteger (Weight -> Weight) -> Weight -> Weight
forall a b. (a -> b) -> a -> b
$ Weight
2Weight -> Int -> Weight
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
63::Int) Weight -> Weight -> Weight
forall a. Num a => a -> a -> a
- Weight
1
              , wcnfClauses :: [WeightedClause]
wcnfClauses    = (ByteString -> WeightedClause) -> [ByteString] -> [WeightedClause]
forall a b. (a -> b) -> [a] -> [b]
map ((\PackedClause
c -> PackedClause -> WeightedClause -> WeightedClause
seq PackedClause
c (Weight
1,PackedClause
c)) (PackedClause -> WeightedClause)
-> (ByteString -> PackedClause) -> ByteString -> WeightedClause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> PackedClause
parseClauseBS) [ByteString]
ls
              }
          (ByteString
"h" : [ByteString]
_) ->
            SomeWCNF -> Either String SomeWCNF
forall a b. b -> Either a b
Right (SomeWCNF -> Either String SomeWCNF)
-> SomeWCNF -> Either String SomeWCNF
forall a b. (a -> b) -> a -> b
$ NewWCNF -> SomeWCNF
SomeWCNFNew (NewWCNF -> SomeWCNF) -> NewWCNF -> SomeWCNF
forall a b. (a -> b) -> a -> b
$ [NewWeightedClause] -> NewWCNF
NewWCNF ([NewWeightedClause] -> NewWCNF) -> [NewWeightedClause] -> NewWCNF
forall a b. (a -> b) -> a -> b
$ (ByteString -> NewWeightedClause)
-> [ByteString] -> [NewWeightedClause]
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 ->
            SomeWCNF -> Either String SomeWCNF
forall a b. b -> Either a b
Right (SomeWCNF -> Either String SomeWCNF)
-> SomeWCNF -> Either String SomeWCNF
forall a b. (a -> b) -> a -> b
$ NewWCNF -> SomeWCNF
SomeWCNFNew (NewWCNF -> SomeWCNF) -> NewWCNF -> SomeWCNF
forall a b. (a -> b) -> a -> b
$ [NewWeightedClause] -> NewWCNF
NewWCNF ([NewWeightedClause] -> NewWCNF) -> [NewWeightedClause] -> NewWCNF
forall a b. (a -> b) -> a -> b
$ (ByteString -> NewWeightedClause)
-> [ByteString] -> [NewWeightedClause]
forall a b. (a -> b) -> [a] -> [b]
map ByteString -> NewWeightedClause
parseNewWCNFLineBS [ByteString]
lls
          [ByteString]
_ ->
            String -> Either String SomeWCNF
forall a b. a -> Either a b
Left String
"cannot find wcnf/cnf header"

  render :: SomeWCNF -> Builder
render (SomeWCNFOld WCNF
wcnf) = WCNF -> Builder
forall a. FileFormat a => a -> Builder
render WCNF
wcnf
  render (SomeWCNFNew NewWCNF
nwcnf) = NewWCNF -> Builder
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
(GCNF -> GCNF -> Bool) -> (GCNF -> GCNF -> Bool) -> Eq GCNF
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
Eq GCNF
-> (GCNF -> GCNF -> Ordering)
-> (GCNF -> GCNF -> Bool)
-> (GCNF -> GCNF -> Bool)
-> (GCNF -> GCNF -> Bool)
-> (GCNF -> GCNF -> Bool)
-> (GCNF -> GCNF -> GCNF)
-> (GCNF -> GCNF -> GCNF)
-> Ord 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
$cp1Ord :: Eq GCNF
Ord, Int -> GCNF -> ShowS
[GCNF] -> ShowS
GCNF -> String
(Int -> GCNF -> ShowS)
-> (GCNF -> String) -> ([GCNF] -> ShowS) -> Show GCNF
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]
(Int -> ReadS GCNF)
-> ReadS [GCNF] -> ReadPrec GCNF -> ReadPrec [GCNF] -> Read 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']) ->
        GCNF -> Either String GCNF
forall a b. b -> Either a b
Right (GCNF -> Either String GCNF) -> GCNF -> Either String GCNF
forall a b. (a -> b) -> a -> b
$
          GCNF :: Int -> Int -> Int -> [GClause] -> GCNF
GCNF
          { gcnfNumVars :: Int
gcnfNumVars        = String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nbvar'
          , gcnfNumClauses :: Int
gcnfNumClauses     = String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nbclauses'
          , gcnfLastGroupIndex :: Int
gcnfLastGroupIndex = String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
lastGroupIndex'
          , gcnfClauses :: [GClause]
gcnfClauses        = (ByteString -> GClause) -> [ByteString] -> [GClause]
forall a b. (a -> b) -> [a] -> [b]
map ByteString -> GClause
parseGCNFLineBS [ByteString]
ls
          }
      ([ByteString
"p",ByteString
"cnf", ByteString
nbvar', ByteString
nbclause']) ->
        GCNF -> Either String GCNF
forall a b. b -> Either a b
Right (GCNF -> Either String GCNF) -> GCNF -> Either String GCNF
forall a b. (a -> b) -> a -> b
$
          GCNF :: Int -> Int -> Int -> [GClause] -> GCNF
GCNF
          { gcnfNumVars :: Int
gcnfNumVars        = String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nbvar'
          , gcnfNumClauses :: Int
gcnfNumClauses     = String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nbclause'
          , gcnfLastGroupIndex :: Int
gcnfLastGroupIndex = String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nbclause'
          , gcnfClauses :: [GClause]
gcnfClauses        = Clause -> [PackedClause] -> [GClause]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] ([PackedClause] -> [GClause]) -> [PackedClause] -> [GClause]
forall a b. (a -> b) -> a -> b
$ (ByteString -> PackedClause) -> [ByteString] -> [PackedClause]
forall a b. (a -> b) -> [a] -> [b]
map ByteString -> PackedClause
parseClauseBS [ByteString]
ls
          }
      [ByteString]
_ ->
        String -> Either String GCNF
forall a b. a -> Either a b
Left String
"cannot find gcnf header"
    where
      l :: BS.ByteString
      ls :: [BS.ByteString]
      (ByteString
l:[ByteString]
ls) = (ByteString -> Bool) -> [ByteString] -> [ByteString]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (ByteString -> Bool) -> ByteString -> Bool
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 Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat ((GClause -> Builder) -> [GClause] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
map GClause -> Builder
f (GCNF -> [GClause]
gcnfClauses GCNF
gcnf))
    where
      header :: Builder
header = [Builder] -> Builder
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
'{' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
idx Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Char -> Builder
char7 Char
'}' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
                  [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat [Char -> Builder
char7 Char
' ' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
lit | Int
lit <- PackedClause -> Clause
SAT.unpackClause PackedClause
c] Builder -> Builder -> Builder
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 PackedClause -> GClause -> GClause
seq PackedClause
ys (GClause -> GClause) -> GClause -> GClause
forall a b. (a -> b) -> a -> b
$ (Int
idx, PackedClause
ys)
  | Bool
otherwise = String -> GClause
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
(QDimacs -> QDimacs -> Bool)
-> (QDimacs -> QDimacs -> Bool) -> Eq QDimacs
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
Eq QDimacs
-> (QDimacs -> QDimacs -> Ordering)
-> (QDimacs -> QDimacs -> Bool)
-> (QDimacs -> QDimacs -> Bool)
-> (QDimacs -> QDimacs -> Bool)
-> (QDimacs -> QDimacs -> Bool)
-> (QDimacs -> QDimacs -> QDimacs)
-> (QDimacs -> QDimacs -> QDimacs)
-> Ord 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
$cp1Ord :: Eq QDimacs
Ord, Int -> QDimacs -> ShowS
[QDimacs] -> ShowS
QDimacs -> String
(Int -> QDimacs -> ShowS)
-> (QDimacs -> String) -> ([QDimacs] -> ShowS) -> Show QDimacs
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]
(Int -> ReadS QDimacs)
-> ReadS [QDimacs]
-> ReadPrec QDimacs
-> ReadPrec [QDimacs]
-> Read 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
(Quantifier -> Quantifier -> Bool)
-> (Quantifier -> Quantifier -> Bool) -> Eq Quantifier
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
Eq Quantifier
-> (Quantifier -> Quantifier -> Ordering)
-> (Quantifier -> Quantifier -> Bool)
-> (Quantifier -> Quantifier -> Bool)
-> (Quantifier -> Quantifier -> Bool)
-> (Quantifier -> Quantifier -> Bool)
-> (Quantifier -> Quantifier -> Quantifier)
-> (Quantifier -> Quantifier -> Quantifier)
-> Ord 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
$cp1Ord :: Eq Quantifier
Ord, Int -> Quantifier -> ShowS
[Quantifier] -> ShowS
Quantifier -> String
(Int -> Quantifier -> ShowS)
-> (Quantifier -> String)
-> ([Quantifier] -> ShowS)
-> Show Quantifier
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]
(Int -> ReadS Quantifier)
-> ReadS [Quantifier]
-> ReadPrec Quantifier
-> ReadPrec [Quantifier]
-> Read 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]
(Quantifier -> Quantifier)
-> (Quantifier -> Quantifier)
-> (Int -> Quantifier)
-> (Quantifier -> Int)
-> (Quantifier -> [Quantifier])
-> (Quantifier -> Quantifier -> [Quantifier])
-> (Quantifier -> Quantifier -> [Quantifier])
-> (Quantifier -> Quantifier -> Quantifier -> [Quantifier])
-> Enum 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
Quantifier -> Quantifier -> Bounded 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 ([ByteString] -> Either String QDimacs)
-> (ByteString -> [ByteString])
-> ByteString
-> Either String QDimacs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> [ByteString]
BS.lines
    where
      f :: [ByteString] -> Either String QDimacs
f [] = String -> Either String QDimacs
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 -> String -> Either String QDimacs
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') -> QDimacs -> Either String QDimacs
forall a b. b -> Either a b
Right (QDimacs -> Either String QDimacs)
-> QDimacs -> Either String QDimacs
forall a b. (a -> b) -> a -> b
$
                    QDimacs :: Int -> Int -> [QuantSet] -> [PackedClause] -> QDimacs
QDimacs
                    { qdimacsNumVars :: Int
qdimacsNumVars = String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
numVars'
                    , qdimacsNumClauses :: Int
qdimacsNumClauses = String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
numClauses'
                    , qdimacsPrefix :: [QuantSet]
qdimacsPrefix = [QuantSet]
prefix'
                    , qdimacsMatrix :: [PackedClause]
qdimacsMatrix = (ByteString -> PackedClause) -> [ByteString] -> [PackedClause]
forall a b. (a -> b) -> [a] -> [b]
map ByteString -> PackedClause
parseClauseBS [ByteString]
ls'
                    }
              [ByteString]
_ -> String -> Either String QDimacs
forall a b. a -> Either a b
Left String
"ToySolver.FileFormat.CNF.parse: invalid problem line"
          Just (Char
c, ByteString
_) -> String -> Either String QDimacs
forall a b. a -> Either a b
Left (String
"ToySolver.FileFormat.CNF.parse: invalid prefix " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. Show a => a -> String
show Char
c)

  render :: QDimacs -> Builder
render QDimacs
qdimacs = Builder
problem_line Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
prefix' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat ((PackedClause -> Builder) -> [PackedClause] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
map PackedClause -> Builder
f (QDimacs -> [PackedClause]
qdimacsMatrix QDimacs
qdimacs))
    where
      problem_line :: Builder
problem_line = [Builder] -> Builder
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' = [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat
        [ Char -> Builder
char7 (if Quantifier
q Quantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
== Quantifier
E then Char
'e' else Char
'a') Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat [Char -> Builder
char7 Char
' ' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
atom | Int
atom <- Clause
atoms] Builder -> Builder -> Builder
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 = [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat [Int -> Builder
intDec Int
lit Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Char -> Builder
char7 Char
' '| Int
lit <- PackedClause -> Clause
SAT.unpackClause PackedClause
c] Builder -> Builder -> Builder
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 [] = ([QuantSet] -> [QuantSet]
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
cChar -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==Char
'a' Bool -> Bool -> Bool
|| Char
cChar -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==Char
'e' ->
              let atoms :: Clause
atoms = ByteString -> Clause
readInts ByteString
s
                  q :: Quantifier
q = if Char
cChar -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==Char
'a' then Quantifier
A else Quantifier
E
              in Quantifier
-> ([QuantSet], [ByteString]) -> ([QuantSet], [ByteString])
seq Quantifier
q (([QuantSet], [ByteString]) -> ([QuantSet], [ByteString]))
-> ([QuantSet], [ByteString]) -> ([QuantSet], [ByteString])
forall a b. (a -> b) -> a -> b
$ Clause -> ([QuantSet], [ByteString]) -> ([QuantSet], [ByteString])
forall a b. NFData a => a -> b -> b
deepseq Clause
atoms (([QuantSet], [ByteString]) -> ([QuantSet], [ByteString]))
-> ([QuantSet], [ByteString]) -> ([QuantSet], [ByteString])
forall a b. (a -> b) -> a -> b
$ [QuantSet] -> [ByteString] -> ([QuantSet], [ByteString])
go ((Quantifier
q, Clause
atoms) QuantSet -> [QuantSet] -> [QuantSet]
forall a. a -> [a] -> [a]
: [QuantSet]
result) [ByteString]
ls
          | Bool
otherwise ->
              ([QuantSet] -> [QuantSet]
forall a. [a] -> [a]
reverse [QuantSet]
result, [ByteString]
lls)
        Maybe (Char, ByteString)
_ -> String -> ([QuantSet], [ByteString])
forall a. HasCallStack => String -> a
error String
"ToySolver.FileFormat.CNF.parseProblem: invalid line"

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