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

Documentation.SBV.Examples.Misc.SoftConstrain

Description

Author : Levent Erkok License : BSD3 Maintainer: erkokl@gmail.com Stability : experimental

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

# Documentation

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.