Documentation

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)

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)