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

Copyright(c) Levent Erkok
Safe HaskellNone



A couple of demonstrations for the caseSplit tactic.



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)