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' = lift . 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 , followModel = ""
172 , useExistingModels = []
173 , seed = Nothing
174 , limitModels = Nothing
175 , limitTime = Nothing
176 , outputFormat = UI.Plain
177 , lineWidth = 120
178 , responses = ""
179 , responsesRepresentation = ""
180 , generateStreamliners = ""
181 }
182 -- catching the (SR timeout) error, and raising a user error
183 catch solve $ \ (e :: SomeException) -> userErr1 $ vcat
184 [ "Enumerate domain: too many."
185 , "When working on domain:" <++> pretty d
186 , "Exception:" <++> pretty (show e)
187 ]
188 solutions <- filter (".solution" `isSuffixOf`) <$> getDirectoryContents outDir
189 when (length solutions >= enumerateDomainMax) $ userErr1 $ vcat
190 [ "Enumerate domain: too many."
191 , "Gave up after" <+> pretty (length solutions) <+> "solutions."
192 , "When working on domain:" <++> pretty d
193 ]
194 enumeration <- fmap concat $ forM solutions $ \ solutionFile -> do
195 Model _ decls _ <- readModelFromFile (outDir </> solutionFile)
196 let (enumeration, errs) = mconcat
197 [ case decl of
198 Declaration (Letting "x" x) | Just c <- e2c x -> ([c], [])
199 _ -> ([], [decl])
200 | decl <- decls ]
201 if null errs
202 then return enumeration
203 else failDoc $ vcat $ "enumerateDomain, not Constants!"
204 : ("When working on domain:" <++> pretty d)
205 : map pretty errs
206 ++ map (pretty . show) errs
207 removeDirectoryIfExists outDir
208 removeDirectoryIfExists tmpDir
209 return enumeration
210
211
212 enumerateRange :: MonadFailDoc m => Range Constant -> m [Constant]
213 enumerateRange (RangeSingle x) = return [x]
214 enumerateRange (RangeBounded (ConstantInt t x) (ConstantInt _ y)) = return $ ConstantInt t <$> [x..y]
215 enumerateRange RangeBounded{} = failDoc "enumerateRange RangeBounded"
216 enumerateRange RangeOpen{} = failDoc "enumerateRange RangeOpen"
217 enumerateRange RangeLowerBounded{} = failDoc "enumerateRange RangeLowerBounded"
218 enumerateRange RangeUpperBounded{} = failDoc "enumerateRange RangeUpperBounded"
219
220 enumerateInConstant :: MonadFailDoc m => Constant -> m [Constant]
221 enumerateInConstant constant = case constant of
222 ConstantAbstract (AbsLitMatrix _ xs) -> return xs
223 ConstantAbstract (AbsLitSet xs) -> return xs
224 ConstantAbstract (AbsLitMSet xs) -> return xs
225 ConstantAbstract (AbsLitFunction xs) -> return [ ConstantAbstract (AbsLitTuple [i,j]) | (i,j) <- xs ]
226 ConstantAbstract (AbsLitSequence xs) -> return [ ConstantAbstract (AbsLitTuple [i,j])
227 | (i',j) <- zip allNats xs
228 , let i = fromInt i'
229 ]
230 ConstantAbstract (AbsLitRelation xs) -> return $ map (ConstantAbstract . AbsLitTuple) xs
231 ConstantAbstract (AbsLitPartition xs) -> return $ map (ConstantAbstract . AbsLitSet) xs
232 TypedConstant c _ -> enumerateInConstant c
233 _ -> failDoc $ vcat [ "enumerateInConstant"
234 , "constant:" <+> pretty constant
235 ]