sbv-8.4: 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.Queries.CaseSplit

Description

A couple of demonstrations for the caseSplit function.

Synopsis

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)