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

Copyright(c) Levent Erkok
Safe HaskellNone



A couple of demonstrations for the caseSplit function.



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

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