| Copyright | (c) Dominik Luecke, Uni Bremen 2007 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | luecke@informatik.uni-bremen.de |
| Stability | experimental |
| Portability | portable |
| Safe Haskell | None |
Propositional.Conversions
Description
Helper functions for printing of Theories in DIMACS-CNF Format
- showDIMACSProblem :: String -> Sign -> [Named FORMULA] -> Maybe (Named FORMULA) -> IO String
- goalDIMACSProblem :: String -> PropProverState -> Named FORMULA -> [String] -> IO String
- createSignMap :: Sign -> Integer -> Map Token Integer -> Map Token Integer
- mapClause :: FORMULA -> Map Token Integer -> String
Documentation
Arguments
| :: String | name of the theory |
| -> Sign | Signature |
| -> [Named FORMULA] | Axioms |
| -> Maybe (Named FORMULA) | Conjectures |
| -> IO String | Output |
Translation of a Propositional Formula to a String in DIMACS Format
Arguments
| :: String | name of the theory |
| -> PropProverState | initial Prover state |
| -> Named FORMULA | goal to prove |
| -> [String] | Options (ignored) |
| -> IO String |
make a DIMACS Problem for SAT-Solvers