sbv-11.0: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainer[email protected]
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