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 , printSolutions = True
145 , copySolutions = False
146 , solutionsInOneFile = False
147 , runsolverCPUTimeLimit = Nothing
148 , runsolverWallTimeLimit = Nothing
149 , runsolverMemoryLimit = Nothing
150 , logLevel = LogNone
151 -- default values for the rest
152 , essenceParams = []
153 , numberingStart = 1
154 , smartFilenames = False
155 , verboseTrail = False
156 , rewritesTrail = False
157 , logRuleFails = False
158 , logRuleSuccesses = False
159 , logRuleAttempts = False
160 , logChoices = False
161 , portfolio = Nothing
162 , strategyQ = "f"
163 , strategyA = "c"
164 , representations = Nothing
165 , representationsFinds = Nothing
166 , representationsGivens = Nothing
167 , representationsAuxiliaries = Nothing
168 , representationsQuantifieds = Nothing
169 , representationsCuts = Nothing
170 , channelling = False
171 , representationLevels = True
172 , unnamedSymmetryBreaking = "none"
173 , followModel = ""
174 , useExistingModels = []
175 , seed = Nothing
176 , limitModels = Nothing
177 , limitTime = Nothing
178 , outputFormat = UI.Plain
179 , lineWidth = 120
180 , responses = ""
181 , responsesRepresentation = ""
182 , generateStreamliners = ""
183 }
184 -- catching the (SR timeout) error, and raising a user error
185 catch solve $ \ (e :: SomeException) -> userErr1 $ vcat
186 [ "Enumerate domain: too many."
187 , "When working on domain:" <++> pretty d
188 , "Exception:" <++> pretty (show e)
189 ]
190 solutions <- filter (".solution" `isSuffixOf`) <$> getDirectoryContents outDir
191 when (length solutions >= enumerateDomainMax) $ userErr1 $ vcat
192 [ "Enumerate domain: too many."
193 , "Gave up after" <+> pretty (length solutions) <+> "solutions."
194 , "When working on domain:" <++> pretty d
195 ]
196 enumeration <- fmap concat $ forM solutions $ \ solutionFile -> do
197 Model _ decls _ <- readModelFromFile (outDir </> solutionFile)
198 let (enumeration, errs) = mconcat
199 [ case decl of
200 Declaration (Letting "x" x) | Just c <- e2c x -> ([c], [])
201 _ -> ([], [decl])
202 | decl <- decls ]
203 if null errs
204 then return enumeration
205 else failDoc $ vcat $ "enumerateDomain, not Constants!"
206 : ("When working on domain:" <++> pretty d)
207 : map pretty errs
208 ++ map (pretty . show) errs
209 removeDirectoryIfExists outDir
210 removeDirectoryIfExists tmpDir
211 return enumeration
212
213
214 enumerateRange :: MonadFailDoc m => Range Constant -> m [Constant]
215 enumerateRange (RangeSingle x) = return [x]
216 enumerateRange (RangeBounded (ConstantInt t x) (ConstantInt _ y)) = return $ ConstantInt t <$> [x..y]
217 enumerateRange RangeBounded{} = failDoc "enumerateRange RangeBounded"
218 enumerateRange RangeOpen{} = failDoc "enumerateRange RangeOpen"
219 enumerateRange RangeLowerBounded{} = failDoc "enumerateRange RangeLowerBounded"
220 enumerateRange RangeUpperBounded{} = failDoc "enumerateRange RangeUpperBounded"
221
222 enumerateInConstant :: MonadFailDoc m => Constant -> m [Constant]
223 enumerateInConstant constant = case constant of
224 ConstantAbstract (AbsLitMatrix _ xs) -> return xs
225 ConstantAbstract (AbsLitSet xs) -> return xs
226 ConstantAbstract (AbsLitMSet xs) -> return xs
227 ConstantAbstract (AbsLitFunction xs) -> return [ ConstantAbstract (AbsLitTuple [i,j]) | (i,j) <- xs ]
228 ConstantAbstract (AbsLitSequence xs) -> return [ ConstantAbstract (AbsLitTuple [i,j])
229 | (i',j) <- zip allNats xs
230 , let i = fromInt i'
231 ]
232 ConstantAbstract (AbsLitRelation xs) -> return $ map (ConstantAbstract . AbsLitTuple) xs
233 ConstantAbstract (AbsLitPartition xs) -> return $ map (ConstantAbstract . AbsLitSet) xs
234 ConstantAbstract (AbsLitPermutation xss) ->
235 let
236 enumPerm [] = []
237 enumPerm (x:xs) = [ ConstantAbstract (AbsLitTuple [i,j]) | (i,j) <- zip (x:xs) xs ] ++
238 [ ConstantAbstract (AbsLitTuple [last xs, x]) ]
239 in
240 return $ concatMap enumPerm xss
241 TypedConstant c _ -> enumerateInConstant c
242 _ -> failDoc $ vcat [ "enumerateInConstant"
243 , "constant:" <+> pretty constant
244 ]