Documentation.SBV.Examples.Queries.UnsatCore

Demonstrates extraction of unsat-cores via queries.

Documentation

p :: Symbolic (Maybe [String])

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 ()

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.