Permalink
Browse files

Integrated Boolean Constraint Solving.

added class Binding and function narrowVar.

optional result for binding function.

added Solver class and branchOn function.

lifting for Solver.

lifting for Binding.

class context for binding function.

added module for boolean constraints.

added context argument to class Narrow.

extended boolean constraint module.

guards and ifThenElse in boolean constraint module.

added first test for boolean constraint solver.

it fails because constraints are not solved after computation.

hlint suggestions. test passes after fixing sat solver package.

more tests for boolean constraints.

added test for unsolved boolean store and Solvable class.

return context from normal form functions and use it in evaluator.

test with unsolvable constraint after backtracking now succeeds.

constraint solving for partial normal forms.

reimplemented booleanToBool.

Retain variables and delayed computations.

simpler formula for backtracking test.
  • Loading branch information...
sebfisch committed Jan 28, 2009
1 parent 1246f8a commit aa955c505d3efb3f908350b7ad20239c540bb45b
View
@@ -8,9 +8,10 @@ package.
>
> import CFLP.Tests.CallTimeChoice as CTC
> import CFLP.Tests.HigherOrder as HO
+> import CFLP.Tests.Boolean as B
>
> main :: IO ()
> main = do
-> runTestTT $ test [CTC.tests,HO.tests]
+> runTestTT $ test [CTC.tests,HO.tests,B.tests]
> return ()
View
@@ -1,5 +1,5 @@
Name: cflp
-Version: 2009.1.28
+Version: 2009.1.29
Cabal-Version: >= 1.6
Synopsis: Constraint Functional-Logic Programming in Haskell
Description: This package provides combinators for constraint
@@ -23,16 +23,19 @@ Extra-Source-Files: README, INSTALL, Makefile, configure, Test.lhs
Library
Build-Depends: base >= 4, mtl, syb, containers,
control-monad-omega, logict, level-monad, stream-monad,
+ incremental-sat-solver,
random, MonadRandom,
value-supply,
HUnit
Exposed-Modules: CFLP
+ CFLP.Constraints.Boolean
CFLP.Strategies
CFLP.Strategies.CallTimeChoice
CFLP.Strategies.DepthCounter
CFLP.Strategies.DepthLimit
CFLP.Strategies.Random
CFLP.Tests
+ CFLP.Tests.Boolean
CFLP.Tests.CallTimeChoice
CFLP.Tests.HigherOrder
CFLP.Types.Bool
View
@@ -15,7 +15,7 @@ functional-logic programming in Haskell.
>
> module CFLP (
>
-> CFLP, Enumerable(..), Ctx, Data, Computation,
+> CFLP, Enumerable(..), Ctx, Data,
>
> eval, evalPartial, evalPrint,
>
@@ -38,6 +38,7 @@ The type class `CFLP` amalgamates all class constraints on constraint
functional-logic computations.
> class (Strategy (Ctx s) s, MonadPlus s
+> , Solvable (Ctx s)
> , MonadUpdate (Ctx s) s
> , Update (Ctx s) s s
> , Update (Ctx s) s (Res s)
@@ -50,13 +51,10 @@ functional-logic computations.
>
> instance (MonadPlus m, Enumerable m) => CFLP (Monadic (UpdateT () m))
-We define a shortcut for types of constraint functional-logic data and
-computations that can be parameterized by an arbitrary strategy.
+We define a shortcut for types of constraint functional-logic data
+that can be parameterized by an arbitrary strategy.
> type Data s a = Nondet (Ctx s) s a
->
-> type Computation a
-> = forall s . CFLP s => Context (Ctx s) -> ID -> Data s a
We provide
@@ -70,12 +68,15 @@ We provide
solutions of a constraint functional-logic computation.
> eval, evalPartial
-> :: (Monad s, CFLP s, Generic a) => [s (Ctx s)] -> Computation a -> IO [a]
+> :: (Monad s, CFLP s, Generic a)
+> => [s (Ctx s)]
+> -> (Context (Ctx s) -> ID -> Data s a)
+> -> IO [a]
> eval s = liftM (liftM primitive) . evaluate s groundNormalForm
> evalPartial s = liftM (liftM primitive) . evaluate s partialNormalForm
>
> evalPrint :: (Monad s, CFLP s, Generic a)
-> => [s (Ctx s)] -> Computation a -> IO ()
+> => [s (Ctx s)] -> (Context (Ctx s) -> ID -> Data s a) -> IO ()
> evalPrint s op = evaluate s partialNormalForm op >>= printSols
>
> printSols :: Show a => [a] -> IO ()
@@ -95,10 +96,14 @@ constraint functional-logic computation according to a given strategy.
> evaluate :: CFLP s
> => [s (Ctx s)]
-> -> (s (Ctx s) -> Nondet (Ctx s) s a -> Res s b)
-> -> Computation a
+> -> (s (Ctx s) -> Nondet (Ctx s) s a -> Res s (b, Ctx s))
+> -> (Context (Ctx s) -> ID -> Data s a)
> -> IO [b]
> evaluate s evalNondet op = do
> i <- initID
-> return $ concatMap enumeration $
-> map (\c -> evalNondet c (Typed (c >>= untyped . flip op i . Context))) s
+> return $ concatMap enumeration $ map (run i) s
+> where
+> run i c = do
+> (res,ctx) <- evalNondet c (Typed (c >>= untyped . flip op i . Context))
+> guard (solvable ctx)
+> return res
@@ -0,0 +1,212 @@
+% Boolean Constraints for CFLP
+% Sebastian Fischer (sebf@informatik.uni-kiel.de)
+
+This module provides boolean constraints for constraint
+functional-logic programming.
+
+> {-# LANGUAGE
+> GeneralizedNewtypeDeriving,
+> NoMonomorphismRestriction,
+> MultiParamTypeClasses,
+> OverlappingInstances,
+> FlexibleInstances,
+> FlexibleContexts,
+> NoMonoPatBinds,
+> TypeFamilies
+> #-}
+>
+> 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 SAT-solving 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` -- don't need choice constraints here!
+> (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
+
@@ -19,7 +19,9 @@ transformers.
>
> module CFLP.Control.Strategy (
>
-> Enumerable(..), Ctx, Res, Strategy(..), Transformer(..), StrategyT(..),
+> Enumerable(..), Solvable(..), Ctx, Res,
+>
+> Strategy(..), Transformer(..), StrategyT(..),
>
> Monadic(..), inside
>
@@ -56,6 +58,21 @@ normal forms.
> type instance Res (UpdateT c m) = m
+Evaluation context must provide a predicate that tells whether they
+are solvable.
+
+> class Solvable c
+> where
+> solvable :: c -> Bool
+> bindVars :: MonadPlus m => c -> m c
+
+The unit context is solvable.
+
+> instance Solvable ()
+> where
+> solvable _ = True
+> bindVars = return
+
A strategy is parameterised by an evlauation context of type `c`. The
type of this context may be different from `Ctx s` because a strategy
can be transformed. The strategy operations need to be able to access
@@ -151,6 +168,15 @@ The operation
transforms the base value of a transformed value with a monadic update
operation.
+If an evaluation context is solvable, then a transformed context also
+is. This instance may overlap with more specific instances that
+redefine the operation for specific solvers.
+
+> instance (Solvable c, Transformer t) => Solvable (t c)
+> where
+> solvable = solvable . project
+> bindVars = inside bindVars
+
Strategy Transformers
---------------------
View
@@ -137,6 +137,19 @@ Deconstructors are also defined mechanically:
> dTrue c True = Just (c [])
> dTrue _ _ = Nothing
+We can even define an instance of integers:
+
+> instance ApplyCons Int where type Result Int = Int; applyCons = const
+> instance Generic Int
+> where constr = foldr1 (!) . map intCons $ interleaved [0..] [-1,-2..]
+>
+> interleaved :: [a] -> [a] -> [a]
+> interleaved [] ys = ys
+> interleaved (x:xs) ys = x : interleaved ys xs
+>
+> intCons :: Int -> Int -> GenericOps Int
+> intCons n = cons (show n) n (\c m -> if n==m then Just (c []) else Nothing)
+
Combinators
-----------
Oops, something went wrong.

0 comments on commit aa955c5

Please sign in to comment.