msakai / toysolver / 563

Committed 15 Dec 2024 01:20AM UTC coverage: 71.768% (+0.5%) from 71.267%

Build # 563

Build Type

push

github

Committed by

web-flow

Commit Message

update URL of “Existential Quantification as Incremental SAT”

Run Details

10438 of 14544 relevant lines covered (71.77%)

0.72 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

82.87

/src/ToySolver/FileFormat/CNF.hs

{-# 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
  { cnfNumVars :: !Int
    -- ^ Number of variables
  , cnfNumClauses :: !Int
    -- ^ Number of clauses
  , cnfClauses :: [SAT.PackedClause]
    -- ^ Clauses
  }
  deriving (Eq, Ord, Show, Read)

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

  render cnf = header <> mconcat (map f (cnfClauses cnf))
    where
      header = mconcat
        [ byteString "p cnf "
        , intDec (cnfNumVars cnf), char7 ' '
        , intDec (cnfNumClauses cnf), char7 '\n'
        ]
      f c = mconcat [intDec lit <> char7 ' '| lit <- SAT.unpackClause c] <> byteString "0\n"

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

parseClauseBS :: BS.ByteString -> SAT.PackedClause
parseClauseBS = SAT.packClause . readInts

isCommentBS :: BS.ByteString -> Bool
isCommentBS s =
  case BS.uncons s of
    Just ('c',_) ->  True
    _ -> 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
  { wcnfNumVars    :: !Int
    -- ^ Number of variables
  , wcnfNumClauses :: !Int
    -- ^ Number of (weighted) clauses
  , 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.
  , wcnfClauses    :: [WeightedClause]
    -- ^ Weighted clauses
  }
  deriving (Eq, Ord, Show, 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 = liftM f . parse
    where
      f (SomeWCNFNew x) = toOldWCNF x
      f (SomeWCNFOld x) = x

  render wcnf = header <> mconcat (map f (wcnfClauses wcnf))
    where
      header = mconcat
        [ byteString "p wcnf "
        , intDec (wcnfNumVars wcnf), char7 ' '
        , intDec (wcnfNumClauses wcnf), char7 ' '
        , integerDec (wcnfTopCost wcnf), char7 '\n'
        ]
      f (w,c) = integerDec w <> mconcat [char7 ' ' <> intDec lit | lit <- SAT.unpackClause c] <> byteString " 0\n"

parseWCNFLineBS :: BS.ByteString -> WeightedClause
parseWCNFLineBS s =
  case BS.readInteger (BS.dropWhile isSpace s) of
    Nothing -> error "ToySolver.FileFormat.CNF: no weight"
    Just (w, s') -> seq w $ seq xs $ (w, xs)
      where
        xs = parseClauseBS 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
  { nwcnfClauses :: [NewWeightedClause]
    -- ^ Weighted clauses
  }
  deriving (Eq, Ord, Show, 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 = liftM f . parse
    where
      f (SomeWCNFNew x) = x
      f (SomeWCNFOld x) = toNewWCNF x

  render nwcnf = mconcat (map f (nwcnfClauses nwcnf))
    where
      f (Nothing, c) = char7 'h' <> mconcat [char7 ' ' <> intDec lit | lit <- SAT.unpackClause c] <> byteString " 0\n"
      f (Just w, c) = integerDec w <> mconcat [char7 ' ' <> intDec lit | lit <- SAT.unpackClause c] <> byteString " 0\n"

parseNewWCNFLineBS :: BS.ByteString -> NewWeightedClause
parseNewWCNFLineBS s =
  case BS.uncons s' of
    Nothing -> error "ToySolver.FileFormat.CNF: no weight"
    Just ('h', s'') ->
      let xs = parseClauseBS s''
       in seq xs $ (Nothing, xs)
    Just _ ->
      case BS.readInteger s' of
        Nothing -> error "ToySolver.FileFormat.CNF: no weight"
        Just (w, s'') ->
          let xs = parseClauseBS s''
           in seq w $ seq xs $ (Just w, xs)
  where
    s' = BS.dropWhile isSpace s

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

data SomeWCNF
  = SomeWCNFOld WCNF
  | SomeWCNFNew NewWCNF
  deriving (Eq, Ord, Show, Read)

toOldWCNF :: NewWCNF -> WCNF
toOldWCNF (NewWCNF cs)
  = WCNF
  { wcnfNumVars = maximum (0 : [abs l | (_, c) <- cs, l <- unpackClause c])
  , wcnfNumClauses = length cs
  , wcnfTopCost = top
  , wcnfClauses = [(fromMaybe top w, c) | (w, c) <- cs]
  }
  where
    top = sum [w | (Just w, _c) <- cs] + 1

toNewWCNF :: WCNF -> NewWCNF
toNewWCNF wcnf = NewWCNF [(if w >= wcnfTopCost wcnf then Nothing else Just w, c) | (w, c) <- wcnfClauses wcnf]

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

  render (SomeWCNFOld wcnf) = render wcnf
  render (SomeWCNFNew nwcnf) = render 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
  { gcnfNumVars        :: !Int
    -- ^ Nubmer of variables
  , gcnfNumClauses     :: !Int
    -- ^ Number of clauses
  , gcnfLastGroupIndex :: !GroupIndex
    -- ^ The last index of a group in the file number of components contained in the file.
  , gcnfClauses        :: [GClause]
  }
  deriving (Eq, Ord, Show, 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 s =
    case BS.words l of
      (["p","gcnf", nbvar', nbclauses', lastGroupIndex']) ->
        Right $
          GCNF
          { gcnfNumVars        = read $ BS.unpack nbvar'
          , gcnfNumClauses     = read $ BS.unpack nbclauses'
          , gcnfLastGroupIndex = read $ BS.unpack lastGroupIndex'
          , gcnfClauses        = map parseGCNFLineBS ls
          }
      (["p","cnf", nbvar', nbclause']) ->
        Right $
          GCNF
          { gcnfNumVars        = read $ BS.unpack nbvar'
          , gcnfNumClauses     = read $ BS.unpack nbclause'
          , gcnfLastGroupIndex = read $ BS.unpack nbclause'
          , gcnfClauses        = zip [1..] $ map parseClauseBS ls
          }
      _ ->
        Left "cannot find gcnf header"
    where
      l :: BS.ByteString
      ls :: [BS.ByteString]
      (l:ls) = filter (not . isCommentBS) (BS.lines s)

  render gcnf = header <> mconcat (map f (gcnfClauses gcnf))
    where
      header = mconcat
        [ byteString "p gcnf "
        , intDec (gcnfNumVars gcnf), char7 ' '
        , intDec (gcnfNumClauses gcnf), char7 ' '
        , intDec (gcnfLastGroupIndex gcnf), char7 '\n'
        ]
      f (idx,c) = char7 '{' <> intDec idx <> char7 '}' <>
                  mconcat [char7 ' ' <> intDec lit | lit <- SAT.unpackClause c] <>
                  byteString " 0\n"

parseGCNFLineBS :: BS.ByteString -> GClause
parseGCNFLineBS s
  | Just ('{', s1) <- BS.uncons (BS.dropWhile isSpace s)
  , Just (!idx,s2) <- BS.readInt s1
  , Just ('}', s3) <- BS.uncons s2 =
      let ys = parseClauseBS s3
      in seq ys $ (idx, ys)
  | otherwise = error "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
  { qdimacsNumVars :: !Int
    -- ^ Number of variables
  , qdimacsNumClauses :: !Int
    -- ^ Number of clauses
  , qdimacsPrefix :: [QuantSet]
    -- ^ Sequence of quantifiers
  , qdimacsMatrix :: [SAT.PackedClause]
    -- ^ Clauses
  }
  deriving (Eq, Ord, Show, Read)

-- | Quantifier
data Quantifier
  = E -- ^ existential quantifier (∃)
  | A -- ^ universal quantifier (∀)
  deriving (Eq, Ord, Show, Read, Enum, Bounded)

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

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

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

  render qdimacs = problem_line <> prefix' <> mconcat (map f (qdimacsMatrix qdimacs))
    where
      problem_line = mconcat
        [ byteString "p cnf "
        , intDec (qdimacsNumVars qdimacs), char7 ' '
        , intDec (qdimacsNumClauses qdimacs), char7 '\n'
        ]
      prefix' = mconcat
        [ char7 (if q == E then 'e' else 'a') <> mconcat [char7 ' ' <> intDec atom | atom <- atoms] <> byteString " 0\n"
        | (q, atoms) <- qdimacsPrefix qdimacs
        ]
      f c = mconcat [intDec lit <> char7 ' '| lit <- SAT.unpackClause c] <> byteString "0\n"

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

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

1	{-# OPTIONS_GHC -Wall #-}
2	{-# OPTIONS_HADDOCK show-extensions #-}
3	{-# LANGUAGE BangPatterns #-}
4	{-# LANGUAGE OverloadedStrings #-}
5	-----------------------------------------------------------------------------
6	-- \|
7	-- Module : ToySolver.FileFormat.CNF
8	-- Copyright : (c) Masahiro Sakai 2016-2018
9	-- License : BSD-style
10	--
11	-- Maintainer : masahiro.sakai@gmail.com
12	-- Stability : provisional
13	-- Portability : non-portable
14	--
15	-- Reader and Writer for DIMACS CNF and family of similar formats.
16	--
17	-----------------------------------------------------------------------------
18	module ToySolver.FileFormat.CNF
19	(
20	-- * FileFormat class
21	module ToySolver.FileFormat.Base
22
23	-- * CNF format
24	, CNF (..)
25
26	-- * WCNF formats
27
28	-- ** (Old) WCNF format
29	, WCNF (..)
30	, WeightedClause
31	, Weight
32
33	-- ** New WCNF format
34	, NewWCNF (..)
35
36	-- ** Old or new WCNF
37	, SomeWCNF (..)
38
39	-- * GCNF format
40	, GCNF (..)
41	, GroupIndex
42	, GClause
43
44	-- * QDIMACS format
45	, QDimacs (..)
46	, Quantifier (..)
47	, QuantSet
48	, Atom
49
50	-- * Re-exports
51	, Lit
52	, Clause
53	, PackedClause
54	, packClause
55	, unpackClause
56	) where
57
58	import Prelude hiding (readFile, writeFile)
59	import Control.DeepSeq
60	import Control.Monad
61	import qualified Data.ByteString.Lazy.Char8 as BS
62	import Data.ByteString.Builder
63	import Data.Char
64	import Data.Maybe
65
66	import ToySolver.FileFormat.Base
67	import qualified ToySolver.SAT.Types as SAT
68	import ToySolver.SAT.Types (Lit, Clause, PackedClause, packClause, unpackClause)
69
70	-- -------------------------------------------------------------------
71
72	-- \| DIMACS CNF format
73	data CNF
74	= CNF
75	{ cnfNumVars :: !Int	1✔
76	-- ^ Number of variables
77	, cnfNumClauses :: !Int	1✔
78	-- ^ Number of clauses
79	, cnfClauses :: [SAT.PackedClause]	1✔
80	-- ^ Clauses
81	}
82	deriving (Eq, Ord, Show, Read)	×
83
84	instance FileFormat CNF where
85	parse s =	1✔
86	case BS.words l of	1✔
87	(["p","cnf", nvar, nclause]) ->
88	Right $	1✔
89	CNF	1✔
90	{ cnfNumVars = read $ BS.unpack nvar	1✔
91	, cnfNumClauses = read $ BS.unpack nclause	1✔
92	, cnfClauses = map parseClauseBS ls	1✔
93	}
94	_ ->
95	Left "cannot find cnf header"	×
96	where
97	l :: BS.ByteString
98	ls :: [BS.ByteString]
99	(l:ls) = filter (not . isCommentBS) (BS.lines s)	1✔
100
101	render cnf = header <> mconcat (map f (cnfClauses cnf))	1✔
102	where
103	header = mconcat	1✔
104	[ byteString "p cnf "	1✔
105	, intDec (cnfNumVars cnf), char7 ' '	1✔
106	, intDec (cnfNumClauses cnf), char7 '\n'	1✔
107	]
108	f c = mconcat [intDec lit <> char7 ' '\| lit <- SAT.unpackClause c] <> byteString "0\n"	1✔
109
110	readInts :: BS.ByteString -> [Int]
111	readInts s =	1✔
112	case BS.readInt (BS.dropWhile isSpace s) of	1✔
113	Just (0,_) -> []	1✔
114	Just (z,s') -> z : readInts s'	1✔
115	Nothing -> error "ToySolver.FileFormat.CNF.readInts: 0 is missing"	×
116
117	parseClauseBS :: BS.ByteString -> SAT.PackedClause
118	parseClauseBS = SAT.packClause . readInts	1✔
119
120	isCommentBS :: BS.ByteString -> Bool
121	isCommentBS s =	1✔
122	case BS.uncons s of	1✔
123	Just ('c',_) -> True	1✔
124	_ -> False	1✔
125
126	-- -------------------------------------------------------------------
127
128	-- \| WCNF format for representing partial weighted Max-SAT problems.
129	--
130	-- This format is used for for MAX-SAT evaluations.
131	--
132	-- References:
133	--
134	-- * <http://maxsat.ia.udl.cat/requirements/>
135	data WCNF
136	= WCNF
137	{ wcnfNumVars :: !Int	1✔
138	-- ^ Number of variables
139	, wcnfNumClauses :: !Int	1✔
140	-- ^ Number of (weighted) clauses
141	, wcnfTopCost :: !Weight	1✔
142	-- ^ Hard clauses have weight equal or greater than "top".
143	-- We assure that "top" is a weight always greater than the sum of the weights of violated soft clauses in the solution.
144	, wcnfClauses :: [WeightedClause]	1✔
145	-- ^ Weighted clauses
146	}
147	deriving (Eq, Ord, Show, Read)	×
148
149	-- \| Weighted clauses
150	type WeightedClause = (Weight, SAT.PackedClause)
151
152	-- \| Weigths must be greater than or equal to 1, and smaller than 2^63.
153	type Weight = Integer
154
155	-- \| Note that 'parse' also accepts new WCNF files and (unweighted) CNF files and converts them into 'WCNF'.
156	instance FileFormat WCNF where
157	parse = liftM f . parse	1✔
158	where
159	f (SomeWCNFNew x) = toOldWCNF x	1✔
160	f (SomeWCNFOld x) = x	1✔
161
162	render wcnf = header <> mconcat (map f (wcnfClauses wcnf))	1✔
163	where
164	header = mconcat	1✔
165	[ byteString "p wcnf "	1✔
166	, intDec (wcnfNumVars wcnf), char7 ' '	1✔
167	, intDec (wcnfNumClauses wcnf), char7 ' '	1✔
168	, integerDec (wcnfTopCost wcnf), char7 '\n'	1✔
169	]
170	f (w,c) = integerDec w <> mconcat [char7 ' ' <> intDec lit \| lit <- SAT.unpackClause c] <> byteString " 0\n"	1✔
171
172	parseWCNFLineBS :: BS.ByteString -> WeightedClause
173	parseWCNFLineBS s =	1✔
174	case BS.readInteger (BS.dropWhile isSpace s) of	1✔
175	Nothing -> error "ToySolver.FileFormat.CNF: no weight"	×
176	Just (w, s') -> seq w $ seq xs $ (w, xs)	1✔
177	where
178	xs = parseClauseBS s'	1✔
179
180	-- -------------------------------------------------------------------
181
182	-- \| New WCNF file format
183	--
184	-- This format is used for for MAX-SAT evaluations >=2020.
185	--
186	-- References:
187	--
188	-- * <https://maxsat-evaluations.github.io/2021/format.html>
189	newtype NewWCNF
190	= NewWCNF
191	{ nwcnfClauses :: [NewWeightedClause]	1✔
192	-- ^ Weighted clauses
193	}
194	deriving (Eq, Ord, Show, Read)	×
195
196	type NewWeightedClause = (Maybe Weight, SAT.PackedClause)
197
198	-- \| Note that 'parse' also accepts (old) WCNF files and (unweighted) CNF files and converts them into 'NewWCNF'.
199	instance FileFormat NewWCNF where
200	parse = liftM f . parse	1✔
201	where
202	f (SomeWCNFNew x) = x	1✔
203	f (SomeWCNFOld x) = toNewWCNF x	1✔
204
205	render nwcnf = mconcat (map f (nwcnfClauses nwcnf))	1✔
206	where
207	f (Nothing, c) = char7 'h' <> mconcat [char7 ' ' <> intDec lit \| lit <- SAT.unpackClause c] <> byteString " 0\n"	1✔
208	f (Just w, c) = integerDec w <> mconcat [char7 ' ' <> intDec lit \| lit <- SAT.unpackClause c] <> byteString " 0\n"	1✔
209
210	parseNewWCNFLineBS :: BS.ByteString -> NewWeightedClause
211	parseNewWCNFLineBS s =	1✔
212	case BS.uncons s' of	1✔
213	Nothing -> error "ToySolver.FileFormat.CNF: no weight"	×
214	Just ('h', s'') ->
215	let xs = parseClauseBS s''	1✔
216	in seq xs $ (Nothing, xs)	1✔
217	Just _ ->
218	case BS.readInteger s' of	1✔
219	Nothing -> error "ToySolver.FileFormat.CNF: no weight"	×
220	Just (w, s'') ->
221	let xs = parseClauseBS s''	1✔
222	in seq w $ seq xs $ (Just w, xs)	1✔
223	where
224	s' = BS.dropWhile isSpace s	1✔
225
226	-- -------------------------------------------------------------------
227
228	data SomeWCNF
229	= SomeWCNFOld WCNF
230	\| SomeWCNFNew NewWCNF
231	deriving (Eq, Ord, Show, Read)	×
232
233	toOldWCNF :: NewWCNF -> WCNF
234	toOldWCNF (NewWCNF cs)	1✔
235	= WCNF	1✔
236	{ wcnfNumVars = maximum (0 : [abs l \| (_, c) <- cs, l <- unpackClause c])	1✔
237	, wcnfNumClauses = length cs	1✔
238	, wcnfTopCost = top	1✔
239	, wcnfClauses = [(fromMaybe top w, c) \| (w, c) <- cs]	1✔
240	}
241	where
242	top = sum [w \| (Just w, _c) <- cs] + 1	1✔
243
244	toNewWCNF :: WCNF -> NewWCNF
245	toNewWCNF wcnf = NewWCNF [(if w >= wcnfTopCost wcnf then Nothing else Just w, c) \| (w, c) <- wcnfClauses wcnf]	1✔
246
247	instance FileFormat SomeWCNF where
248	parse s =	1✔
249	case filter (not . isCommentBS) (BS.lines s) of	1✔
250	[] -> Right $ SomeWCNFNew $ NewWCNF []	×
251	lls@(l : ls) ->
252	case BS.words l of	1✔
253	(["p","wcnf", nvar, nclause, top]) ->
254	Right $ SomeWCNFOld $	1✔
255	WCNF	1✔
256	{ wcnfNumVars = read $ BS.unpack nvar	1✔
257	, wcnfNumClauses = read $ BS.unpack nclause	1✔
258	, wcnfTopCost = read $ BS.unpack top	1✔
259	, wcnfClauses = map parseWCNFLineBS ls	1✔
260	}
261	(["p","wcnf", nvar, nclause]) ->
262	Right $ SomeWCNFOld $	×
263	WCNF	×
264	{ wcnfNumVars = read $ BS.unpack nvar	×
265	, wcnfNumClauses = read $ BS.unpack nclause	×
266	-- top must be greater than the sum of the weights of violated soft clauses.
267	, wcnfTopCost = fromInteger $ 2^(63::Int) - 1	×
268	, wcnfClauses = map parseWCNFLineBS ls	×
269	}
270	(["p","cnf", nvar, nclause]) ->
271	Right $ SomeWCNFOld $	1✔
272	WCNF	1✔
273	{ wcnfNumVars = read $ BS.unpack nvar	1✔
274	, wcnfNumClauses = read $ BS.unpack nclause	1✔
275	-- top must be greater than the sum of the weights of violated soft clauses.
276	, wcnfTopCost = fromInteger $ 2^(63::Int) - 1	1✔
277	, wcnfClauses = map ((\c -> seq c (1,c)) . parseClauseBS) ls	1✔
278	}
279	("h" : _) ->
280	Right $ SomeWCNFNew $ NewWCNF $ map parseNewWCNFLineBS lls	1✔
281	(s : _) \| Just _ <- BS.readInteger s ->	1✔
282	Right $ SomeWCNFNew $ NewWCNF $ map parseNewWCNFLineBS lls	1✔
283	_ ->
284	Left "cannot find wcnf/cnf header"	×
285
286	render (SomeWCNFOld wcnf) = render wcnf	×
287	render (SomeWCNFNew nwcnf) = render nwcnf	×
288
289	-- -------------------------------------------------------------------
290
291	-- \| Group oriented CNF Input Format
292	--
293	-- This format is used in Group oriented MUS track of the SAT Competition 2011.
294	--
295	-- References:
296	--
297	-- * <http://www.satcompetition.org/2011/rules.pdf>
298	data GCNF
299	= GCNF
300	{ gcnfNumVars :: !Int	1✔
301	-- ^ Nubmer of variables
302	, gcnfNumClauses :: !Int	1✔
303	-- ^ Number of clauses
304	, gcnfLastGroupIndex :: !GroupIndex	1✔
305	-- ^ The last index of a group in the file number of components contained in the file.
306	, gcnfClauses :: [GClause]	1✔
307	}
308	deriving (Eq, Ord, Show, Read)	×
309
310	-- \| Component number between 0 and `gcnfLastGroupIndex`
311	type GroupIndex = Int
312
313	-- \| Clause together with component number
314	type GClause = (GroupIndex, SAT.PackedClause)
315
316	instance FileFormat GCNF where
317	parse s =	1✔
318	case BS.words l of	1✔
319	(["p","gcnf", nbvar', nbclauses', lastGroupIndex']) ->
320	Right $	1✔
321	GCNF	1✔
322	{ gcnfNumVars = read $ BS.unpack nbvar'	1✔
323	, gcnfNumClauses = read $ BS.unpack nbclauses'	1✔
324	, gcnfLastGroupIndex = read $ BS.unpack lastGroupIndex'	1✔
325	, gcnfClauses = map parseGCNFLineBS ls	1✔
326	}
327	(["p","cnf", nbvar', nbclause']) ->
328	Right $	1✔
329	GCNF	1✔
330	{ gcnfNumVars = read $ BS.unpack nbvar'	1✔
331	, gcnfNumClauses = read $ BS.unpack nbclause'	1✔
332	, gcnfLastGroupIndex = read $ BS.unpack nbclause'	1✔
333	, gcnfClauses = zip [1..] $ map parseClauseBS ls	1✔
334	}
335	_ ->
336	Left "cannot find gcnf header"	×
337	where
338	l :: BS.ByteString
339	ls :: [BS.ByteString]
340	(l:ls) = filter (not . isCommentBS) (BS.lines s)	1✔
341
342	render gcnf = header <> mconcat (map f (gcnfClauses gcnf))	1✔
343	where
344	header = mconcat	1✔
345	[ byteString "p gcnf "	1✔
346	, intDec (gcnfNumVars gcnf), char7 ' '	1✔
347	, intDec (gcnfNumClauses gcnf), char7 ' '	1✔
348	, intDec (gcnfLastGroupIndex gcnf), char7 '\n'	1✔
349	]
350	f (idx,c) = char7 '{' <> intDec idx <> char7 '}' <>	1✔
351	mconcat [char7 ' ' <> intDec lit \| lit <- SAT.unpackClause c] <>	1✔
352	byteString " 0\n"	1✔
353
354	parseGCNFLineBS :: BS.ByteString -> GClause
355	parseGCNFLineBS s	1✔
356	\| Just ('{', s1) <- BS.uncons (BS.dropWhile isSpace s)	1✔
357	, Just (!idx,s2) <- BS.readInt s1	1✔
358	, Just ('}', s3) <- BS.uncons s2 =	1✔
359	let ys = parseClauseBS s3	1✔
360	in seq ys $ (idx, ys)	1✔
361	\| otherwise = error "ToySolver.FileFormat.CNF: parse error"	×
362
363	-- -------------------------------------------------------------------
364
365	{-
366	http://www.qbflib.org/qdimacs.html
367
368	<input> ::= <preamble> <prefix> <matrix> EOF
369
370	<preamble> ::= [<comment_lines>] <problem_line>
371	<comment_lines> ::= <comment_line> <comment_lines> \| <comment_line>
372	<comment_line> ::= c <text> EOL
373	<problem_line> ::= p cnf <pnum> <pnum> EOL
374
375	<prefix> ::= [<quant_sets>]
376	<quant_sets> ::= <quant_set> <quant_sets> \| <quant_set>
377	<quant_set> ::= <quantifier> <atom_set> 0 EOL
378	<quantifier> ::= e \| a
379	<atom_set> ::= <pnum> <atom_set> \| <pnum>
380
381	<matrix> ::= <clause_list>
382	<clause_list> ::= <clause> <clause_list> \| <clause>
383	<clause> ::= <literal> <clause> \| <literal> 0 EOL
384	<literal> ::= <num>
385
386	<text> ::= {A sequence of non-special ASCII characters}
387	<num> ::= {A 32-bit signed integer different from 0}
388	<pnum> ::= {A 32-bit signed integer greater than 0}
389	-}
390
391	-- \| QDIMACS format
392	--
393	-- Quantified boolean expression in prenex normal form,
394	-- consisting of a sequence of quantifiers ('qdimacsPrefix') and
395	-- a quantifier-free CNF part ('qdimacsMatrix').
396	--
397	-- References:
398	--
399	-- * QDIMACS standard Ver. 1.1
400	-- <http://www.qbflib.org/qdimacs.html>
401	data QDimacs
402	= QDimacs
403	{ qdimacsNumVars :: !Int	1✔
404	-- ^ Number of variables
405	, qdimacsNumClauses :: !Int	1✔
406	-- ^ Number of clauses
407	, qdimacsPrefix :: [QuantSet]	1✔
408	-- ^ Sequence of quantifiers
409	, qdimacsMatrix :: [SAT.PackedClause]	1✔
410	-- ^ Clauses
411	}
412	deriving (Eq, Ord, Show, Read)	×
413
414	-- \| Quantifier
415	data Quantifier
416	= E -- ^ existential quantifier (∃)
417	\| A -- ^ universal quantifier (∀)
418	deriving (Eq, Ord, Show, Read, Enum, Bounded)	×
419
420	-- \| Quantified set of variables
421	type QuantSet = (Quantifier, [Atom])
422
423	-- \| Synonym of 'SAT.Var'
424	type Atom = SAT.Var
425
426	instance FileFormat QDimacs where
427	parse = f . BS.lines	1✔
428	where
429	f [] = Left "ToySolver.FileFormat.CNF.parse: premature end of file"	×
430	f (l : ls) =
431	case BS.uncons l of	1✔
432	Nothing -> Left "ToySolver.FileFormat.CNF.parse: no problem line"	×
433	Just ('c', _) -> f ls	×
434	Just ('p', s) ->
435	case BS.words s of	1✔
436	["cnf", numVars', numClauses'] ->
437	case parsePrefix ls of	1✔
438	(prefix', ls') -> Right $	1✔
439	QDimacs	1✔
440	{ qdimacsNumVars = read $ BS.unpack numVars'	1✔
441	, qdimacsNumClauses = read $ BS.unpack numClauses'	1✔
442	, qdimacsPrefix = prefix'	1✔
443	, qdimacsMatrix = map parseClauseBS ls'	1✔
444	}
445	_ -> Left "ToySolver.FileFormat.CNF.parse: invalid problem line"	×
446	Just (c, _) -> Left ("ToySolver.FileFormat.CNF.parse: invalid prefix " ++ show c)	×
447
448	render qdimacs = problem_line <> prefix' <> mconcat (map f (qdimacsMatrix qdimacs))	1✔
449	where
450	problem_line = mconcat	1✔
451	[ byteString "p cnf "	1✔
452	, intDec (qdimacsNumVars qdimacs), char7 ' '	1✔
453	, intDec (qdimacsNumClauses qdimacs), char7 '\n'	1✔
454	]
455	prefix' = mconcat	1✔
456	[ char7 (if q == E then 'e' else 'a') <> mconcat [char7 ' ' <> intDec atom \| atom <- atoms] <> byteString " 0\n"	1✔
457	\| (q, atoms) <- qdimacsPrefix qdimacs	1✔
458	]
459	f c = mconcat [intDec lit <> char7 ' '\| lit <- SAT.unpackClause c] <> byteString "0\n"	1✔
460
461	parsePrefix :: [BS.ByteString] -> ([QuantSet], [BS.ByteString])
462	parsePrefix = go []	1✔
463	where
464	go result [] = (reverse result, [])	1✔
465	go result lls@(l : ls) =
466	case BS.uncons l of	1✔
467	Just (c,s)
468	\| c=='a' \|\| c=='e' ->	1✔
469	let atoms = readInts s	1✔
470	q = if c=='a' then A else E	1✔
471	in seq q $ deepseq atoms $ go ((q, atoms) : result) ls	1✔
472	\| otherwise ->	×
473	(reverse result, lls)	1✔
474	_ -> error "ToySolver.FileFormat.CNF.parseProblem: invalid line"	×
475
476	-- -------------------------------------------------------------------

msakai / toysolver / 563

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous