| Copyright | (c) Jonatzhan von Schroeder DFKI GmbH 2010 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Christian.Maeder@dfki.de |
| Stability | provisional |
| Portability | needs POSIX |
| Safe Haskell | None |
QBF.ProverState
Contents
Description
Data structures and initialising functions for Prover state and configurations.
Synopsis
- data QBFProverState = QBFProverState {}
- qbfProverState :: Sign -> [Named FORMULA] -> [FreeDefMorphism FORMULA Morphism] -> QBFProverState
- transSenName :: String -> String
- insertSentence :: QBFProverState -> Named FORMULA -> QBFProverState
- showQDIMACSProblem :: String -> QBFProverState -> Named FORMULA -> [String] -> IO String
Data structures
data QBFProverState Source #
Constructors
| QBFProverState | |
Fields
| |
Instances
| Show QBFProverState Source # | |
Defined in QBF.ProverState Methods showsPrec :: Int -> QBFProverState -> ShowS show :: QBFProverState -> String showList :: [QBFProverState] -> ShowS | |
Arguments
| :: Sign | QBF signature |
| -> [Named FORMULA] | list of named QBF formulas |
| -> [FreeDefMorphism FORMULA Morphism] | freeness constraints |
| -> QBFProverState |
Creates an initial qbf prover state
transSenName :: String -> String Source #
Arguments
| :: QBFProverState | prover state containing the axioms |
| -> Named FORMULA | formula to add |
| -> QBFProverState |
Inserts a named SoftFOL term into SoftFOL prover state.
Arguments
| :: String | theory name |
| -> QBFProverState | prover state |
| -> Named FORMULA | goal |
| -> [String] | extra options |
| -> IO String | formatted output of the goal |
Pretty printing QBF goal in QDIMACS format.