Documentation.SBV.Examples.Queries.CaseSplit

A couple of demonstrations for the caseSplit function.

Documentation

csDemo1 :: IO (String, Float)

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)

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)