{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE OverloadedStrings #-}
module ToySolver.FileFormat.CNF
(
module ToySolver.FileFormat.Base
, CNF (..)
, WCNF (..)
, WeightedClause
, Weight
, NewWCNF (..)
, SomeWCNF (..)
, GCNF (..)
, GroupIndex
, GClause
, QDimacs (..)
, Quantifier (..)
, QuantSet
, Atom
, 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)
data CNF
= CNF
{ CNF -> Int
cnfNumVars :: !Int
, CNF -> Int
cnfNumClauses :: !Int
, CNF -> [PackedClause]
cnfClauses :: [SAT.PackedClause]
}
deriving (CNF -> CNF -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CNF -> CNF -> Bool
$c/= :: CNF -> CNF -> Bool
== :: CNF -> CNF -> Bool
$c== :: CNF -> CNF -> Bool
Eq, Eq CNF
CNF -> CNF -> Bool
CNF -> CNF -> Ordering
CNF -> CNF -> CNF
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CNF -> CNF -> CNF
$cmin :: CNF -> CNF -> CNF
max :: CNF -> CNF -> CNF
$cmax :: CNF -> CNF -> CNF
>= :: CNF -> CNF -> Bool
$c>= :: CNF -> CNF -> Bool
> :: CNF -> CNF -> Bool
$c> :: CNF -> CNF -> Bool
<= :: CNF -> CNF -> Bool
$c<= :: CNF -> CNF -> Bool
< :: CNF -> CNF -> Bool
$c< :: CNF -> CNF -> Bool
compare :: CNF -> CNF -> Ordering
$ccompare :: CNF -> CNF -> Ordering
Ord, Int -> CNF -> ShowS
[CNF] -> ShowS
CNF -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CNF] -> ShowS
$cshowList :: [CNF] -> ShowS
show :: CNF -> String
$cshow :: CNF -> String
showsPrec :: Int -> CNF -> ShowS
$cshowsPrec :: Int -> CNF -> ShowS
Show, ReadPrec [CNF]
ReadPrec CNF
Int -> ReadS CNF
ReadS [CNF]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [CNF]
$creadListPrec :: ReadPrec [CNF]
readPrec :: ReadPrec CNF
$creadPrec :: ReadPrec CNF
readList :: ReadS [CNF]
$creadList :: ReadS [CNF]
readsPrec :: Int -> ReadS CNF
$creadsPrec :: Int -> ReadS CNF
Read)
instance FileFormat CNF where
parse :: ByteString -> Either String CNF
parse ByteString
s =
case ByteString -> [ByteString]
BS.words ByteString
l of
([ByteString
"p",ByteString
"cnf", ByteString
nvar, ByteString
nclause]) ->
forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$
CNF
{ cnfNumVars :: Int
cnfNumVars = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nvar
, cnfNumClauses :: Int
cnfNumClauses = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nclause
, cnfClauses :: [PackedClause]
cnfClauses = forall a b. (a -> b) -> [a] -> [b]
map ByteString -> PackedClause
parseClauseBS [ByteString]
ls
}
[ByteString]
_ ->
forall a b. a -> Either a b
Left String
"cannot find cnf header"
where
l :: BS.ByteString
ls :: [BS.ByteString]
(ByteString
l:[ByteString]
ls) = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Bool
isCommentBS) (ByteString -> [ByteString]
BS.lines ByteString
s)
render :: CNF -> Builder
render CNF
cnf = Builder
header forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map PackedClause -> Builder
f (CNF -> [PackedClause]
cnfClauses CNF
cnf))
where
header :: Builder
header = forall a. Monoid a => [a] -> a
mconcat
[ ByteString -> Builder
byteString ByteString
"p cnf "
, Int -> Builder
intDec (CNF -> Int
cnfNumVars CNF
cnf), Char -> Builder
char7 Char
' '
, Int -> Builder
intDec (CNF -> Int
cnfNumClauses CNF
cnf), Char -> Builder
char7 Char
'\n'
]
f :: PackedClause -> Builder
f PackedClause
c = forall a. Monoid a => [a] -> a
mconcat [Int -> Builder
intDec Int
lit forall a. Semigroup a => a -> a -> a
<> Char -> Builder
char7 Char
' '| Int
lit <- PackedClause -> Clause
SAT.unpackClause PackedClause
c] forall a. Semigroup a => a -> a -> a
<> ByteString -> Builder
byteString ByteString
"0\n"
readInts :: BS.ByteString -> [Int]
readInts :: ByteString -> Clause
readInts ByteString
s =
case ByteString -> Maybe (Int, ByteString)
BS.readInt ((Char -> Bool) -> ByteString -> ByteString
BS.dropWhile Char -> Bool
isSpace ByteString
s) of
Just (Int
0,ByteString
_) -> []
Just (Int
z,ByteString
s') -> Int
z forall a. a -> [a] -> [a]
: ByteString -> Clause
readInts ByteString
s'
Maybe (Int, ByteString)
Nothing -> forall a. HasCallStack => String -> a
error String
"ToySolver.FileFormat.CNF.readInts: 0 is missing"
parseClauseBS :: BS.ByteString -> SAT.PackedClause
parseClauseBS :: ByteString -> PackedClause
parseClauseBS = Clause -> PackedClause
SAT.packClause forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Clause
readInts
isCommentBS :: BS.ByteString -> Bool
ByteString
s =
case ByteString -> Maybe (Char, ByteString)
BS.uncons ByteString
s of
Just (Char
'c',ByteString
_) -> Bool
True
Maybe (Char, ByteString)
_ -> Bool
False
data WCNF
= WCNF
{ WCNF -> Int
wcnfNumVars :: !Int
, WCNF -> Int
wcnfNumClauses :: !Int
, WCNF -> Weight
wcnfTopCost :: !Weight
, WCNF -> [WeightedClause]
wcnfClauses :: [WeightedClause]
}
deriving (WCNF -> WCNF -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WCNF -> WCNF -> Bool
$c/= :: WCNF -> WCNF -> Bool
== :: WCNF -> WCNF -> Bool
$c== :: WCNF -> WCNF -> Bool
Eq, Eq WCNF
WCNF -> WCNF -> Bool
WCNF -> WCNF -> Ordering
WCNF -> WCNF -> WCNF
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: WCNF -> WCNF -> WCNF
$cmin :: WCNF -> WCNF -> WCNF
max :: WCNF -> WCNF -> WCNF
$cmax :: WCNF -> WCNF -> WCNF
>= :: WCNF -> WCNF -> Bool
$c>= :: WCNF -> WCNF -> Bool
> :: WCNF -> WCNF -> Bool
$c> :: WCNF -> WCNF -> Bool
<= :: WCNF -> WCNF -> Bool
$c<= :: WCNF -> WCNF -> Bool
< :: WCNF -> WCNF -> Bool
$c< :: WCNF -> WCNF -> Bool
compare :: WCNF -> WCNF -> Ordering
$ccompare :: WCNF -> WCNF -> Ordering
Ord, Int -> WCNF -> ShowS
[WCNF] -> ShowS
WCNF -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [WCNF] -> ShowS
$cshowList :: [WCNF] -> ShowS
show :: WCNF -> String
$cshow :: WCNF -> String
showsPrec :: Int -> WCNF -> ShowS
$cshowsPrec :: Int -> WCNF -> ShowS
Show, ReadPrec [WCNF]
ReadPrec WCNF
Int -> ReadS WCNF
ReadS [WCNF]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [WCNF]
$creadListPrec :: ReadPrec [WCNF]
readPrec :: ReadPrec WCNF
$creadPrec :: ReadPrec WCNF
readList :: ReadS [WCNF]
$creadList :: ReadS [WCNF]
readsPrec :: Int -> ReadS WCNF
$creadsPrec :: Int -> ReadS WCNF
Read)
type WeightedClause = (Weight, SAT.PackedClause)
type Weight = Integer
instance FileFormat WCNF where
parse :: ByteString -> Either String WCNF
parse = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM SomeWCNF -> WCNF
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FileFormat a => ByteString -> Either String a
parse
where
f :: SomeWCNF -> WCNF
f (SomeWCNFNew NewWCNF
x) = NewWCNF -> WCNF
toOldWCNF NewWCNF
x
f (SomeWCNFOld WCNF
x) = WCNF
x
render :: WCNF -> Builder
render WCNF
wcnf = Builder
header forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map WeightedClause -> Builder
f (WCNF -> [WeightedClause]
wcnfClauses WCNF
wcnf))
where
header :: Builder
header = forall a. Monoid a => [a] -> a
mconcat
[ ByteString -> Builder
byteString ByteString
"p wcnf "
, Int -> Builder
intDec (WCNF -> Int
wcnfNumVars WCNF
wcnf), Char -> Builder
char7 Char
' '
, Int -> Builder
intDec (WCNF -> Int
wcnfNumClauses WCNF
wcnf), Char -> Builder
char7 Char
' '
, Weight -> Builder
integerDec (WCNF -> Weight
wcnfTopCost WCNF
wcnf), Char -> Builder
char7 Char
'\n'
]
f :: WeightedClause -> Builder
f (Weight
w,PackedClause
c) = Weight -> Builder
integerDec Weight
w forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat [Char -> Builder
char7 Char
' ' forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
lit | Int
lit <- PackedClause -> Clause
SAT.unpackClause PackedClause
c] forall a. Semigroup a => a -> a -> a
<> ByteString -> Builder
byteString ByteString
" 0\n"
parseWCNFLineBS :: BS.ByteString -> WeightedClause
parseWCNFLineBS :: ByteString -> WeightedClause
parseWCNFLineBS ByteString
s =
case ByteString -> Maybe (Weight, ByteString)
BS.readInteger ((Char -> Bool) -> ByteString -> ByteString
BS.dropWhile Char -> Bool
isSpace ByteString
s) of
Maybe (Weight, ByteString)
Nothing -> forall a. HasCallStack => String -> a
error String
"ToySolver.FileFormat.CNF: no weight"
Just (Weight
w, ByteString
s') -> seq :: forall a b. a -> b -> b
seq Weight
w forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq PackedClause
xs forall a b. (a -> b) -> a -> b
$ (Weight
w, PackedClause
xs)
where
xs :: PackedClause
xs = ByteString -> PackedClause
parseClauseBS ByteString
s'
newtype NewWCNF
= NewWCNF
{ NewWCNF -> [NewWeightedClause]
nwcnfClauses :: [NewWeightedClause]
}
deriving (NewWCNF -> NewWCNF -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NewWCNF -> NewWCNF -> Bool
$c/= :: NewWCNF -> NewWCNF -> Bool
== :: NewWCNF -> NewWCNF -> Bool
$c== :: NewWCNF -> NewWCNF -> Bool
Eq, Eq NewWCNF
NewWCNF -> NewWCNF -> Bool
NewWCNF -> NewWCNF -> Ordering
NewWCNF -> NewWCNF -> NewWCNF
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: NewWCNF -> NewWCNF -> NewWCNF
$cmin :: NewWCNF -> NewWCNF -> NewWCNF
max :: NewWCNF -> NewWCNF -> NewWCNF
$cmax :: NewWCNF -> NewWCNF -> NewWCNF
>= :: NewWCNF -> NewWCNF -> Bool
$c>= :: NewWCNF -> NewWCNF -> Bool
> :: NewWCNF -> NewWCNF -> Bool
$c> :: NewWCNF -> NewWCNF -> Bool
<= :: NewWCNF -> NewWCNF -> Bool
$c<= :: NewWCNF -> NewWCNF -> Bool
< :: NewWCNF -> NewWCNF -> Bool
$c< :: NewWCNF -> NewWCNF -> Bool
compare :: NewWCNF -> NewWCNF -> Ordering
$ccompare :: NewWCNF -> NewWCNF -> Ordering
Ord, Int -> NewWCNF -> ShowS
[NewWCNF] -> ShowS
NewWCNF -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NewWCNF] -> ShowS
$cshowList :: [NewWCNF] -> ShowS
show :: NewWCNF -> String
$cshow :: NewWCNF -> String
showsPrec :: Int -> NewWCNF -> ShowS
$cshowsPrec :: Int -> NewWCNF -> ShowS
Show, ReadPrec [NewWCNF]
ReadPrec NewWCNF
Int -> ReadS NewWCNF
ReadS [NewWCNF]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [NewWCNF]
$creadListPrec :: ReadPrec [NewWCNF]
readPrec :: ReadPrec NewWCNF
$creadPrec :: ReadPrec NewWCNF
readList :: ReadS [NewWCNF]
$creadList :: ReadS [NewWCNF]
readsPrec :: Int -> ReadS NewWCNF
$creadsPrec :: Int -> ReadS NewWCNF
Read)
type NewWeightedClause = (Maybe Weight, SAT.PackedClause)
instance FileFormat NewWCNF where
parse :: ByteString -> Either String NewWCNF
parse = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM SomeWCNF -> NewWCNF
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FileFormat a => ByteString -> Either String a
parse
where
f :: SomeWCNF -> NewWCNF
f (SomeWCNFNew NewWCNF
x) = NewWCNF
x
f (SomeWCNFOld WCNF
x) = WCNF -> NewWCNF
toNewWCNF WCNF
x
render :: NewWCNF -> Builder
render NewWCNF
nwcnf = forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map NewWeightedClause -> Builder
f (NewWCNF -> [NewWeightedClause]
nwcnfClauses NewWCNF
nwcnf))
where
f :: NewWeightedClause -> Builder
f (Maybe Weight
Nothing, PackedClause
c) = Char -> Builder
char7 Char
'h' forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat [Char -> Builder
char7 Char
' ' forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
lit | Int
lit <- PackedClause -> Clause
SAT.unpackClause PackedClause
c] forall a. Semigroup a => a -> a -> a
<> ByteString -> Builder
byteString ByteString
" 0\n"
f (Just Weight
w, PackedClause
c) = Weight -> Builder
integerDec Weight
w forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat [Char -> Builder
char7 Char
' ' forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
lit | Int
lit <- PackedClause -> Clause
SAT.unpackClause PackedClause
c] forall a. Semigroup a => a -> a -> a
<> ByteString -> Builder
byteString ByteString
" 0\n"
parseNewWCNFLineBS :: BS.ByteString -> NewWeightedClause
parseNewWCNFLineBS :: ByteString -> NewWeightedClause
parseNewWCNFLineBS ByteString
s =
case ByteString -> Maybe (Char, ByteString)
BS.uncons ByteString
s' of
Maybe (Char, ByteString)
Nothing -> forall a. HasCallStack => String -> a
error String
"ToySolver.FileFormat.CNF: no weight"
Just (Char
'h', ByteString
s'') ->
let xs :: PackedClause
xs = ByteString -> PackedClause
parseClauseBS ByteString
s''
in seq :: forall a b. a -> b -> b
seq PackedClause
xs forall a b. (a -> b) -> a -> b
$ (forall a. Maybe a
Nothing, PackedClause
xs)
Just (Char, ByteString)
_ ->
case ByteString -> Maybe (Weight, ByteString)
BS.readInteger ByteString
s' of
Maybe (Weight, ByteString)
Nothing -> forall a. HasCallStack => String -> a
error String
"ToySolver.FileFormat.CNF: no weight"
Just (Weight
w, ByteString
s'') ->
let xs :: PackedClause
xs = ByteString -> PackedClause
parseClauseBS ByteString
s''
in seq :: forall a b. a -> b -> b
seq Weight
w forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq PackedClause
xs forall a b. (a -> b) -> a -> b
$ (forall a. a -> Maybe a
Just Weight
w, PackedClause
xs)
where
s' :: ByteString
s' = (Char -> Bool) -> ByteString -> ByteString
BS.dropWhile Char -> Bool
isSpace ByteString
s
data SomeWCNF
= SomeWCNFOld WCNF
| SomeWCNFNew NewWCNF
deriving (SomeWCNF -> SomeWCNF -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SomeWCNF -> SomeWCNF -> Bool
$c/= :: SomeWCNF -> SomeWCNF -> Bool
== :: SomeWCNF -> SomeWCNF -> Bool
$c== :: SomeWCNF -> SomeWCNF -> Bool
Eq, Eq SomeWCNF
SomeWCNF -> SomeWCNF -> Bool
SomeWCNF -> SomeWCNF -> Ordering
SomeWCNF -> SomeWCNF -> SomeWCNF
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SomeWCNF -> SomeWCNF -> SomeWCNF
$cmin :: SomeWCNF -> SomeWCNF -> SomeWCNF
max :: SomeWCNF -> SomeWCNF -> SomeWCNF
$cmax :: SomeWCNF -> SomeWCNF -> SomeWCNF
>= :: SomeWCNF -> SomeWCNF -> Bool
$c>= :: SomeWCNF -> SomeWCNF -> Bool
> :: SomeWCNF -> SomeWCNF -> Bool
$c> :: SomeWCNF -> SomeWCNF -> Bool
<= :: SomeWCNF -> SomeWCNF -> Bool
$c<= :: SomeWCNF -> SomeWCNF -> Bool
< :: SomeWCNF -> SomeWCNF -> Bool
$c< :: SomeWCNF -> SomeWCNF -> Bool
compare :: SomeWCNF -> SomeWCNF -> Ordering
$ccompare :: SomeWCNF -> SomeWCNF -> Ordering
Ord, Int -> SomeWCNF -> ShowS
[SomeWCNF] -> ShowS
SomeWCNF -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SomeWCNF] -> ShowS
$cshowList :: [SomeWCNF] -> ShowS
show :: SomeWCNF -> String
$cshow :: SomeWCNF -> String
showsPrec :: Int -> SomeWCNF -> ShowS
$cshowsPrec :: Int -> SomeWCNF -> ShowS
Show, ReadPrec [SomeWCNF]
ReadPrec SomeWCNF
Int -> ReadS SomeWCNF
ReadS [SomeWCNF]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [SomeWCNF]
$creadListPrec :: ReadPrec [SomeWCNF]
readPrec :: ReadPrec SomeWCNF
$creadPrec :: ReadPrec SomeWCNF
readList :: ReadS [SomeWCNF]
$creadList :: ReadS [SomeWCNF]
readsPrec :: Int -> ReadS SomeWCNF
$creadsPrec :: Int -> ReadS SomeWCNF
Read)
toOldWCNF :: NewWCNF -> WCNF
toOldWCNF :: NewWCNF -> WCNF
toOldWCNF (NewWCNF [NewWeightedClause]
cs)
= WCNF
{ wcnfNumVars :: Int
wcnfNumVars = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 forall a. a -> [a] -> [a]
: [forall a. Num a => a -> a
abs Int
l | (Maybe Weight
_, PackedClause
c) <- [NewWeightedClause]
cs, Int
l <- PackedClause -> Clause
unpackClause PackedClause
c])
, wcnfNumClauses :: Int
wcnfNumClauses = forall (t :: * -> *) a. Foldable t => t a -> Int
length [NewWeightedClause]
cs
, wcnfTopCost :: Weight
wcnfTopCost = Weight
top
, wcnfClauses :: [WeightedClause]
wcnfClauses = [(forall a. a -> Maybe a -> a
fromMaybe Weight
top Maybe Weight
w, PackedClause
c) | (Maybe Weight
w, PackedClause
c) <- [NewWeightedClause]
cs]
}
where
top :: Weight
top = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Weight
w | (Just Weight
w, PackedClause
c) <- [NewWeightedClause]
cs] forall a. Num a => a -> a -> a
+ Weight
1
toNewWCNF :: WCNF -> NewWCNF
toNewWCNF :: WCNF -> NewWCNF
toNewWCNF WCNF
wcnf = [NewWeightedClause] -> NewWCNF
NewWCNF [(if Weight
w forall a. Ord a => a -> a -> Bool
>= WCNF -> Weight
wcnfTopCost WCNF
wcnf then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just Weight
w, PackedClause
c) | (Weight
w, PackedClause
c) <- WCNF -> [WeightedClause]
wcnfClauses WCNF
wcnf]
instance FileFormat SomeWCNF where
parse :: ByteString -> Either String SomeWCNF
parse ByteString
s =
case forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Bool
isCommentBS) (ByteString -> [ByteString]
BS.lines ByteString
s) of
[] -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ NewWCNF -> SomeWCNF
SomeWCNFNew forall a b. (a -> b) -> a -> b
$ [NewWeightedClause] -> NewWCNF
NewWCNF []
lls :: [ByteString]
lls@(ByteString
l : [ByteString]
ls) ->
case ByteString -> [ByteString]
BS.words ByteString
l of
([ByteString
"p",ByteString
"wcnf", ByteString
nvar, ByteString
nclause, ByteString
top]) ->
forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ WCNF -> SomeWCNF
SomeWCNFOld forall a b. (a -> b) -> a -> b
$
WCNF
{ wcnfNumVars :: Int
wcnfNumVars = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nvar
, wcnfNumClauses :: Int
wcnfNumClauses = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nclause
, wcnfTopCost :: Weight
wcnfTopCost = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
top
, wcnfClauses :: [WeightedClause]
wcnfClauses = forall a b. (a -> b) -> [a] -> [b]
map ByteString -> WeightedClause
parseWCNFLineBS [ByteString]
ls
}
([ByteString
"p",ByteString
"wcnf", ByteString
nvar, ByteString
nclause]) ->
forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ WCNF -> SomeWCNF
SomeWCNFOld forall a b. (a -> b) -> a -> b
$
WCNF
{ wcnfNumVars :: Int
wcnfNumVars = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nvar
, wcnfNumClauses :: Int
wcnfNumClauses = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nclause
, wcnfTopCost :: Weight
wcnfTopCost = forall a. Num a => Weight -> a
fromInteger forall a b. (a -> b) -> a -> b
$ Weight
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
63::Int) forall a. Num a => a -> a -> a
- Weight
1
, wcnfClauses :: [WeightedClause]
wcnfClauses = forall a b. (a -> b) -> [a] -> [b]
map ByteString -> WeightedClause
parseWCNFLineBS [ByteString]
ls
}
([ByteString
"p",ByteString
"cnf", ByteString
nvar, ByteString
nclause]) ->
forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ WCNF -> SomeWCNF
SomeWCNFOld forall a b. (a -> b) -> a -> b
$
WCNF
{ wcnfNumVars :: Int
wcnfNumVars = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nvar
, wcnfNumClauses :: Int
wcnfNumClauses = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nclause
, wcnfTopCost :: Weight
wcnfTopCost = forall a. Num a => Weight -> a
fromInteger forall a b. (a -> b) -> a -> b
$ Weight
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
63::Int) forall a. Num a => a -> a -> a
- Weight
1
, wcnfClauses :: [WeightedClause]
wcnfClauses = forall a b. (a -> b) -> [a] -> [b]
map ((\PackedClause
c -> seq :: forall a b. a -> b -> b
seq PackedClause
c (Weight
1,PackedClause
c)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> PackedClause
parseClauseBS) [ByteString]
ls
}
(ByteString
"h" : [ByteString]
_) ->
forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ NewWCNF -> SomeWCNF
SomeWCNFNew forall a b. (a -> b) -> a -> b
$ [NewWeightedClause] -> NewWCNF
NewWCNF forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ByteString -> NewWeightedClause
parseNewWCNFLineBS [ByteString]
lls
(ByteString
s : [ByteString]
_) | Just (Weight, ByteString)
_ <- ByteString -> Maybe (Weight, ByteString)
BS.readInteger ByteString
s ->
forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ NewWCNF -> SomeWCNF
SomeWCNFNew forall a b. (a -> b) -> a -> b
$ [NewWeightedClause] -> NewWCNF
NewWCNF forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ByteString -> NewWeightedClause
parseNewWCNFLineBS [ByteString]
lls
[ByteString]
_ ->
forall a b. a -> Either a b
Left String
"cannot find wcnf/cnf header"
render :: SomeWCNF -> Builder
render (SomeWCNFOld WCNF
wcnf) = forall a. FileFormat a => a -> Builder
render WCNF
wcnf
render (SomeWCNFNew NewWCNF
nwcnf) = forall a. FileFormat a => a -> Builder
render NewWCNF
nwcnf
data GCNF
= GCNF
{ GCNF -> Int
gcnfNumVars :: !Int
, GCNF -> Int
gcnfNumClauses :: !Int
, GCNF -> Int
gcnfLastGroupIndex :: !GroupIndex
, GCNF -> [GClause]
gcnfClauses :: [GClause]
}
deriving (GCNF -> GCNF -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GCNF -> GCNF -> Bool
$c/= :: GCNF -> GCNF -> Bool
== :: GCNF -> GCNF -> Bool
$c== :: GCNF -> GCNF -> Bool
Eq, Eq GCNF
GCNF -> GCNF -> Bool
GCNF -> GCNF -> Ordering
GCNF -> GCNF -> GCNF
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: GCNF -> GCNF -> GCNF
$cmin :: GCNF -> GCNF -> GCNF
max :: GCNF -> GCNF -> GCNF
$cmax :: GCNF -> GCNF -> GCNF
>= :: GCNF -> GCNF -> Bool
$c>= :: GCNF -> GCNF -> Bool
> :: GCNF -> GCNF -> Bool
$c> :: GCNF -> GCNF -> Bool
<= :: GCNF -> GCNF -> Bool
$c<= :: GCNF -> GCNF -> Bool
< :: GCNF -> GCNF -> Bool
$c< :: GCNF -> GCNF -> Bool
compare :: GCNF -> GCNF -> Ordering
$ccompare :: GCNF -> GCNF -> Ordering
Ord, Int -> GCNF -> ShowS
[GCNF] -> ShowS
GCNF -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GCNF] -> ShowS
$cshowList :: [GCNF] -> ShowS
show :: GCNF -> String
$cshow :: GCNF -> String
showsPrec :: Int -> GCNF -> ShowS
$cshowsPrec :: Int -> GCNF -> ShowS
Show, ReadPrec [GCNF]
ReadPrec GCNF
Int -> ReadS GCNF
ReadS [GCNF]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [GCNF]
$creadListPrec :: ReadPrec [GCNF]
readPrec :: ReadPrec GCNF
$creadPrec :: ReadPrec GCNF
readList :: ReadS [GCNF]
$creadList :: ReadS [GCNF]
readsPrec :: Int -> ReadS GCNF
$creadsPrec :: Int -> ReadS GCNF
Read)
type GroupIndex = Int
type GClause = (GroupIndex, SAT.PackedClause)
instance FileFormat GCNF where
parse :: ByteString -> Either String GCNF
parse ByteString
s =
case ByteString -> [ByteString]
BS.words ByteString
l of
([ByteString
"p",ByteString
"gcnf", ByteString
nbvar', ByteString
nbclauses', ByteString
lastGroupIndex']) ->
forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$
GCNF
{ gcnfNumVars :: Int
gcnfNumVars = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nbvar'
, gcnfNumClauses :: Int
gcnfNumClauses = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nbclauses'
, gcnfLastGroupIndex :: Int
gcnfLastGroupIndex = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
lastGroupIndex'
, gcnfClauses :: [GClause]
gcnfClauses = forall a b. (a -> b) -> [a] -> [b]
map ByteString -> GClause
parseGCNFLineBS [ByteString]
ls
}
([ByteString
"p",ByteString
"cnf", ByteString
nbvar', ByteString
nbclause']) ->
forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$
GCNF
{ gcnfNumVars :: Int
gcnfNumVars = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nbvar'
, gcnfNumClauses :: Int
gcnfNumClauses = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nbclause'
, gcnfLastGroupIndex :: Int
gcnfLastGroupIndex = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
nbclause'
, gcnfClauses :: [GClause]
gcnfClauses = forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ByteString -> PackedClause
parseClauseBS [ByteString]
ls
}
[ByteString]
_ ->
forall a b. a -> Either a b
Left String
"cannot find gcnf header"
where
l :: BS.ByteString
ls :: [BS.ByteString]
(ByteString
l:[ByteString]
ls) = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Bool
isCommentBS) (ByteString -> [ByteString]
BS.lines ByteString
s)
render :: GCNF -> Builder
render GCNF
gcnf = Builder
header forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map GClause -> Builder
f (GCNF -> [GClause]
gcnfClauses GCNF
gcnf))
where
header :: Builder
header = forall a. Monoid a => [a] -> a
mconcat
[ ByteString -> Builder
byteString ByteString
"p gcnf "
, Int -> Builder
intDec (GCNF -> Int
gcnfNumVars GCNF
gcnf), Char -> Builder
char7 Char
' '
, Int -> Builder
intDec (GCNF -> Int
gcnfNumClauses GCNF
gcnf), Char -> Builder
char7 Char
' '
, Int -> Builder
intDec (GCNF -> Int
gcnfLastGroupIndex GCNF
gcnf), Char -> Builder
char7 Char
'\n'
]
f :: GClause -> Builder
f (Int
idx,PackedClause
c) = Char -> Builder
char7 Char
'{' forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
idx forall a. Semigroup a => a -> a -> a
<> Char -> Builder
char7 Char
'}' forall a. Semigroup a => a -> a -> a
<>
forall a. Monoid a => [a] -> a
mconcat [Char -> Builder
char7 Char
' ' forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
lit | Int
lit <- PackedClause -> Clause
SAT.unpackClause PackedClause
c] forall a. Semigroup a => a -> a -> a
<>
ByteString -> Builder
byteString ByteString
" 0\n"
parseGCNFLineBS :: BS.ByteString -> GClause
parseGCNFLineBS :: ByteString -> GClause
parseGCNFLineBS ByteString
s
| Just (Char
'{', ByteString
s1) <- ByteString -> Maybe (Char, ByteString)
BS.uncons ((Char -> Bool) -> ByteString -> ByteString
BS.dropWhile Char -> Bool
isSpace ByteString
s)
, Just (!Int
idx,ByteString
s2) <- ByteString -> Maybe (Int, ByteString)
BS.readInt ByteString
s1
, Just (Char
'}', ByteString
s3) <- ByteString -> Maybe (Char, ByteString)
BS.uncons ByteString
s2 =
let ys :: PackedClause
ys = ByteString -> PackedClause
parseClauseBS ByteString
s3
in seq :: forall a b. a -> b -> b
seq PackedClause
ys forall a b. (a -> b) -> a -> b
$ (Int
idx, PackedClause
ys)
| Bool
otherwise = forall a. HasCallStack => String -> a
error String
"ToySolver.FileFormat.CNF: parse error"
data QDimacs
= QDimacs
{ QDimacs -> Int
qdimacsNumVars :: !Int
, QDimacs -> Int
qdimacsNumClauses :: !Int
, QDimacs -> [QuantSet]
qdimacsPrefix :: [QuantSet]
, QDimacs -> [PackedClause]
qdimacsMatrix :: [SAT.PackedClause]
}
deriving (QDimacs -> QDimacs -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: QDimacs -> QDimacs -> Bool
$c/= :: QDimacs -> QDimacs -> Bool
== :: QDimacs -> QDimacs -> Bool
$c== :: QDimacs -> QDimacs -> Bool
Eq, Eq QDimacs
QDimacs -> QDimacs -> Bool
QDimacs -> QDimacs -> Ordering
QDimacs -> QDimacs -> QDimacs
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: QDimacs -> QDimacs -> QDimacs
$cmin :: QDimacs -> QDimacs -> QDimacs
max :: QDimacs -> QDimacs -> QDimacs
$cmax :: QDimacs -> QDimacs -> QDimacs
>= :: QDimacs -> QDimacs -> Bool
$c>= :: QDimacs -> QDimacs -> Bool
> :: QDimacs -> QDimacs -> Bool
$c> :: QDimacs -> QDimacs -> Bool
<= :: QDimacs -> QDimacs -> Bool
$c<= :: QDimacs -> QDimacs -> Bool
< :: QDimacs -> QDimacs -> Bool
$c< :: QDimacs -> QDimacs -> Bool
compare :: QDimacs -> QDimacs -> Ordering
$ccompare :: QDimacs -> QDimacs -> Ordering
Ord, Int -> QDimacs -> ShowS
[QDimacs] -> ShowS
QDimacs -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [QDimacs] -> ShowS
$cshowList :: [QDimacs] -> ShowS
show :: QDimacs -> String
$cshow :: QDimacs -> String
showsPrec :: Int -> QDimacs -> ShowS
$cshowsPrec :: Int -> QDimacs -> ShowS
Show, ReadPrec [QDimacs]
ReadPrec QDimacs
Int -> ReadS QDimacs
ReadS [QDimacs]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [QDimacs]
$creadListPrec :: ReadPrec [QDimacs]
readPrec :: ReadPrec QDimacs
$creadPrec :: ReadPrec QDimacs
readList :: ReadS [QDimacs]
$creadList :: ReadS [QDimacs]
readsPrec :: Int -> ReadS QDimacs
$creadsPrec :: Int -> ReadS QDimacs
Read)
data Quantifier
= E
| A
deriving (Quantifier -> Quantifier -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Quantifier -> Quantifier -> Bool
$c/= :: Quantifier -> Quantifier -> Bool
== :: Quantifier -> Quantifier -> Bool
$c== :: Quantifier -> Quantifier -> Bool
Eq, Eq Quantifier
Quantifier -> Quantifier -> Bool
Quantifier -> Quantifier -> Ordering
Quantifier -> Quantifier -> Quantifier
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Quantifier -> Quantifier -> Quantifier
$cmin :: Quantifier -> Quantifier -> Quantifier
max :: Quantifier -> Quantifier -> Quantifier
$cmax :: Quantifier -> Quantifier -> Quantifier
>= :: Quantifier -> Quantifier -> Bool
$c>= :: Quantifier -> Quantifier -> Bool
> :: Quantifier -> Quantifier -> Bool
$c> :: Quantifier -> Quantifier -> Bool
<= :: Quantifier -> Quantifier -> Bool
$c<= :: Quantifier -> Quantifier -> Bool
< :: Quantifier -> Quantifier -> Bool
$c< :: Quantifier -> Quantifier -> Bool
compare :: Quantifier -> Quantifier -> Ordering
$ccompare :: Quantifier -> Quantifier -> Ordering
Ord, Int -> Quantifier -> ShowS
[Quantifier] -> ShowS
Quantifier -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Quantifier] -> ShowS
$cshowList :: [Quantifier] -> ShowS
show :: Quantifier -> String
$cshow :: Quantifier -> String
showsPrec :: Int -> Quantifier -> ShowS
$cshowsPrec :: Int -> Quantifier -> ShowS
Show, ReadPrec [Quantifier]
ReadPrec Quantifier
Int -> ReadS Quantifier
ReadS [Quantifier]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Quantifier]
$creadListPrec :: ReadPrec [Quantifier]
readPrec :: ReadPrec Quantifier
$creadPrec :: ReadPrec Quantifier
readList :: ReadS [Quantifier]
$creadList :: ReadS [Quantifier]
readsPrec :: Int -> ReadS Quantifier
$creadsPrec :: Int -> ReadS Quantifier
Read, Int -> Quantifier
Quantifier -> Int
Quantifier -> [Quantifier]
Quantifier -> Quantifier
Quantifier -> Quantifier -> [Quantifier]
Quantifier -> Quantifier -> Quantifier -> [Quantifier]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Quantifier -> Quantifier -> Quantifier -> [Quantifier]
$cenumFromThenTo :: Quantifier -> Quantifier -> Quantifier -> [Quantifier]
enumFromTo :: Quantifier -> Quantifier -> [Quantifier]
$cenumFromTo :: Quantifier -> Quantifier -> [Quantifier]
enumFromThen :: Quantifier -> Quantifier -> [Quantifier]
$cenumFromThen :: Quantifier -> Quantifier -> [Quantifier]
enumFrom :: Quantifier -> [Quantifier]
$cenumFrom :: Quantifier -> [Quantifier]
fromEnum :: Quantifier -> Int
$cfromEnum :: Quantifier -> Int
toEnum :: Int -> Quantifier
$ctoEnum :: Int -> Quantifier
pred :: Quantifier -> Quantifier
$cpred :: Quantifier -> Quantifier
succ :: Quantifier -> Quantifier
$csucc :: Quantifier -> Quantifier
Enum, Quantifier
forall a. a -> a -> Bounded a
maxBound :: Quantifier
$cmaxBound :: Quantifier
minBound :: Quantifier
$cminBound :: Quantifier
Bounded)
type QuantSet = (Quantifier, [Atom])
type Atom = SAT.Var
instance FileFormat QDimacs where
parse :: ByteString -> Either String QDimacs
parse = [ByteString] -> Either String QDimacs
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> [ByteString]
BS.lines
where
f :: [ByteString] -> Either String QDimacs
f [] = forall a b. a -> Either a b
Left String
"ToySolver.FileFormat.CNF.parse: premature end of file"
f (ByteString
l : [ByteString]
ls) =
case ByteString -> Maybe (Char, ByteString)
BS.uncons ByteString
l of
Maybe (Char, ByteString)
Nothing -> forall a b. a -> Either a b
Left String
"ToySolver.FileFormat.CNF.parse: no problem line"
Just (Char
'c', ByteString
_) -> [ByteString] -> Either String QDimacs
f [ByteString]
ls
Just (Char
'p', ByteString
s) ->
case ByteString -> [ByteString]
BS.words ByteString
s of
[ByteString
"cnf", ByteString
numVars', ByteString
numClauses'] ->
case [ByteString] -> ([QuantSet], [ByteString])
parsePrefix [ByteString]
ls of
([QuantSet]
prefix', [ByteString]
ls') -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$
QDimacs
{ qdimacsNumVars :: Int
qdimacsNumVars = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
numVars'
, qdimacsNumClauses :: Int
qdimacsNumClauses = forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ ByteString -> String
BS.unpack ByteString
numClauses'
, qdimacsPrefix :: [QuantSet]
qdimacsPrefix = [QuantSet]
prefix'
, qdimacsMatrix :: [PackedClause]
qdimacsMatrix = forall a b. (a -> b) -> [a] -> [b]
map ByteString -> PackedClause
parseClauseBS [ByteString]
ls'
}
[ByteString]
_ -> forall a b. a -> Either a b
Left String
"ToySolver.FileFormat.CNF.parse: invalid problem line"
Just (Char
c, ByteString
_) -> forall a b. a -> Either a b
Left (String
"ToySolver.FileFormat.CNF.parse: invalid prefix " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Char
c)
render :: QDimacs -> Builder
render QDimacs
qdimacs = Builder
problem_line forall a. Semigroup a => a -> a -> a
<> Builder
prefix' forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map PackedClause -> Builder
f (QDimacs -> [PackedClause]
qdimacsMatrix QDimacs
qdimacs))
where
problem_line :: Builder
problem_line = forall a. Monoid a => [a] -> a
mconcat
[ ByteString -> Builder
byteString ByteString
"p cnf "
, Int -> Builder
intDec (QDimacs -> Int
qdimacsNumVars QDimacs
qdimacs), Char -> Builder
char7 Char
' '
, Int -> Builder
intDec (QDimacs -> Int
qdimacsNumClauses QDimacs
qdimacs), Char -> Builder
char7 Char
'\n'
]
prefix' :: Builder
prefix' = forall a. Monoid a => [a] -> a
mconcat
[ Char -> Builder
char7 (if Quantifier
q forall a. Eq a => a -> a -> Bool
== Quantifier
E then Char
'e' else Char
'a') forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat [Char -> Builder
char7 Char
' ' forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
atom | Int
atom <- Clause
atoms] forall a. Semigroup a => a -> a -> a
<> ByteString -> Builder
byteString ByteString
" 0\n"
| (Quantifier
q, Clause
atoms) <- QDimacs -> [QuantSet]
qdimacsPrefix QDimacs
qdimacs
]
f :: PackedClause -> Builder
f PackedClause
c = forall a. Monoid a => [a] -> a
mconcat [Int -> Builder
intDec Int
lit forall a. Semigroup a => a -> a -> a
<> Char -> Builder
char7 Char
' '| Int
lit <- PackedClause -> Clause
SAT.unpackClause PackedClause
c] forall a. Semigroup a => a -> a -> a
<> ByteString -> Builder
byteString ByteString
"0\n"
parsePrefix :: [BS.ByteString] -> ([QuantSet], [BS.ByteString])
parsePrefix :: [ByteString] -> ([QuantSet], [ByteString])
parsePrefix = [QuantSet] -> [ByteString] -> ([QuantSet], [ByteString])
go []
where
go :: [QuantSet] -> [ByteString] -> ([QuantSet], [ByteString])
go [QuantSet]
result [] = (forall a. [a] -> [a]
reverse [QuantSet]
result, [])
go [QuantSet]
result lls :: [ByteString]
lls@(ByteString
l : [ByteString]
ls) =
case ByteString -> Maybe (Char, ByteString)
BS.uncons ByteString
l of
Just (Char
c,ByteString
s)
| Char
cforall a. Eq a => a -> a -> Bool
==Char
'a' Bool -> Bool -> Bool
|| Char
cforall a. Eq a => a -> a -> Bool
==Char
'e' ->
let atoms :: Clause
atoms = ByteString -> Clause
readInts ByteString
s
q :: Quantifier
q = if Char
cforall a. Eq a => a -> a -> Bool
==Char
'a' then Quantifier
A else Quantifier
E
in seq :: forall a b. a -> b -> b
seq Quantifier
q forall a b. (a -> b) -> a -> b
$ forall a b. NFData a => a -> b -> b
deepseq Clause
atoms forall a b. (a -> b) -> a -> b
$ [QuantSet] -> [ByteString] -> ([QuantSet], [ByteString])
go ((Quantifier
q, Clause
atoms) forall a. a -> [a] -> [a]
: [QuantSet]
result) [ByteString]
ls
| Bool
otherwise ->
(forall a. [a] -> [a]
reverse [QuantSet]
result, [ByteString]
lls)
Maybe (Char, ByteString)
_ -> forall a. HasCallStack => String -> a
error String
"ToySolver.FileFormat.CNF.parseProblem: invalid line"