{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# 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 format
  , WCNF (..)
  , WeightedClause
  , Weight

  -- * 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 qualified Data.ByteString.Lazy.Char8 as BS
import Data.ByteString.Builder
import Data.Char
#if !MIN_VERSION_base(4,11,0)
import Data.Monoid
#endif

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

instance FileFormat WCNF where
  parse :: ByteString -> Either String WCNF
parse ByteString
s =
    case ByteString -> [ByteString]
BS.words ByteString
l of
      ([ByteString
"p",ByteString
"wcnf", ByteString
nvar, ByteString
nclause, ByteString
top]) ->
        WCNF -> Either String WCNF
forall a b. b -> Either a b
Right (WCNF -> Either String WCNF) -> WCNF -> Either String WCNF
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]) ->
        WCNF -> Either String WCNF
forall a b. b -> Either a b
Right (WCNF -> Either String WCNF) -> WCNF -> Either String WCNF
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]) ->
        WCNF -> Either String WCNF
forall a b. b -> Either a b
Right (WCNF -> Either String WCNF) -> WCNF -> Either String WCNF
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]
_ ->
        String -> Either String WCNF
forall a b. a -> Either a b
Left String
"cannot find wcnf/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 :: 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'

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

-- | 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"

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