Main part of the program + DIMACS CNF parsing

Civilisation.hs

@@ -0,0 +1,43 @@
+{- |
+Module      :  Civilisation
+Description :  
+Copyright   :  (c) Dimitri Lozeve
+License     :  BSD3
+
+Maintainer  :  Dimitri Lozeve <dimitri.lozeve@gmail.com>
+Stability   :  unstable
+Portability :  portable
+
+-}
+
+import Data.Maybe
+
+import Sat
+
+
+-- Main entry point of the program
+main :: IO ()
+main = do
+  text <- readFile "test.cnf"
+  let f = parseDIMACS text in
+    case solveDPLL (f, []) of
+      UNSAT -> putStrLn "UNSAT"
+      SAT a -> putStrLn $ "SAT " ++ show a
+
+-- Parses a formula in the DIMACS CNF format.
+parseDIMACS :: String -> CNF
+parseDIMACS = mapMaybe parseClause . lines
+
+-- Parses a clause (a single line in the DIMACS file).
+parseClause :: String -> Maybe Clause
+parseClause "" = Nothing
+parseClause ('c':_) = Nothing
+parseClause ('p':_) = Nothing
+parseClause ('%':_) = Nothing
+parseClause ('0':_) = Nothing
+parseClause s = (Just . map (litFromInt . read) . init . words) s
+
+-- Interprets an Int, such as (-5), as a Lit, such as (Neg 5).
+litFromInt :: Int -> Lit
+litFromInt n | n < 0 = Neg (-n)
+             | otherwise = Pos n