{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Misc.SoftConstrain where
import Data.SBV
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"
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