Hets - the Heterogeneous Tool Set

Copyright(c) Jonatzhan von Schroeder DFKI GmbH 2010
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityneeds POSIX
Safe HaskellNone

QBF.ProverState

Contents

Description

Data structures and initialising functions for Prover state and configurations.

Synopsis

Data structures

qbfProverState Source #

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 #

insertSentence Source #

Arguments

:: QBFProverState

prover state containing the axioms

-> Named FORMULA

formula to add

-> QBFProverState 

Inserts a named SoftFOL term into SoftFOL prover state.

showQDIMACSProblem Source #

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.