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

Copyright(c) Levent Erkok
Safe HaskellNone



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.



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.