{-# language DeriveFunctor #-}
{-# language FlexibleContexts #-}
{-# language GADTs #-}
{-# language GeneralizedNewtypeDeriving #-}
{-# language LambdaCase #-}
{-# language NamedFieldPuns #-}
{-# language OverloadedStrings #-}
{-# language RecordWildCards #-}
module FastDownward
(
Problem
, Var
, newVar
, readVar
, writeVar
, modifyVar
, resetInitial
, Effect
, Test
, (?=)
, FastDownward.any
, requiresAxioms
, solve
, SolveResult(..)
, Solution
, runProblem
, totallyOrderedPlan
, partiallyOrderedPlan
)
where
import Control.Applicative ( Alternative(..) )
import qualified Control.Monad.Fail
import Control.Monad.IO.Class ( MonadIO, liftIO )
import Control.Monad.State.Class ( get, gets, modify )
import Control.Monad.Trans.Cont
import Control.Monad.Trans.Reader ( ReaderT(..), runReaderT )
import Control.Monad.Trans.State.Lazy ( StateT, evalStateT )
import Data.Coerce ( coerce )
import qualified Data.Foldable
import qualified Data.Graph
import Data.IORef
import Data.IntMap.Lazy ( IntMap )
import qualified Data.IntMap.Lazy as IntMap
import Data.List ( inits, intersect )
import Data.Map.Lazy ( Map )
import qualified Data.Map.Lazy as Map
import Data.Maybe ( mapMaybe )
import Data.Sequence ( Seq )
import qualified Data.Sequence as Seq
import Data.String ( fromString )
import qualified Data.Text.Lazy
import qualified Data.Text.Lazy.IO
import Data.Traversable ( for )
import qualified FastDownward.Exec as Exec
import qualified FastDownward.SAS
import qualified FastDownward.SAS.Axiom
import qualified FastDownward.SAS.Effect
import qualified FastDownward.SAS.Operator
import qualified FastDownward.SAS.Plan
import qualified FastDownward.SAS.Variable
import Prelude hiding ( reads )
import System.Exit
import System.IO.Temp
data Var a =
Var
{ variableIndex :: {-# UNPACK #-} !FastDownward.SAS.VariableIndex
, values :: {-# UNPACK #-} !( IORef ( Map a ( Committed, FastDownward.SAS.DomainIndex ) ) )
, subscribed :: {-# UNPACK #-} !( IORef ( a -> FastDownward.SAS.DomainIndex -> IO () ) )
, fromDomainIndex :: {-# UNPACK #-} !( IORef ( Map FastDownward.SAS.DomainIndex a ) )
}
data Committed =
Committed | Uncommitted
newtype Problem a =
Problem { unProblem :: StateT ProblemState IO a }
deriving
( Functor, Applicative, Monad, MonadIO )
data VariableDeclaration =
VariableDeclaration
{ initial :: {-# UNPACK #-} !FastDownward.SAS.DomainIndex
, _enumerateDomain :: IO [ FastDownward.SAS.DomainIndex ]
, _axiomLayer :: {-# UNPACK #-} !Int
}
data ProblemState =
ProblemState
{ initialState :: !( Map FastDownward.SAS.VariableIndex VariableDeclaration )
, axioms :: !( Seq FastDownward.SAS.Axiom )
}
observeValue :: ( Ord a, MonadIO m ) => Var a -> a -> m FastDownward.SAS.DomainIndex
observeValue var a = liftIO $ do
vs <-
readIORef ( values var )
case Map.lookup a vs of
Just ( _, i ) ->
return i
Nothing -> do
let
i =
FastDownward.SAS.DomainIndex ( fromIntegral ( Map.size vs ) )
modifyIORef ( fromDomainIndex var ) ( Map.insert i a )
i <$ modifyIORef ( values var ) ( Map.insert a ( Uncommitted, i ) )
commit :: ( Ord a, MonadIO m ) => Var a -> a -> m ()
commit var a = liftIO $ do
modifyIORef ( values var ) ( Map.adjust ( \( _, x ) -> ( Committed, x ) ) a )
newVar :: Ord a => a -> Problem ( Var a )
newVar =
newVarAt (-1)
newVarAt :: Ord a => Int -> a -> Problem ( Var a )
newVarAt axiomLayer initialValue = do
values <-
liftIO ( newIORef mempty )
variableIndex <-
freshIndex
subscribed <-
liftIO ( newIORef ( \_ _ -> return () ) )
fromDomainIndex <-
liftIO ( newIORef mempty )
let
enumerate =
map snd . Map.elems <$> liftIO ( readIORef values )
var =
Var{..}
initialI <-
observeValue var initialValue
commit var initialValue
Problem
( modify
( \ps ->
ps
{ initialState =
Map.insert
variableIndex
( VariableDeclaration initialI enumerate axiomLayer )
( initialState ps )
}
)
)
return var
freshIndex :: Problem FastDownward.SAS.VariableIndex
freshIndex =
FastDownward.SAS.VariableIndex <$> Problem ( gets ( fromIntegral . Map.size . initialState ) )
writeVar :: Ord a => Var a -> a -> Effect ()
writeVar var a = Effect $ do
edomainIndex <- liftIO $ do
currentValues <-
readIORef ( values var )
case Map.lookup a currentValues of
Just ( Committed, domainIndex ) ->
return ( Right domainIndex )
Just ( Uncommitted, domainIndex ) ->
return ( Left domainIndex )
Nothing -> do
Left <$> observeValue var a
ContT $ \k -> ReaderT $ \es -> do
es' <-
case edomainIndex of
Left domainIndex -> do
laterRef <-
newIORef $ do
currentValues <-
readIORef ( values var )
case Map.lookup a currentValues of
Just ( Committed, _ ) ->
return ()
_ -> do
commit var a
notify <-
readIORef ( subscribed var )
notify a domainIndex
return
es
{ writes =
IntMap.insert ( coerce ( variableIndex var ) ) domainIndex ( writes es )
, onCommit = do
action <-
readIORef laterRef
writeIORef laterRef ( return () )
>> action
>> onCommit es
}
Right domainIndex ->
return
es
{ writes =
IntMap.insert ( coerce ( variableIndex var ) ) domainIndex ( writes es )
}
runReaderT ( k () ) es'
readVar :: Ord a => Var a -> Effect a
readVar var = Effect $ ContT $ \k -> ReaderT $ \es -> do
let
mPrevRead =
IntMap.lookup ( coerce ( variableIndex var ) ) ( reads es )
mPrevWrite =
IntMap.lookup ( coerce ( variableIndex var ) ) ( writes es )
case ( mPrevWrite, mPrevRead ) of
( Just prevWriteIndex, _ ) -> do
prevWrite <-
( Map.! prevWriteIndex ) <$> readIORef ( fromDomainIndex var )
runReaderT ( k prevWrite ) es
( Nothing, Just prevReadIndex ) -> do
prevRead <-
( Map.! prevReadIndex ) <$> readIORef ( fromDomainIndex var )
runReaderT ( k prevRead ) es
( Nothing, Nothing ) -> do
let
runRecordingRead a domainIndex =
let
es' =
es
{ reads =
IntMap.insert ( coerce ( variableIndex var ) ) domainIndex ( reads es )
}
in runReaderT ( k a ) es'
currentValues <-
readIORef ( values var )
modifyIORef
( subscribed var )
( \io x y -> runRecordingRead x y >> io x y )
Map.foldMapWithKey
( \a ( committed, domainIndex ) ->
case committed of
Committed ->
runRecordingRead a domainIndex
_ ->
return ()
)
currentValues
modifyVar :: Ord a => Var a -> ( a -> a ) -> Effect ()
modifyVar v f =
readVar v >>= writeVar v . f
newtype Effect a =
Effect { runEffect :: ContT () ( ReaderT EffectState IO ) a }
deriving
( Functor, Applicative )
instance Monad Effect where
return a =
Effect ( return a )
{-# INLINE return #-}
Effect a >>= f = Effect $
a >>= runEffect . f
{-# INLINE (>>=) #-}
instance Control.Monad.Fail.MonadFail Effect where
fail _ =
empty
{-# INLINE fail #-}
instance Alternative Effect where
empty =
Effect ( ContT ( \_k -> return () ) )
{-# INLINE empty #-}
Effect a <|> Effect b =
Effect $ ContT $ \k ->
runContT a k <|> runContT b k
{-# INLINE (<|>) #-}
data EffectState =
EffectState
{ reads :: IntMap FastDownward.SAS.DomainIndex
, writes :: IntMap FastDownward.SAS.DomainIndex
, onCommit :: IO ()
}
data SolveResult a
= Unsolvable
| UnsolvableIncomplete
| OutOfMemory
| OutOfTime
| CriticalError
| InputError
| Unsupported
| Crashed String String ExitCode
| Solved ( Solution a )
deriving
( Functor, Show )
data Solution a =
Solution
{ sas :: FastDownward.SAS.Plan
, operators :: IntMap.IntMap a
, stepIndices :: [ IntMap.Key ]
}
deriving
( Functor, Show )
totallyOrderedPlan :: Solution a -> [ a ]
totallyOrderedPlan Solution{..} =
map ( operators IntMap.! ) stepIndices
solve
:: Show a
=> Exec.SearchConfiguration
-> [ Effect a ]
-> [ Test ]
-> Problem ( SolveResult a )
solve cfg ops tests = do
s0 <-
Problem get
Problem $ liftIO $ flip evalStateT s0 $ do
goal <-
unProblem ( Prelude.traverse testToVariableAssignment tests )
operators <-
liftIO ( exhaustEffects ops )
initialState <-
gets initialState
axioms <-
gets axioms
variables <-
for
( Map.toAscList initialState )
( \( FastDownward.SAS.VariableIndex i
, VariableDeclaration _ enumerate axiomLayer
) -> do
domain <-
liftIO enumerate
return
FastDownward.SAS.Variable
{ name =
fromString ( "var-" <> show i )
, domain =
Seq.fromList $
map
( \( FastDownward.SAS.DomainIndex d ) ->
fromString
( "Atom var-" <> show i <> "(" <> show d <> ")" )
)
domain
++ [ "Atom dummy(dummy)" ]
, axiomLayer = axiomLayer
}
)
let
plan =
FastDownward.SAS.Plan
{ version =
FastDownward.SAS.SAS3
, useCosts =
FastDownward.SAS.NoCosts
, variables =
Seq.fromList variables
, mutexGroups =
mempty
, initialState =
FastDownward.SAS.State
( Seq.fromList $ map ( initial . snd ) ( Map.toAscList initialState ) )
, goal =
FastDownward.SAS.Goal ( Seq.fromList goal )
, operators =
Seq.fromList $ zipWith
( \i ( _, EffectState{ reads, writes } ) ->
let
unchangedWrites =
IntMap.mapMaybe
( \( a, b ) -> if a == b then Just a else Nothing )
( IntMap.intersectionWith (,) writes reads )
actualWrites =
writes `IntMap.difference` unchangedWrites
in
FastDownward.SAS.Operator
{ name = fromString ( "op" <> show i )
, prevail =
Seq.fromList $ map
( \( x, y ) -> FastDownward.SAS.VariableAssignment ( coerce x ) y )
( IntMap.toList
( IntMap.difference reads writes <> unchangedWrites
)
)
, effects =
Seq.fromList $ map
( \( v, post ) -> FastDownward.SAS.Effect ( coerce v ) Nothing post )
( IntMap.toList ( IntMap.difference writes reads ) )
++
IntMap.elems
( IntMap.intersectionWithKey
( \v pre post ->
FastDownward.SAS.Effect ( coerce v ) ( Just pre ) post
)
reads
actualWrites
)
}
)
[ 0 :: Int .. ]
operators
, axioms =
Seq.fromList $ Data.Foldable.toList axioms
}
planFilePath <-
liftIO ( emptySystemTempFile "sas_plan" )
( exitCode, stdout, stderr ) <-
liftIO
( Exec.callFastDownward
Exec.Options
{ fastDownward = "downward"
, problem = plan
, planFilePath = planFilePath
, searchConfiguration = cfg
}
)
case exitCode of
ExitFailure 11 ->
return Unsolvable
ExitFailure 12 ->
return UnsolvableIncomplete
ExitFailure 22 ->
return OutOfMemory
ExitFailure 23 ->
return OutOfTime
ExitFailure 32 ->
return CriticalError
ExitFailure 33 ->
return InputError
ExitFailure 34 ->
return Unsupported
ExitFailure other ->
return ( Crashed stdout stderr ( ExitFailure other ) )
ExitSuccess -> liftIO $ do
planText <-
Data.Text.Lazy.IO.readFile planFilePath
let
stepIndices =
map
( read
. Data.Text.Lazy.unpack
. Data.Text.Lazy.init
. Data.Text.Lazy.drop 3
)
( takeWhile
( "(" `Data.Text.Lazy.isPrefixOf` )
( Data.Text.Lazy.lines planText )
)
return
( Solved
Solution
{ sas = plan
, operators = IntMap.fromList ( zip [0..] ( map fst operators ) )
, ..
}
)
exhaustEffects
:: Traversable t
=> t ( Effect a )
-> IO [ ( a, EffectState ) ]
exhaustEffects ops = do
out <-
newIORef []
Data.Foldable.for_
ops
( \( Effect ( ContT k ) ) ->
runReaderT
( k
( \a ->
ReaderT $ \es -> do
onCommit es
let
es' = es { onCommit = return () }
modifyIORef out ( ( a, es' ) : )
)
)
s0
)
readIORef out
where
s0 =
EffectState mempty mempty ( return () )
runProblem :: MonadIO m => Problem a -> m a
runProblem p = liftIO $
evalStateT
( unProblem p )
ProblemState { initialState = mempty , axioms = mempty }
(?=) :: Ord a => Var a -> a -> Test
(?=) =
TestEq
data Test where
TestEq :: Ord a => {-# UNPACK #-} !( Var a ) -> !a -> Test
Any :: ![ Test ] -> Test
requiresAxioms :: Test -> Bool
requiresAxioms =
\case
TestEq{} ->
False
Any{} ->
True
resetInitial :: Ord a => Var a -> a -> Problem ()
resetInitial var a = do
liftIO ( writeIORef ( values var ) mempty )
liftIO ( writeIORef ( fromDomainIndex var ) mempty )
i <-
observeValue var a
commit var a
Problem $ modify $ \ps ->
ps
{ initialState =
Map.adjust
( \decl -> decl { initial = i } )
( variableIndex var )
( initialState ps )
}
any :: [ Test ] -> Test
any =
Any
testToVariableAssignment :: Test -> Problem FastDownward.SAS.VariableAssignment
testToVariableAssignment ( TestEq var a ) =
FastDownward.SAS.VariableAssignment ( variableIndex var )
<$> observeValue var a
testToVariableAssignment ( Any tests ) = do
axiom <-
newVarAt 0 False
falseI <-
observeValue axiom False
trueI <-
observeValue axiom True
assigns <-
Prelude.traverse testToVariableAssignment tests
Problem $ modify $ \ps ->
ps
{ axioms =
Seq.fromList
[ FastDownward.SAS.Axiom
{ variable = variableIndex axiom
, conditions = Seq.singleton va
, pre = falseI
, post = trueI
}
| va <- assigns
]
<> axioms ps
}
return ( FastDownward.SAS.VariableAssignment ( variableIndex axiom ) trueI )
partiallyOrderedPlan
:: Ord a
=> Solution a
-> ( Data.Graph.Graph
, Data.Graph.Vertex -> ( a, IntMap.Key, [ IntMap.Key ] )
, IntMap.Key -> Maybe Data.Graph.Vertex
)
partiallyOrderedPlan Solution{..} =
let
ops =
IntMap.fromList ( zip [0..] ( Data.Foldable.toList ( FastDownward.SAS.Plan.operators sas ) ) )
operation i =
ops IntMap.! i
g = do
( i, o ) : priorReversed <-
map
reverse
( tail ( inits ( map ( \i -> ( i, operation i ) ) stepIndices ) ) )
let
priors =
reverse priorReversed
return
( operators IntMap.! i
, i
, mapMaybe
( \( j, x ) -> if o `after` x then Just j else Nothing )
priors
)
( gr, fromVertex, toVertex ) =
Data.Graph.graphFromEdges g
in
( Data.Graph.transposeG gr, fromVertex, toVertex )
assignments :: FastDownward.SAS.Operator -> [ FastDownward.SAS.VariableAssignment ]
assignments o =
[ FastDownward.SAS.VariableAssignment
( FastDownward.SAS.Effect.variable e )
( FastDownward.SAS.Effect.post e )
| e <- Data.Foldable.toList ( FastDownward.SAS.Operator.effects o )
]
requirements :: FastDownward.SAS.Operator -> Seq FastDownward.SAS.VariableAssignment
requirements o =
FastDownward.SAS.Operator.prevail o <> Seq.fromList ( original o )
original :: FastDownward.SAS.Operator -> [ FastDownward.SAS.VariableAssignment ]
original o =
mapMaybe
( \e ->
FastDownward.SAS.VariableAssignment ( FastDownward.SAS.Effect.variable e )
<$> FastDownward.SAS.Effect.pre e
)
( Data.Foldable.toList ( FastDownward.SAS.Operator.effects o ) )
after
:: FastDownward.SAS.Operator.Operator
-> FastDownward.SAS.Operator.Operator
-> Bool
o `after` x =
not ( null ( Data.Foldable.toList ( requirements o ) `intersect` assignments x ) ) ||
not ( null ( Data.Foldable.toList ( requirements x ) `intersect` original o ) )