Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
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.