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

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.Queries.UnsatCore

Description

Demonstrates extraction of unsat-cores via queries.

Synopsis

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.