Data.SBV.Examples.Misc.UnsatCore

Demonstrates extraction of unsat-cores.

Documentation

p :: Goal

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
Unsatisfiable. Unsat core:
  less than 5
  more than 10
=====================================
Unsat core is: ["less than 5","more than 10"]

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