Copyright	© Edward Kmett 2010-2014 Johan Kiviniemi 2013
License	BSD3
Maintainer	Edward Kmett <[email protected]>
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Ersatz.Solver.DepQBF

Description

DepQBF is a solver capable of solving quantified boolean formulae (QBF).

Synopsis

depqbf :: MonadIO m => Solver QSAT m
depqbfPath :: MonadIO m => FilePath -> Solver QSAT m
depqbfPathArgs :: MonadIO m => FilePath -> [String] -> Solver QSAT m

Documentation

depqbf :: MonadIO m => Solver QSAT m Source #

This is a Solver for QSAT problems that runs the depqbf solver using the current PATH, it tries to run an executable named depqbf.

depqbfPath :: MonadIO m => FilePath -> Solver QSAT m Source #

This is a Solver for QSAT problems that lets you specify the path to the depqbf executable. This passes different arguments to depqbf depending on its version:

If using version 6.03 or later, this passes ["--qdo", "--no-dynamic-nenofex"].
Otherwise, this passes ["--qdo"].

depqbfPathArgs :: MonadIO m => FilePath -> [String] -> Solver QSAT m Source #

This is a Solver for QSAT problems that lets you specify the path to the depqbf executable as well as a list of command line arguments. They will appear after the problem file name.