Hets - the Heterogeneous Tool Set
Copyright(c) Dominik Luecke Uni Bremen 2007
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerluecke@informatik.uni-bremen.de
Stabilityexperimental
Portabilityportable
Safe HaskellNone

Propositional.ProveMinisat

Description

This is the connection of the SAT-Solver minisat to Hets

Synopsis

Documentation

data MiniSatVer Source #

Constructors

Minisat 
Minisat2 

Instances

Instances details
Show MiniSatVer Source # 
Instance details

Defined in Propositional.ProveMinisat

Methods

showsPrec :: Int -> MiniSatVer -> ShowS

show :: MiniSatVer -> String

showList :: [MiniSatVer] -> ShowS

minisatProver :: MiniSatVer -> Prover Sign FORMULA Morphism PropSL ProofTree Source #

The Prover implementation.

Implemented are: a prover GUI, and both commandline prover interfaces.

minisatConsChecker :: MiniSatVer -> ConsChecker Sign FORMULA PropSL Morphism ProofTree Source #

The Consistency Cheker.