-----------------------------------------------------------------------------
-- |
-- 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 String
"x"
                   SString
y <- String -> Symbolic SString
sString String
"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
.== SString
"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
./= SString
"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
.== SString
"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
.== SString
"default-y-value"

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