Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Read/Write a CNF file only with ghc standard libraries
- fromFile :: FilePath -> IO (Maybe ((Int, Int), [[Int]]))
- clauseListFromFile :: FilePath -> IO [[Int]]
- fromMinisatOutput :: FilePath -> IO (Maybe ((Int, Int), [Int]))
- clauseListFromMinisatOutput :: FilePath -> IO [Int]
- toFile :: FilePath -> [[Int]] -> IO ()
- toCNFString :: [[Int]] -> String
- asCNFString :: BoolForm -> String
- asCNFString_ :: BoolForm -> String
- module SAT.Mios.Util.BoolExp
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
toCNFString :: [[Int]] -> String Source #
Convert [Clause] to String, where Clause is [Int]
>>>
toCNFString []
"p cnf 0 0\n"
>>>
toCNFString [[-1, 2], [-3, -4]]
"p cnf 4 2\n-1 2 0\n-3 -4 0\n"
>>>
toCNFString [[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"
asCNFString :: BoolForm -> String Source #
String from BoolFrom
asCNFString_ :: BoolForm -> String Source #
String from BoolFrom
Bool Operation
module SAT.Mios.Util.BoolExp