1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
------------------------------------------------------------------------------
--- This module defines a simple parser for the output of a DIMACS solver.
---
--- @author Sven Hueser
--- @version July 2021
------------------------------------------------------------------------------

module Dimacs.Parser where

import Prelude hiding ( some, (<*), (*>), (<$>) )

import DetParser
import Dimacs.Types
import Dimacs.Scanner


parse :: String -> Either ParseError [Boolean]
parse s = case parseDimacs $ scan s of
  Left e        -> Left e
  Right ([], x) -> Right x
  Right _       -> Left "incomplete parse"

parseDimacs :: Parser Token [Boolean]
parseDimacs [] = eof []
parseDimacs (t:ts) = case t of
  KW_sat   -> some parseVar <* terminal EOF $ ts
  KW_unsat -> terminal EOF *> yield [] $ ts
  _        -> unexpected t ts

parseVar :: Parser Token Boolean
parseVar [] = eof []
parseVar (t:ts) = case t of
  VarNot   -> Not <$> parseVar $ ts
  VarNum i -> yield (Var i) ts
  _        -> unexpected t ts