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

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Documentation.SBV.Examples.Misc.SoftConstrain

Description

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.

Synopsis

- example :: IO SatResult

# Documentation

example :: IO SatResult Source #

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.