% Boolean Constraints for CFLP
% Sebastian Fischer (sebf@informatik.unikiel.de)
This module provides boolean constraints for constraint
functionallogic programming.
>
>
> module CFLP.Constraints.Boolean (
>
> Boolean, yes, no, neg, (.&&.), (.||.),
>
> BooleanSolver(..), SatCtx, Sat, satSolving,
>
> ifThen, ifThenElse, booleanToBool
>
> ) where
>
> import Control.Monad
>
> import CFLP
> import CFLP.Control.Strategy
>
> import CFLP.Control.Monad.Update
>
> import CFLP.Data.Types
> ( HeadNormalForm(..), Nondet(..), Context(..), label, joinNondet )
> import CFLP.Data.Primitive
>
> import CFLP.Types.Bool
>
> import Data.Boolean.SatSolver
Generic Creation of Boolean Formulas
====================================
We make the type of boolean formulas an instance of `ApplyCons` and
`Generic` in order to be able to define boolean formulas in CFLP
programs.
> instance ApplyCons Boolean
> where
> type Result Boolean = Boolean
> applyCons = const
>
> instance Generic Boolean
> where
> constr = cons "BVAR" Var dVar
> ! cons "TRUE" Yes dYes
> ! cons "FALSE" No dNo
> ! cons "NOT" Not dNot
> ! cons "AND" (:&&:) dAnd
> ! cons "OR" (:||:) dOr
>
> dVar, dYes, dNo, dNot, dAnd, dOr :: Decons Boolean
>
> dVar c (Var n) = Just (c [generic n])
> dVar _ _ = Nothing
>
> dYes c Yes = Just (c [])
> dYes _ _ = Nothing
>
> dNo c No = Just (c [])
> dNo _ _ = Nothing
>
> dNot c (Not x) = Just (c [generic x])
> dNot _ _ = Nothing
>
> dAnd c (x:&&:y) = Just (c [generic x, generic y])
> dAnd _ _ = Nothing
>
> dOr c (x:||:y) = Just (c [generic x, generic y])
> dOr _ _ = Nothing
We define functions for constructing boolean formulas, but none for
pattern matching.
> infixr 3 .&&.
> infixr 2 .||.
>
> var :: Monad m => Nondet c m Int -> Nondet c m Boolean
> yes, no :: Monad m => Nondet c m Boolean
> neg :: Monad m => Nondet c m Boolean -> Nondet c m Boolean
> (.&&.), (.||.) :: Monad m => Nondet c m Boolean -> Nondet c m Boolean
> -> Nondet c m Boolean
>
> var :! yes :! no :! neg :! (.&&.) :! (.||.) :! () = constructors
Extending Computations with SAT Solving
==============================================
An evaluation context that can satisfy boolean formulas is an instance
of the following type class.
> class BooleanSolver c
> where
> lookupBoolean :: Int -> c -> Maybe Bool
> assertBoolean :: MonadPlus m => c -> Boolean -> c -> m c
A transformed boolean solver is still a boolean solver.
> instance (BooleanSolver c, Transformer t) => BooleanSolver (t c)
> where
> lookupBoolean n = lookupBoolean n . project
> assertBoolean _ = inside . assertBoolean undefined
We define a context transformer that adds SATsolving capabilities to
an arbitrary context.
> data SatCtx c = SatCtx SatSolver c
>
> instance Transformer SatCtx
> where
> project (SatCtx _ c) = c
> replace (SatCtx s _) = SatCtx s
A context of type `SatCtx c` is always a boolean solver.
> instance BooleanSolver (SatCtx c)
> where
> lookupBoolean n (SatCtx s _) = lookupVar n s
> assertBoolean _ b (SatCtx s c) = liftM (flip SatCtx c) (assertTrue b s)
It is also solvable.
> instance Solvable c => Solvable (SatCtx c)
> where
> solvable (SatCtx s c) = isSolvable s && solvable c
> bindVars (SatCtx s c) = liftM2 SatCtx (solve s) (bindVars c)
We define a strategy transformer to create SAT solving strategies.
> newtype Sat s a = Sat { fromSat :: s a }
> deriving (Monad, MonadPlus, Enumerable)
>
> type instance Ctx (Sat s) = SatCtx (Ctx s)
> type instance Res (Sat s) = Sat (Res s)
>
> instance BooleanSolver c => StrategyT c Sat
> where
> liftStrategy _ = Sat
> baseStrategy _ = fromSat
>
> alterNarrowed c n b = maybe b (const (return True)) (lookupBoolean n c)
The context of a sat solving strategy is initialized with a new sat
solver.
> satSolving :: Monad s => s c -> Sat s (SatCtx c)
> satSolving = Sat . liftM (SatCtx newSatSolver)
Narrowing and Guards
====================
We provide an instance of `Narrow` for booleans in order to be able to
create logic boolean variables. We can create such variables if the
evaluation context is a boolean solver.
> instance BooleanSolver c => Narrow c Boolean
> where
> narrow (Context c) u =
> let v = label u
> in maybe (var (nondet v))
> (\b -> if b then yes else no)
> (lookupBoolean v c)
The function `ifThen` implements a guard for boolean formulas.
> ifThen :: (CFLP s, BooleanSolver (Ctx s))
> => Data s Boolean -> Data s a -> Context (Ctx s) -> Data s a
> ifThen x y = withPrim x $ \b c ->
> joinNondet (do update (assertBoolean c b); return y)
We also provide `ifThenElse`.
> ifThenElse :: (CFLP s, BooleanSolver (Ctx s))
> => Data s Boolean -> Data s a -> Data s a
> -> Context (Ctx s) -> Data s a
> ifThenElse x y z = withPrim x $ \b c ->
> joinNondet ((do update (assertBoolean c b); return y)
> `mplus`
> (do update (assertBoolean c (Not b)); return z))
Boolean constraints can be converted to boolean data terms.
> booleanToBool :: (CFLP s, BooleanSolver (Ctx s))
> => Data s Boolean -> Context (Ctx s) -> Data s Bool
> booleanToBool b = withHNF b $ \b c@(Context cs) ->
> case b of
> FreeVar u x -> Typed $
> maybe (return (FreeVar u (untyped (ifThenElse (Typed x) true false c))))
> (untyped . nondet)
> (lookupBoolean (label u) cs)
> Delayed check resume -> Typed $ do
> narrowed <- check c
> if narrowed
> then untyped (booleanToBool (Typed (resume c)) c)
> else return (Delayed check
> (\c -> untyped (booleanToBool (Typed (resume c)) c)))
> _ -> ifThenElse (Typed (return b)) true false c