mios-1.6.2: A Minisat-based CDCL SAT solver in Haskell

Safe HaskellSafe
LanguageHaskell2010

SAT.Mios.Util.DIMACS

Contents

Description

Read/Write a CNF file only with ghc standard libraries

Synopsis

Input

fromFile :: FilePath -> IO (Maybe ((Int, Int), [[Int]])) Source #

read a CNF file and return: ((numbefOfVariables, numberOfClauses), [Literal])

>>> fromFile "acnf"
((3, 4), [[1, 2], [-2, 3], [-1, 2, -3], [3]]

clauseListFromFile :: FilePath -> IO [[Int]] Source #

return clauses as [[Int]] from file

>>> clauseListFromFile "a.cnf"
[[1, 2], [-2, 3], [-1, 2, -3], [3]]

fromMinisatOutput :: FilePath -> IO (Maybe ((Int, Int), [Int])) Source #

read a minisat output: ((numbefOfVariables, 0), [Literal])

>>> fromFile "result"
((3, 0), [1, -2, 3])

clauseListFromMinisatOutput :: FilePath -> IO [Int] Source #

return clauses as [[Int]] from file

>>> clauseListFromMinisatOutput "result"
[1,-2,3]

Output

toFile :: FilePath -> [[Int]] -> IO () Source #

Write the DIMACS to file f, using toDIMACSString

toDIMACSString :: [[Int]] -> String Source #

Convert [Clause] to String, where Clause is [Int]

>>> toDIMACSString []
"p cnf 0 0\n"
>>> toDIMACSString [[-1, 2], [-3, -4]]
"p cnf 4 2\n-1 2 0\n-3 -4 0\n"
>>> toDIMACSString [[1], [-2], [-3, -4], [1,2,3,4]]
"p cnf 4 4\n1 0\n-2 0\n-3 -4 0\n1 2 3 4 0\n"

asDIMACSString :: BoolForm -> String Source #

String from BoolFrom

asDIMACSString_ :: BoolForm -> String Source #

String from BoolFrom

Bool Operation