never executed always true always false
1 module Conjure.Process.Enumerate
2 ( EnumerateDomain
3 , enumerateDomain
4 , enumerateInConstant
5 , EnumerateDomainNoIO(..)
6 ) where
7
8 import Conjure.Prelude
9 import Conjure.Bug
10 import Conjure.UserError
11 import Conjure.Language.AdHoc
12 import Conjure.Language.AbstractLiteral
13 import Conjure.Language.Constant
14 import Conjure.Language.Type
15 import Conjure.Language.Domain
16 import Conjure.Language.Pretty
17 import Conjure.Language.Definition
18 import Conjure.Language.NameGen
19
20 import Conjure.UI.IO
21 import Conjure.UI as UI ( UI(..), OutputFormat(..) )
22 import {-# SOURCE #-} Conjure.UI.MainHelper
23
24 -- temporary
25 import System.IO.Temp ( withSystemTempDirectory )
26
27 -- pipes
28 import qualified Pipes
29
30
31 -- | This class is only to track where `enumerateDomain` might get called.
32 -- It is essentially MonadIO, but doesn't allow arbitrary IO.
33 class (Functor m, Applicative m, Monad m, MonadUserError m) => EnumerateDomain m where liftIO' :: IO a -> m a
34 instance EnumerateDomain IO where liftIO' = id
35 instance EnumerateDomain m => EnumerateDomain (IdentityT m) where liftIO' = lift . liftIO'
36 instance EnumerateDomain m => EnumerateDomain (MaybeT m) where liftIO' = lift . liftIO'
37 instance EnumerateDomain m => EnumerateDomain (ExceptT m) where liftIO' = lift . liftIO'
38 instance EnumerateDomain m => EnumerateDomain (ReaderT r m) where liftIO' = lift . liftIO'
39 instance (EnumerateDomain m, Monoid w) => EnumerateDomain (WriterT w m) where liftIO' = lift . liftIO'
40 instance EnumerateDomain m => EnumerateDomain (StateT st m) where liftIO' = lift . liftIO'
41 instance EnumerateDomain m => EnumerateDomain (Pipes.Proxy a b c d m) where liftIO' = lift . liftIO'
42 instance EnumerateDomain m => EnumerateDomain (NameGenM m) where liftIO' = lift . liftIO'
43 instance (EnumerateDomain m, MonadFail m) => EnumerateDomain (UserErrorT m) where liftIO' = liftUserErrorT . liftIO'
44
45 -- | Use this if you don't want to allow a (EnumerateDomain m => m a) computation actually do IO.
46 data EnumerateDomainNoIO a = Done a | TriedIO | Failed Doc
47 deriving (Show)
48
49 instance Eq a => Eq (EnumerateDomainNoIO a) where
50 (Done a) == (Done b) = a ==b
51 TriedIO == TriedIO = True
52 (Failed _) == (Failed _) = True
53 _ == _ = False
54
55
56 instance Functor EnumerateDomainNoIO where
57 fmap _ (Failed msg) = Failed msg
58 fmap _ TriedIO = TriedIO
59 fmap f (Done x) = Done (f x)
60
61 instance Applicative EnumerateDomainNoIO where
62 pure = Done
63 (<*>) = ap
64
65 instance Monad EnumerateDomainNoIO where
66 Failed msg >>= _ = Failed msg
67 TriedIO >>= _ = TriedIO
68 Done x >>= f = f x
69
70 instance MonadFailDoc EnumerateDomainNoIO where
71 failDoc = Failed
72 instance MonadFail EnumerateDomainNoIO where
73 fail = Failed . stringToDoc
74
75 instance MonadUserError EnumerateDomainNoIO where
76 userErr docs = Failed (vcat $ "User error:" : docs)
77
78 instance NameGen EnumerateDomainNoIO where
79 nextName _ = failDoc "nextName{EnumerateDomainNoIO}"
80 exportNameGenState = failDoc "exportNameGenState{EnumerateDomainNoIO}"
81 importNameGenState _ = failDoc "importNameGenState{EnumerateDomainNoIO}"
82
83 instance EnumerateDomain EnumerateDomainNoIO where liftIO' _ = TriedIO
84
85 enumerateDomainMax :: Int
86 enumerateDomainMax = 10000
87
88 minionTimelimit :: Int
89 minionTimelimit = 60
90
91 savilerowTimelimit :: Int
92 savilerowTimelimit = 60 * 1000
93
94 enumerateDomain :: (MonadFailDoc m, EnumerateDomain m) => Domain () Constant -> m [Constant]
95
96 enumerateDomain d | not (null [ () | ConstantUndefined{} <- universeBi d ]) =
97 bug $ vcat [ "called enumerateDomain with a domain that has undefinedness values in it."
98 , pretty d
99 ]
100
101 enumerateDomain DomainBool = return [ConstantBool False, ConstantBool True]
102 enumerateDomain (DomainInt _ []) = failDoc "enumerateDomain: infinite domain"
103 enumerateDomain (DomainInt _ rs) = concatMapM enumerateRange rs
104 enumerateDomain (DomainUnnamed _ (ConstantInt t n)) = return (map (ConstantInt t) [1..n])
105 enumerateDomain (DomainEnum _dName (Just rs) _mp) = concatMapM enumerateRange rs
106 enumerateDomain (DomainTuple ds) = do
107 inners <- mapM enumerateDomain ds
108 return $ map (ConstantAbstract . AbsLitTuple) (sequence inners)
109 enumerateDomain (DomainMatrix (DomainInt t indexDom) innerDom) = do
110 inners <- enumerateDomain innerDom
111 indexInts <- rangesInts indexDom
112 return
113 [ ConstantAbstract (AbsLitMatrix (DomainInt t indexDom) vals)
114 | vals <- replicateM (length indexInts) inners
115 ]
116
117 -- the sledgehammer approach
118 enumerateDomain d = liftIO' $ withSystemTempDirectory ("conjure-enumerateDomain-" ++ show (hash d)) $ \ tmpDir -> do
119 let model = Model { mLanguage = LanguageVersion "Essence" [1,0]
120 , mStatements = [Declaration (FindOrGiven Find "x" (fmap Constant d))]
121 , mInfo = def
122 }
123 let essenceFile = tmpDir </> "out.essence"
124 let outDir = tmpDir </> "outDir"
125 writeModel 120 Plain (Just essenceFile) model
126 let
127 solve :: IO ()
128 solve = let ?typeCheckerMode = StronglyTyped in ignoreLogs $ runNameGen () $ mainWithArgs Solve
129 { UI.essence = essenceFile
130 , validateSolutionsOpt = False
131 , outputDirectory = outDir
132 , savilerowOptions =
133 [ "-O0"
134 , "-preprocess" , "None"
135 , "-timelimit" , show savilerowTimelimit
136 ]
137 , solverOptions =
138 [ "-cpulimit" , show minionTimelimit
139 ]
140 , solver = "minion"
141 , graphSolver = False
142 , cgroups = False
143 , nbSolutions = show enumerateDomainMax
144 , copySolutions = False
145 , solutionsInOneFile = False
146 , runsolverCPUTimeLimit = Nothing
147 , runsolverWallTimeLimit = Nothing
148 , runsolverMemoryLimit = Nothing
149 , logLevel = LogNone
150 -- default values for the rest
151 , essenceParams = []
152 , numberingStart = 1
153 , smartFilenames = False
154 , verboseTrail = False
155 , rewritesTrail = False
156 , logRuleFails = False
157 , logRuleSuccesses = False
158 , logRuleAttempts = False
159 , logChoices = False
160 , portfolio = Nothing
161 , strategyQ = "f"
162 , strategyA = "c"
163 , representations = Nothing
164 , representationsFinds = Nothing
165 , representationsGivens = Nothing
166 , representationsAuxiliaries = Nothing
167 , representationsQuantifieds = Nothing
168 , representationsCuts = Nothing
169 , channelling = False
170 , representationLevels = True
171 , unnamedSymmetryBreaking = "none"
172 , followModel = ""
173 , useExistingModels = []
174 , seed = Nothing
175 , limitModels = Nothing
176 , limitTime = Nothing
177 , outputFormat = UI.Plain
178 , lineWidth = 120
179 , responses = ""
180 , responsesRepresentation = ""
181 , generateStreamliners = ""
182 }
183 -- catching the (SR timeout) error, and raising a user error
184 catch solve $ \ (e :: SomeException) -> userErr1 $ vcat
185 [ "Enumerate domain: too many."
186 , "When working on domain:" <++> pretty d
187 , "Exception:" <++> pretty (show e)
188 ]
189 solutions <- filter (".solution" `isSuffixOf`) <$> getDirectoryContents outDir
190 when (length solutions >= enumerateDomainMax) $ userErr1 $ vcat
191 [ "Enumerate domain: too many."
192 , "Gave up after" <+> pretty (length solutions) <+> "solutions."
193 , "When working on domain:" <++> pretty d
194 ]
195 enumeration <- fmap concat $ forM solutions $ \ solutionFile -> do
196 Model _ decls _ <- readModelFromFile (outDir </> solutionFile)
197 let (enumeration, errs) = mconcat
198 [ case decl of
199 Declaration (Letting "x" x) | Just c <- e2c x -> ([c], [])
200 _ -> ([], [decl])
201 | decl <- decls ]
202 if null errs
203 then return enumeration
204 else failDoc $ vcat $ "enumerateDomain, not Constants!"
205 : ("When working on domain:" <++> pretty d)
206 : map pretty errs
207 ++ map (pretty . show) errs
208 removeDirectoryIfExists outDir
209 removeDirectoryIfExists tmpDir
210 return enumeration
211
212
213 enumerateRange :: MonadFailDoc m => Range Constant -> m [Constant]
214 enumerateRange (RangeSingle x) = return [x]
215 enumerateRange (RangeBounded (ConstantInt t x) (ConstantInt _ y)) = return $ ConstantInt t <$> [x..y]
216 enumerateRange RangeBounded{} = failDoc "enumerateRange RangeBounded"
217 enumerateRange RangeOpen{} = failDoc "enumerateRange RangeOpen"
218 enumerateRange RangeLowerBounded{} = failDoc "enumerateRange RangeLowerBounded"
219 enumerateRange RangeUpperBounded{} = failDoc "enumerateRange RangeUpperBounded"
220
221 enumerateInConstant :: MonadFailDoc m => Constant -> m [Constant]
222 enumerateInConstant constant = case constant of
223 ConstantAbstract (AbsLitMatrix _ xs) -> return xs
224 ConstantAbstract (AbsLitSet xs) -> return xs
225 ConstantAbstract (AbsLitMSet xs) -> return xs
226 ConstantAbstract (AbsLitFunction xs) -> return [ ConstantAbstract (AbsLitTuple [i,j]) | (i,j) <- xs ]
227 ConstantAbstract (AbsLitSequence xs) -> return [ ConstantAbstract (AbsLitTuple [i,j])
228 | (i',j) <- zip allNats xs
229 , let i = fromInt i'
230 ]
231 ConstantAbstract (AbsLitRelation xs) -> return $ map (ConstantAbstract . AbsLitTuple) xs
232 ConstantAbstract (AbsLitPartition xs) -> return $ map (ConstantAbstract . AbsLitSet) xs
233 ConstantAbstract (AbsLitPermutation xss) ->
234 let
235 enumPerm [] = []
236 enumPerm (x:xs) = [ ConstantAbstract (AbsLitTuple [i,j]) | (i,j) <- zip (x:xs) xs ] ++
237 [ ConstantAbstract (AbsLitTuple [last xs, x]) ]
238 in
239 return $ concatMap enumPerm xss
240 TypedConstant c _ -> enumerateInConstant c
241 _ -> failDoc $ vcat [ "enumerateInConstant"
242 , "constant:" <+> pretty constant
243 ]