    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Misc.SoftConstrain
    -- Copyright : (c) 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.
    -----------------------------------------------------------------------------

    {-# LANGUAGE OverloadedStrings #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Misc.SoftConstrain where

    import Data.SBV

    -- | 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.
    example :: IO SatResult
    example :: IO SatResult
    example = SymbolicT IO SBool -> IO SatResult
    forall a. Provable a => a -> IO SatResult
    sat (SymbolicT IO SBool -> IO SatResult)
    -> SymbolicT IO SBool -> IO SatResult
    forall a b. (a -> b) -> a -> b
    $ do SString
    x <- String -> Symbolic SString
    sString "x"
                       SString
    y <- String -> Symbolic SString
    sString "y"

                       SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SString
    x SString -> SString -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== "x-must-really-be-hello"
                       SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SString
    y SString -> SString -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= "y-can-be-anything-but-hello"

                       -- Now add soft-constraints to indicate our preference
                       -- for what these variables should be:
                       SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    softConstrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SString
    x SString -> SString -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== "default-x-value"
                       SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    softConstrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SString
    y SString -> SString -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== "default-y-value"

                       SBool -> SymbolicT IO SBool
    forall (m :: * -> *) a. Monad m => a -> m a
    return SBool
    sTrue