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

Show MiniSatVer Source # 

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.