| 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.
- 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
Constructors
| QBFProverState | |
Fields
| |
Instances
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
Arguments
| :: QBFProverState | prover state containing the axioms |
| -> Named FORMULA | formula to add |
| -> QBFProverState |
Inserts a named SoftFOL term into SoftFOL prover state.