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

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

Documentation.SBV.Examples.Queries.CaseSplit

Description

A couple of demonstrations for the `caseSplit` function.

Synopsis

- csDemo1 :: IO (String, Float)
- csDemo2 :: IO (String, Integer)

# Documentation

csDemo1 :: IO (String, Float) Source #

A simple floating-point problem, but we do the sat-analysis via a case-split. Due to the nature of floating-point numbers, a case-split on the characteristics of the number (such as NaN, negative-zero, etc. is most suitable.)

We have:

    >>> csDemo1
    Case fpIsNegativeZero: Starting
    Case fpIsNegativeZero: Unsatisfiable
    Case fpIsPositiveZero: Starting
    Case fpIsPositiveZero: Unsatisfiable
    Case fpIsNormal: Starting
    Case fpIsNormal: Unsatisfiable
    Case fpIsSubnormal: Starting
    Case fpIsSubnormal: Unsatisfiable
    Case fpIsPoint: Starting
    Case fpIsPoint: Unsatisfiable
    Case fpIsNaN: Starting
    Case fpIsNaN: Satisfiable
    ("fpIsNaN",NaN)

csDemo2 :: IO (String, Integer) Source #

Demonstrates the "coverage" case.

We have:

    >>> csDemo2
    Case negative: Starting
    Case negative: Unsatisfiable
    Case less than 8: Starting
    Case less than 8: Unsatisfiable
    Case Coverage: Starting
    Case Coverage: Satisfiable
    ("Coverage",10)