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

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.Queries.UnsatCore

Description

Demonstrates extraction of unsat-cores via queries.

Synopsis

- p :: Symbolic (Maybe [String])
- ucCore :: IO ()

# Documentation

p :: Symbolic (Maybe [String]) Source #

A simple goal with three constraints, two of which are conflicting with each other. The third is irrelevant, in the sense that it does not contribute to the fact that the goal is unsatisfiable.

ucCore :: IO () Source #

Extract the unsat-core of `p`. We have:

    >>> ucCore
    Unsat core is: ["less than 5","more than 10"]

Demonstrating that the constraint `a .> b` is not needed for unsatisfiablity in this case.