sbv-8.10: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.DeltaSat.DeltaSat

Description

The encoding of the Flyspec example from the dReal web page

Synopsis

Documentation

flyspeck :: IO SatResult Source #

Encode the delta-sat problem as given in http://dreal.github.io/ We have:

>>> flyspeck
Unsatisfiable