Documentation.SBV.Examples.Misc.SoftConstrain

Demonstrates soft-constraints, i.e., those that the solver is free to leave unsatisfied. Solvers will try to satisfy this constraint, unless it is impossible to do so to get a model. Can be good in modeling default values, for instance.

Documentation

example :: IO SatResult

Create two strings, requiring one to be a particular value, constraining the other to be different than another constant string. But also add soft constraints to indicate our preferences for each of these variables. We get:

>>> example
Satisfiable. Model:
  x = "x-must-really-be-hello" :: String
  y =        "default-y-value" :: String

Note how the value of x is constrained properly and thus the default value doesn't kick in, but y takes the default value since it is acceptable by all the other hard constraints.