Data.SBV.Examples.Queries.CaseSplit

A couple of demonstrations for the caseSplit tactic.

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)