sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.DeltaSat.DeltaSat

Description

The encoding of the Flyspec example from the dReal web page

Synopsis

- flyspeck :: IO SatResult

# Documentation

flyspeck :: IO SatResult Source #

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

    >>> flyspeck
    Unsatisfiable