never executed always true always false
1 {-# LANGUAGE RecordWildCards #-}
2
3 module Conjure.UI.MainHelper ( mainWithArgs, savilerowScriptName ) where
4
5 import Conjure.Prelude
6 import Conjure.Bug
7 import Conjure.UserError
8 import Conjure.UI ( UI(..), OutputFormat(..) )
9 import Conjure.UI.IO ( readModel, readModelFromFile, readModelFromStdin
10 , readModelInfoFromFile, readParamOrSolutionFromFile
11 , writeModel )
12 import Conjure.UI.Model ( parseStrategy, outputModels, modelRepresentationsJSON, prologue )
13 import qualified Conjure.UI.Model as Config ( Config(..) )
14 import Conjure.UI.TranslateParameter ( translateParameter )
15 import Conjure.UI.TranslateSolution ( translateSolution )
16 import Conjure.UI.ValidateSolution ( validateSolution )
17 import Conjure.UI.TypeCheck ( typeCheckModel_StandAlone, typeCheckModel )
18 import Conjure.UI.Split ( outputSplittedModels, removeUnusedDecls )
19 import Conjure.UI.VarSymBreaking ( outputVarSymBreaking )
20 import Conjure.UI.ParameterGenerator ( parameterGenerator )
21 import Conjure.UI.NormaliseQuantified ( normaliseQuantifiedVariables )
22 import Conjure.UI.SolveStats ( mkSolveStats )
23
24 import Conjure.Language.Name ( Name(..) )
25 import Conjure.Language.Definition ( Model(..), ModelInfo(..), Statement(..), Declaration(..), FindOrGiven(..) )
26 import Conjure.Language.Type ( TypeCheckerMode(..) )
27 import Conjure.Language.Domain ( Domain(..), Range(..) )
28 import Conjure.Language.NameGen ( NameGen, NameGenM, runNameGen )
29 import Conjure.Language.Pretty
30 import qualified Conjure.Language.ParserC as ParserC ( parseModel )
31 import Conjure.Language.ModelDiff ( modelDiffIO )
32 import Conjure.Rules.Definition ( viewAuto, Strategy(..) )
33 import Conjure.Process.Enumerate ( EnumerateDomain )
34 import Conjure.Process.Streamlining ( streamlining, streamliningToStdout )
35 import Conjure.Language.NameResolution ( resolveNames, resolveNamesMulti )
36 import Conjure.Process.Boost ( boost )
37 import Conjure.Language.ModelStats ( modelDeclarationsJSON )
38 import Conjure.Language.AdHoc ( toSimpleJSON )
39
40
41 -- base
42 import Control.Exception ( IOException, handle )
43 import System.IO ( Handle, hSetBuffering, stdout, BufferMode(..), hPutStrLn, stderr )
44 import System.Environment ( getEnvironment )
45 import System.Info ( os )
46 import GHC.Conc ( numCapabilities )
47 import GHC.IO.Handle ( hIsEOF, hClose, hGetLine )
48 import Data.Char ( isDigit )
49
50 import qualified Data.Set as S -- containers
51 import qualified Data.HashMap.Strict as M -- unordered-containers
52
53 -- filepath
54 import System.FilePath ( splitFileName, takeBaseName, (<.>) )
55
56 -- directory
57 import System.Directory ( copyFile, findExecutable )
58
59 -- shelly
60 import Shelly ( runHandle, lastStderr, lastExitCode, errExit, Sh )
61
62 -- text
63 import qualified Data.Text as T ( unlines, isInfixOf )
64
65 -- parallel-io
66 import Control.Concurrent.ParallelIO.Global ( parallel, stopGlobalPool )
67 import Conjure.LSP.LanguageServer (startServer, LSPConfig (LSPConfig))
68
69
70 mainWithArgs :: forall m .
71 MonadIO m =>
72 MonadLog m =>
73 MonadFailDoc m =>
74 EnumerateDomain m =>
75 NameGen m =>
76 (?typeCheckerMode :: TypeCheckerMode) =>
77 UI -> m ()
78 mainWithArgs LSP{} = liftIO $ startServer LSPConfig
79 mainWithArgs mode@Modelling{..} = do
80 essenceM <- readModelFromFile essence
81 doIfNotCached -- start the show!
82 ( sort (mStatements essenceM)
83 , portfolio
84 -- when the following flags change, invalidate hash
85 -- nested tuples, because :(
86 , ( numberingStart
87 , smartFilenames
88 , strategyQ
89 , strategyA
90 , responses
91 )
92 , ( representations
93 , representationsFinds
94 , representationsGivens
95 , representationsAuxiliaries
96 , representationsQuantifieds
97 , representationsCuts
98 )
99 , ( channelling
100 , representationLevels
101 , seed
102 , limitModels
103 , limitTime
104 , outputFormat
105 )
106 , generateStreamliners
107 )
108 (outputDirectory </> ".conjure-checksum")
109 (pp logLevel "Using cached models.")
110 (void $ mainWithArgs_Modelling "" mode Nothing S.empty)
111 mainWithArgs TranslateParameter{..} = do
112 when (null eprime ) $ userErr1 "Mandatory field --eprime"
113 when (null essenceParam) $ userErr1 "Mandatory field --essence-param"
114 let outputFilename = fromMaybe (dropExtension essenceParam ++ ".eprime-param") eprimeParam
115 eprimeF <- readModelInfoFromFile eprime
116 essenceParamF <- readParamOrSolutionFromFile eprimeF essenceParam
117 output <- runNameGen () $ translateParameter False eprimeF essenceParamF
118 writeModel lineWidth outputFormat (Just outputFilename) output
119 mainWithArgs TranslateSolution{..} = do
120 when (null eprime ) $ userErr1 "Mandatory field --eprime"
121 when (null eprimeSolution) $ userErr1 "Mandatory field --eprime-solution"
122 eprimeF <- readModelInfoFromFile eprime
123 essenceParamF <- maybe (return def) (readParamOrSolutionFromFile eprimeF) essenceParamO
124 eprimeSolutionF <- readParamOrSolutionFromFile eprimeF eprimeSolution
125 output <- runNameGen () $ translateSolution eprimeF essenceParamF eprimeSolutionF
126 let outputFilename = fromMaybe (dropExtension eprimeSolution ++ ".solution") essenceSolutionO
127 writeModel lineWidth outputFormat (Just outputFilename) output
128 mainWithArgs ValidateSolution{..} = do
129 when (null essence ) $ userErr1 "Mandatory field --essence"
130 when (null essenceSolution) $ userErr1 "Mandatory field --solution"
131 essence2 <- readModelFromFile essence
132 param2 <- maybe (return def) (readParamOrSolutionFromFile essence2) essenceParamO
133 solution2 <- readParamOrSolutionFromFile essence2 essenceSolution
134 [essence3, param3, solution3] <- runNameGen () $ resolveNamesMulti [essence2, param2, solution2]
135 runNameGen () $ validateSolution essence3 param3 solution3
136 mainWithArgs IDE{..} = do
137 essence2 <-
138 if null essence
139 then readModelFromStdin
140 else readModelFromFile essence
141 void $ runNameGen () $ typeCheckModel_StandAlone essence2
142 if
143 | dumpDeclarations -> liftIO $ putStrLn $ render lineWidth (modelDeclarationsJSON essence2)
144 | dumpRepresentations -> do
145 json <- runNameGen () $ modelRepresentationsJSON essence2
146 liftIO $ putStrLn $ render lineWidth json
147 | otherwise -> writeModel lineWidth ASTJSON Nothing essence2
148 -- mainWithArgs Pretty{..} | outputFormat == Plain= do
149 -- (_,cts) <- liftIO $ pairWithContents essence
150 -- res <- prettyPrintWithChecks cts
151 -- liftIO $ putStrLn $ render lineWidth res
152 mainWithArgs Pretty{..} = do
153 model0 <- if or [ s `isSuffixOf` essence
154 | s <- [".param", ".eprime-param", ".solution", ".eprime.solution"] ]
155 then do
156 liftIO $ hPutStrLn stderr "Parsing as a parameter file"
157 readParamOrSolutionFromFile def essence
158 else readModelFromFile essence
159 let model1 = model0
160 |> (if normaliseQuantified then normaliseQuantifiedVariables else id)
161 |> (if removeUnused then removeUnusedDecls else id)
162 writeModel lineWidth outputFormat Nothing model1
163
164 mainWithArgs Diff{..} =
165 join $ modelDiffIO
166 <$> readModelFromFile file1
167 <*> readModelFromFile file2
168 mainWithArgs TypeCheck{..} = do
169 essenceF <- readModelFromFile essence
170 void $ runNameGen () $ typeCheckModel_StandAlone essenceF
171 mainWithArgs Split{..} = do
172 model <- readModelFromFile essence
173 outputSplittedModels outputDirectory model
174 mainWithArgs SymmetryDetection{..} = do
175 let jsonFilePath = if null json then essence ++ "-json" else json
176 model <- readModelFromFile essence
177 outputVarSymBreaking jsonFilePath model
178 mainWithArgs ParameterGenerator{..} = do
179 model <- readModelFromFile essence
180 ((genModel, repairModel), classes) <- runNameGen () $ parameterGenerator minInt maxInt model
181
182 let genModelOut = dropExtension essence ++ "-instanceGenerator.essence"
183 writeModel lineWidth outputFormat (Just genModelOut) genModel
184
185 let repairModelOut = dropExtension essence ++ "-instanceRepair.essence"
186 writeModel lineWidth outputFormat (Just repairModelOut) repairModel
187
188 let
189 toIrace nm lb ub _ | lb == ub =
190 pretty nm <+>
191 "\"-" <> pretty nm <> " \" c" <+>
192 prParens (pretty lb)
193 toIrace nm lb ub (Just klass) =
194 pretty nm <+>
195 "\"-" <> pretty nm <> " \" " <> pretty klass <+>
196 prettyList prParens "," [lb, ub]
197 toIrace nm _ _ Nothing = bug ("Missing class for:" <+> pretty nm)
198
199 essenceOutFileContents = render lineWidth $ vcat
200 [ toIrace nm lb ub (lookup nm classes)
201 | Declaration (FindOrGiven Given nm (DomainInt _ [RangeBounded lb ub])) <- mStatements genModel
202 ]
203 liftIO $ writeFile (genModelOut ++ ".irace") (essenceOutFileContents ++ "\n")
204 mainWithArgs Streamlining{..} = runNameGen essence
205 (readModelFromFile essence >>= resolveNames >>= typeCheckModel >>= streamliningToStdout)
206 mainWithArgs AutoIG{..} | generatorToIrace = do
207 model <- readModelFromFile essence
208 let
209 toIrace nm lb ub | lb == ub =
210 pretty nm <+>
211 "\"-" <> pretty nm <> " \" c" <+>
212 prParens (pretty lb)
213 toIrace nm lb ub =
214 pretty nm <+>
215 "\"-" <> pretty nm <> " \" i" <+>
216 prettyList prParens "," [lb, ub]
217 let (iraceStmts, errors) = mconcat
218 [ case st of
219 Declaration (FindOrGiven Given nm domain) ->
220 case domain of
221 DomainInt _ [RangeBounded lb ub] -> ([toIrace nm lb ub], [])
222 _ -> ([], ["Unsupported domain for given" <+> pretty nm <> ":" <+> pretty domain])
223 _ -> ([], [])
224 | st <- mStatements model
225 ]
226 if null errors
227 then do
228 let essenceOutFileContents = render lineWidth $ vcat iraceStmts
229 liftIO $ writeFile outputFilepath (essenceOutFileContents ++ "\n")
230 else
231 userErr errors
232 mainWithArgs AutoIG{..} | removeAux = do
233 model <- readModelFromFile essence
234 let stmts' = [ case st of
235 Declaration (FindOrGiven _ nm _) | "Aux" `isPrefixOf` show (pretty nm) -> Nothing
236 | otherwise -> Just st
237 Declaration (Letting nm _) | "Aux" `isPrefixOf` show (pretty nm) -> Nothing
238 | otherwise -> Just st
239 _ -> Just st
240 | st <- mStatements model
241 ]
242 writeModel lineWidth outputFormat (Just outputFilepath) model {mStatements = catMaybes stmts'}
243 mainWithArgs AutoIG{} = userErr1 "You must pass one of --generator-to-irace or --remove-aux to this command."
244 mainWithArgs Boost{..} = do
245 model <- readModelFromFile essence
246 runNameGen model $ do
247 boosted <- boost logLevel logRuleSuccesses model
248 writeModel lineWidth outputFormat Nothing boosted
249 mainWithArgs config@Solve{..} = do
250 liftIO $ createDirectoryIfMissing True outputDirectory
251 -- some sanity checks
252 (solverName, _smtLogicName) <- splitSolverName solver
253 case lookup solverName solverExecutables of
254 Nothing -> userErr1 ("Unsupported solver:" <+> pretty solver)
255 Just ex -> do
256 fp <- liftIO $ findExecutable ex
257 case fp of
258 Nothing -> userErr1 ("Cannot find executable" <+> pretty ex <+> "(for solver" <+> pretty solver <> ")")
259 Just _ -> return ()
260 case solver of
261 "cplex" -> do
262 env <- liftIO getEnvironment
263 case lookup "CPLEX_PATH" env of
264 Nothing -> userErr1 $ vcat
265 [ "Set environment variable CPLEX_PATH. Something like:"
266 , " CPLEX_PATH=/path/to/cplex/library conjure solve"
267 ]
268 Just{} -> return ()
269 _ -> return ()
270 unless (nbSolutions == "all" || all isDigit nbSolutions) $
271 userErr1 (vcat [ "The value for --number-of-solutions must either be a number or the string \"all\"."
272 , "Was given:" <+> pretty nbSolutions
273 ])
274 when (solver `elem` ["bc_minisat_all", "nbc_minisat_all", "bdd_minisat_all"] && nbSolutions /= "all") $
275 userErr1 "The solvers bc_minisat_all, nbc_minisat_all and bdd_minisat_all only work with --number-of-solutions=all"
276 essenceM_beforeNR <- readModelFromFile essence
277 essenceM <- prologue essenceM_beforeNR
278 unless (null [ () | Objective{} <- mStatements essenceM ]) $ do -- this is an optimisation problem
279 when (nbSolutions == "all" || nbSolutions /= "1") $
280 userErr1 ("Not supported for optimisation problems: --number-of-solutions=" <> pretty nbSolutions)
281 essenceParamsParsed <- forM essenceParams $ \ f -> do
282 p <- readParamOrSolutionFromFile essenceM f
283 return (f, p)
284 let givens = [ nm | Declaration (FindOrGiven Given nm _) <- mStatements essenceM ]
285 ++ [ nm | Declaration (GivenDomainDefnEnum nm) <- mStatements essenceM ]
286 when (not (null givens) && null essenceParams) $
287 userErr1 $ vcat
288 [ "The problem specification is parameterised, but no *.param files are given."
289 , "Parameters:" <+> prettyList id "," givens
290 ]
291 let isEmptyParam Model{mStatements=[]} = True
292 isEmptyParam _ = False
293 hasNonEmptyParams =
294 null essenceParams || -- either no params were given
295 all (isEmptyParam . snd) essenceParamsParsed -- or all those given were empty
296 when (null givens && not hasNonEmptyParams) $
297 userErr1 "The problem specification is _not_ parameterised, but *.param files are given."
298
299 eprimes <-
300 if not (null useExistingModels)
301 then do
302 pp logLevel "Using existing models."
303 return useExistingModels
304 else doIfNotCached -- start the show!
305 ( sort (mStatements essenceM_beforeNR)
306 , portfolio
307 -- when the following flags change, invalidate hash
308 -- nested tuples, because :(
309 , ( numberingStart
310 , smartFilenames
311 , strategyQ
312 , strategyA
313 , responses
314 )
315 , ( representations
316 , representationsFinds
317 , representationsGivens
318 , representationsAuxiliaries
319 , representationsQuantifieds
320 , representationsCuts
321 )
322 , ( channelling
323 , representationLevels
324 , seed
325 , limitModels
326 , limitTime
327 , outputFormat
328 )
329 , generateStreamliners
330 )
331 (outputDirectory </> ".conjure-checksum")
332 (pp logLevel "Using cached models." >> getEprimes)
333 conjuring
334
335 eprimesParsed <- forM eprimes $ \ f -> do
336 p1 <- liftIO $ handle (\(_ :: IOException) -> return Nothing) (Just <$> readModelInfoFromFile (outputDirectory </> f))
337 p2 <- liftIO $ handle (\(_ :: IOException) -> return Nothing) (Just <$> readModelInfoFromFile f)
338 case (p1, p2) of
339 (Just p, _) -> return (outputDirectory </> f, p)
340 (_, Just p) -> return (f, p)
341 _ -> userErr1 $ "Model not found:" <+> pretty f
342
343 msolutions <- liftIO $ savileRows eprimesParsed essenceParamsParsed
344 case msolutions of
345 Left msg -> userErr msg
346 Right solutions -> do
347
348 when (null solutions) (pp logLevel "No solutions found.")
349
350 when validateSolutionsOpt $ validating solutions
351
352 let params = nub [ dropExtension p | (_,p,_) <- solutions ]
353
354 when copySolutions $ do
355 -- clean-up: move the solutions next to the essence file.
356 -- our intention is that a user intending to just solve something
357 -- should never have to look into outputDirectory.
358
359 let
360 copySolution :: MonadIO m => FilePath -> FilePath -> m ()
361 copySolution old new = do
362 pp logLevel ("Copying solution to:" <+> pretty new)
363 liftIO (copyFile old new)
364
365 let (essenceDir0, essenceFilename) = splitFileName essence
366 let essenceDir = if essenceDir0 == "./" then "" else essenceDir0
367 let essenceBasename = takeBaseName essenceFilename
368
369 let extensions = [ ".solution", ".solution.json", ".solution.minizinc"
370 , ".solutions", ".solutions.json"
371 ]
372
373 files <- liftIO $ getAllFiles outputDirectory
374
375 unless (length eprimes == 1) $
376 pp logLevel $ "Multiple eprime models found in the output directory, not copying solutions."
377
378 when (length eprimes == 1) $ do
379 forM_ (sort files) $ \ file ->
380 forM_ extensions $ \ ext ->
381 case stripPostfix ext (snd (splitFileName file)) of
382 Nothing -> return ()
383 Just base -> do
384 let parts' = splitOn "-" base
385 let parts = case (take 1 parts', parts', last parts') of
386 ([model], _:paramparts, stripPrefix "solution" -> msolnum) ->
387 case msolnum of
388 Nothing -> [model, intercalate "-" paramparts]
389 Just{} -> [model, intercalate "-" (init paramparts), last paramparts]
390 _ -> parts'
391 case (solutionsInOneFile, null essenceParams, nbSolutions == "1", parts) of
392 -- not parameterised, but no solution numbers. must be using solutionsInOneFile.
393 (True, True, _singleSolution, [_model, ""]) ->
394 copySolution file $ essenceDir
395 </> essenceBasename
396 <.> ext
397 -- not parameterised, with solution numbers
398 (False, True, singleSolution, [_model, "", (stripPrefix "solution" -> Just solnum)]) ->
399 if singleSolution
400 then when (solnum == "000001") $ -- only copy the first solution
401 copySolution file $ essenceDir
402 </> essenceBasename
403 <.> ext
404 else copySolution file $ essenceDir
405 </> intercalate "-" [essenceBasename, solnum]
406 <.> ext
407 -- parameterised, but no solution numbers. must be using solutionsInOneFile.
408 (True, False, _singleSolution, [_model, param]) | param `elem` params ->
409 copySolution file $ essenceDir
410 </> intercalate "-" [ essenceBasename
411 , param
412 ]
413 <.> ext
414 -- parameterised, with solution numbers
415 (False, False, singleSolution, [_model, param, (stripPrefix "solution" -> Just solnum)])
416 | or [ param `elem` params
417 , or [('/' : param) `isSuffixOf` p | p <- params] ] ->
418 if singleSolution
419 then when (solnum == "000001") $ -- only copy the first solution
420 copySolution file $ essenceDir
421 </> intercalate "-" [ essenceBasename
422 , param
423 ]
424 <.> ext
425 else copySolution file $ essenceDir
426 </> intercalate "-" [ essenceBasename
427 , param
428 , solnum
429 ]
430 <.> ext
431 _ -> return () -- ignore, we don't know how to handle this file
432
433 liftIO stopGlobalPool
434
435 where
436 conjuring :: m [FilePath]
437 conjuring = do
438 pp logLevel $ "Generating models for" <+> pretty essence
439 -- remove old eprime files
440 liftIO $ getAllFilesWithSuffix ".eprime" outputDirectory >>= mapM_ removeFileIfExists
441 let modelling = let savedChoices = def
442 estimateNumberOfModels = False
443 in Modelling{..} -- construct a Modelling UI, copying all relevant fields
444 -- from the given Solve UI
445 n <- mainWithArgs_Modelling "" modelling Nothing S.empty
446 eprimes <- getEprimes
447 when (null eprimes) $ bug "Failed to generate models."
448 if S.size n == 1
449 then pp logLevel $ "Generated models:" <+> prettyList id "," eprimes
450 else pp logLevel $ "Generated" <+> pretty (S.size n) <+> "models:" <+> prettyList id "," eprimes
451 pp logLevel $ "Saved under:" <+> pretty outputDirectory
452 return [ outputDirectory </> f | f <- eprimes ]
453
454 getEprimes :: m [FilePath]
455 getEprimes = sort . filter (".eprime" `isSuffixOf`) <$> liftIO (getDirectoryContents outputDirectory)
456
457 combineResults :: [Either e [a]] -> Either e [a]
458 combineResults = fmap concat . sequence
459
460 savileRows
461 :: [(FilePath, Model)] -- models
462 -> [(FilePath, Model)] -- params
463 -> IO (Either [Doc] [(FilePath, FilePath, Maybe FilePath)])
464 savileRows eprimes params = fmap combineResults $
465 if null params
466 then autoParallel [ savileRowNoParam config m
467 | m <- eprimes
468 ]
469 else autoParallel [ savileRowWithParams config m p
470 | m <- eprimes
471 , p <- params
472 ]
473
474 -- validating :: [(FilePath, FilePath, Maybe FilePath)] -> IO ()
475 validating solutions =
476 if null essenceParams
477 then sequence_ [ validateSolutionNoParam config sol
478 | (_, _, Just sol) <- solutions ]
479 else sequence_ [ validateSolutionWithParams config sol p
480 | (_, p, Just sol) <- solutions ]
481
482
483 mainWithArgs_Modelling :: forall m .
484 MonadIO m =>
485 MonadLog m =>
486 MonadFailDoc m =>
487 EnumerateDomain m =>
488 (?typeCheckerMode :: TypeCheckerMode) =>
489 String -> -- modelNamePrefix
490 UI ->
491 Maybe Int -> -- portfolioSize for the recursive call
492 S.Set Int -> -- modelHashesBefore
493 m (S.Set Int)
494 mainWithArgs_Modelling _ mode@Modelling{..} _ modelHashesBefore | Just portfolioSize <- portfolio = do
495 pp logLevel $ "Running in portfolio mode, aiming to generate" <+> pretty portfolioSize <+> "models."
496 let
497 go modelsSoFar [] = do
498 pp logLevel $ "Done, no more levels, generated" <+> pretty (S.size modelsSoFar) <+> "models."
499 return modelsSoFar
500 go modelsSoFar (l:ls) = do
501 let nbModelsNeeded = portfolioSize - S.size modelsSoFar
502 if nbModelsNeeded <= 0
503 then return modelsSoFar
504 else do
505 modelsSoFar' <- l (Just portfolioSize) modelsSoFar
506 go modelsSoFar' ls
507
508 go modelHashesBefore
509 [ mainWithArgs_Modelling "01_compact"
510 mode { portfolio = Nothing
511 , strategyA = "c"
512 , representations = Just "c"
513 , representationsFinds = Just "c"
514 , representationsGivens = Just "s"
515 , representationsAuxiliaries = Just "c"
516 , representationsQuantifieds = Just "c"
517 , representationsCuts = Just "c"
518 , channelling = False
519 , representationLevels = True
520 , smartFilenames = True
521 }
522 , mainWithArgs_Modelling "02_compact"
523 mode { portfolio = Nothing
524 , strategyA = "c"
525 , representations = Just "c"
526 , representationsFinds = Just "c"
527 , representationsGivens = Just "c"
528 , representationsAuxiliaries = Just "c"
529 , representationsQuantifieds = Just "c"
530 , representationsCuts = Just "c"
531 , channelling = False
532 , representationLevels = True
533 , smartFilenames = True
534 }
535 , mainWithArgs_Modelling "03_sparse"
536 mode { portfolio = Nothing
537 , strategyA = "s"
538 , representations = Just "s"
539 , representationsFinds = Just "s"
540 , representationsGivens = Just "s"
541 , representationsAuxiliaries = Just "s"
542 , representationsQuantifieds = Just "s"
543 , representationsCuts = Just "s"
544 , channelling = False
545 , representationLevels = True
546 , smartFilenames = True
547 }
548 , mainWithArgs_Modelling "04_nochPrunedLevels"
549 mode { portfolio = Nothing
550 , strategyA = "x"
551 , representations = Just "x"
552 , representationsFinds = Just "x"
553 , representationsGivens = Just "s"
554 , representationsAuxiliaries = Just "c"
555 , representationsQuantifieds = Just "c"
556 , representationsCuts = Just "c"
557 , channelling = False
558 , representationLevels = True
559 , smartFilenames = True
560 }
561 , mainWithArgs_Modelling "05_nochAllLevels"
562 mode { portfolio = Nothing
563 , strategyA = "x"
564 , representations = Just "x"
565 , representationsFinds = Just "x"
566 , representationsGivens = Just "s"
567 , representationsAuxiliaries = Just "c"
568 , representationsQuantifieds = Just "c"
569 , representationsCuts = Just "c"
570 , channelling = False
571 , representationLevels = False
572 , smartFilenames = True
573 }
574 , mainWithArgs_Modelling "06_chPrunedLevels"
575 mode { portfolio = Nothing
576 , strategyA = "x"
577 , representations = Just "x"
578 , representationsFinds = Just "x"
579 , representationsGivens = Just "s"
580 , representationsAuxiliaries = Just "c"
581 , representationsQuantifieds = Just "c"
582 , representationsCuts = Just "c"
583 , channelling = True
584 , representationLevels = True
585 , smartFilenames = True
586 }
587 , mainWithArgs_Modelling "07_chAllLevels"
588 mode { portfolio = Nothing
589 , strategyA = "x"
590 , representations = Just "x"
591 , representationsFinds = Just "x"
592 , representationsGivens = Just "s"
593 , representationsAuxiliaries = Just "c"
594 , representationsQuantifieds = Just "c"
595 , representationsCuts = Just "c"
596 , channelling = True
597 , representationLevels = False
598 , smartFilenames = True
599 }
600 , mainWithArgs_Modelling "08_fullPrunedLevels"
601 mode { portfolio = Nothing
602 , strategyA = "x"
603 , representations = Just "x"
604 , representationsFinds = Just "x"
605 , representationsGivens = Just "s"
606 , representationsAuxiliaries = Just "x"
607 , representationsQuantifieds = Just "x"
608 , representationsCuts = Just "x"
609 , channelling = True
610 , representationLevels = True
611 , smartFilenames = True
612 }
613 , mainWithArgs_Modelling "09_fullAllLevels"
614 mode { portfolio = Nothing
615 , strategyA = "x"
616 , representations = Just "x"
617 , representationsFinds = Just "x"
618 , representationsGivens = Just "s"
619 , representationsAuxiliaries = Just "x"
620 , representationsQuantifieds = Just "x"
621 , representationsCuts = Just "x"
622 , channelling = True
623 , representationLevels = False
624 , smartFilenames = True
625 }
626 , mainWithArgs_Modelling "10_fullParamsPrunedLevels"
627 mode { portfolio = Nothing
628 , strategyA = "x"
629 , representations = Just "x"
630 , representationsFinds = Just "x"
631 , representationsGivens = Just "x"
632 , representationsAuxiliaries = Just "x"
633 , representationsQuantifieds = Just "x"
634 , representationsCuts = Just "x"
635 , channelling = True
636 , representationLevels = True
637 , smartFilenames = True
638 }
639 , mainWithArgs_Modelling "11_fullParamsAllLevels"
640 mode { portfolio = Nothing
641 , strategyA = "x"
642 , representations = Just "x"
643 , representationsFinds = Just "x"
644 , representationsGivens = Just "x"
645 , representationsAuxiliaries = Just "x"
646 , representationsQuantifieds = Just "x"
647 , representationsCuts = Just "x"
648 , channelling = True
649 , representationLevels = False
650 , smartFilenames = True
651 }
652 ]
653 mainWithArgs_Modelling "" mode portfolioSize modelHashesBefore =
654 mainWithArgs_Modelling "model" mode portfolioSize modelHashesBefore
655 mainWithArgs_Modelling modelNamePrefix mode@Modelling{..} portfolioSize modelHashesBefore | strategyA == "c" && channelling == True =
656 mainWithArgs_Modelling modelNamePrefix mode{channelling=False} portfolioSize modelHashesBefore
657 mainWithArgs_Modelling modelNamePrefix Modelling{..} portfolioSize modelHashesBefore = do
658 unless (modelNamePrefix == "model") $
659 pp logLevel $ "Portfolio level:" <+> pretty modelNamePrefix
660 let
661 parseStrategy_ s = maybe (userErr1 ("Not a valid strategy:" <+> pretty s))
662 return
663 (parseStrategy s)
664
665 getConfig = do
666 strategyQ' <- parseStrategy_ strategyQ
667 strategyA' <- parseStrategy_ strategyA
668 representations' <- maybe (return strategyA') parseStrategy_ representations
669 representationsFinds' <- maybe (return representations') parseStrategy_ representationsFinds
670 representationsGivens' <- maybe (return Sparse ) parseStrategy_ representationsGivens
671 representationsAuxiliaries' <- maybe (return representations') parseStrategy_ representationsAuxiliaries
672 representationsQuantifieds' <- maybe (return representations') parseStrategy_ representationsQuantifieds
673 representationsCuts' <- maybe (return representations') parseStrategy_ representationsCuts
674
675 case fst (viewAuto strategyQ') of
676 Compact -> userErr1 "The Compact heuristic isn't supported for questions."
677 _ -> return ()
678
679 let
680 parseCommaSeparated :: Read a => Doc -> String -> m (Maybe [a])
681 parseCommaSeparated flag str =
682 if null str
683 then return Nothing
684 else do
685 let parts = splitOn "," str
686 let intParts = mapMaybe readMay parts
687 if length parts == length intParts
688 then return (Just intParts)
689 else userErr1 $ vcat [ "Cannot parse the value for" <+> flag
690 , "Expected a comma separated list of integers."
691 , "But got:" <+> pretty str
692 ]
693
694 responsesList <- parseCommaSeparated "--responses" responses
695 generateStreamlinersList <- parseCommaSeparated "--generate-streamliners" generateStreamliners
696
697 responsesRepresentationList <- do
698 if null responsesRepresentation
699 then return Nothing
700 else do
701 let parts =
702 [ case splitOn ":" pair of
703 [nm, val] ->
704 case readMay val of
705 Just i -> Just (Name (stringToText nm), i)
706 Nothing -> Nothing
707 _ -> Nothing
708 | pair <- splitOn "," responsesRepresentation
709 ]
710 let partsJust = catMaybes parts
711 if length parts == length partsJust
712 then return (Just partsJust)
713 else userErr1 $ vcat [ "Cannot parse the value for --responses-representation."
714 , "Expected a comma separated list of variable name : integer pairs."
715 , "But got:" <+> pretty responsesRepresentation
716 ]
717
718 trail <- if (followModel /= "")
719 then miTrailGeneralised . mInfo <$> readModelInfoFromFile followModel
720 else return []
721
722 return Config.Config
723 { Config.outputDirectory = outputDirectory
724 , Config.logLevel = logLevel
725 , Config.verboseTrail = verboseTrail
726 , Config.rewritesTrail = rewritesTrail
727 , Config.logRuleFails = logRuleFails
728 , Config.logRuleSuccesses = logRuleSuccesses
729 , Config.logRuleAttempts = logRuleAttempts
730 , Config.logChoices = logChoices
731 , Config.followTrail = M.fromList trail
732 , Config.strategyQ = strategyQ'
733 , Config.strategyA = strategyA'
734 , Config.representations = representations'
735 , Config.representationsFinds = representationsFinds'
736 , Config.representationsGivens = representationsGivens'
737 , Config.representationsAuxiliaries = representationsAuxiliaries'
738 , Config.representationsQuantifieds = representationsQuantifieds'
739 , Config.representationsCuts = representationsCuts'
740 , Config.channelling = channelling
741 , Config.representationLevels = representationLevels
742 , Config.limitModels = if limitModels == Just 0 then Nothing else limitModels
743 , Config.numberingStart = numberingStart
744 , Config.smartFilenames = smartFilenames
745 , Config.lineWidth = lineWidth
746 , Config.responses = responsesList
747 , Config.responsesRepresentation = responsesRepresentationList
748 , Config.generateStreamliners = generateStreamlinersList
749 , Config.estimateNumberOfModels = estimateNumberOfModels
750 }
751
752 essenceM <- readModelFromFile essence
753 liftIO $ hSetBuffering stdout LineBuffering
754 liftIO $ maybe (return ()) setRandomSeed seed
755 config <- getConfig
756 runNameGen essenceM $ do
757 modelWithStreamliners <-
758 case Config.generateStreamliners config of
759 Nothing -> return essenceM
760 Just ix -> do
761 streamliners <- pure essenceM >>= resolveNames >>= typeCheckModel >>= streamlining
762 let chosen = [ streamliner | (i, streamliner) <- zip [1..] streamliners, i `elem` ix ]
763 return essenceM { mStatements = mStatements essenceM ++ [SuchThat [x | (_, (x, _)) <- chosen]] }
764 outputModels portfolioSize modelHashesBefore modelNamePrefix config modelWithStreamliners
765 mainWithArgs_Modelling _ _ _ _ = bug "mainWithArgs_Modelling"
766
767 pp :: MonadIO m => LogLevel -> Doc -> m ()
768 pp LogNone = const $ return ()
769 pp _ = liftIO . putStrLn . renderNormal
770
771
772 savilerowScriptName :: FilePath
773 savilerowScriptName
774 | os `elem` ["darwin", "linux"] = "savilerow"
775 | os `elem` ["mingw32"] = "savilerow.bat"
776 | otherwise = bug "Cannot detect operating system."
777
778
779 quoteMultiWord :: String -> String
780 quoteMultiWord s
781 | ' ' `elem` s = "\"" ++ s ++ "\""
782 | otherwise = s
783
784
785 savileRowNoParam ::
786 (?typeCheckerMode :: TypeCheckerMode) =>
787 UI ->
788 (FilePath, Model) -> -- model
789 IO (Either
790 [Doc] -- user error
791 [ ( FilePath -- model
792 , FilePath -- param
793 , Maybe FilePath -- solution, Nothing if solutionsInOneFile=True
794 ) ])
795 savileRowNoParam ui@Solve{..} (modelPath, eprimeModel) = sh $ errExit False $ do
796 pp logLevel $ hsep ["Savile Row:", pretty modelPath]
797 let outBase = (dropExtension . snd . splitFileName) modelPath
798 srArgs <- liftIO $ srMkArgs ui outBase modelPath
799 let tr = translateSolution eprimeModel def
800 let handler = liftIO . srStdoutHandler
801 (outBase, modelPath, "<no param file>", ui)
802 tr (1::Int)
803 let runsolverArgs = maybe [] (\ limit -> ["-C", show limit]) runsolverCPUTimeLimit ++
804 maybe [] (\ limit -> ["-W", show limit]) runsolverWallTimeLimit ++
805 maybe [] (\ limit -> ["-R", show limit]) runsolverMemoryLimit ++
806 ["--quiet", "-v", outputDirectory </> outBase ++ ".runsolver-info"]
807 (stdoutSR, solutions) <- partitionEithers <$>
808 case (runsolverCPUTimeLimit, runsolverWallTimeLimit, runsolverMemoryLimit) of
809 (Nothing, Nothing, Nothing) -> do
810 when (logLevel >= LogDebug) $ do
811 liftIO $ putStrLn "Using the following options for Savile Row:"
812 liftIO $ putStrLn $ " savilerow " ++ unwords (map (quoteMultiWord . textToString) srArgs)
813 runHandle savilerowScriptName srArgs handler
814 _ ->
815 if os /= "linux"
816 then return [Left "runsolver is only supported on linux"]
817 else do
818 when (logLevel >= LogDebug) $ do
819 liftIO $ putStrLn "Using the following options for Savile Row:"
820 liftIO $ putStrLn $ " runsolver " ++ unwords (map quoteMultiWord runsolverArgs)
821 ++ " savilerow " ++ unwords (map (quoteMultiWord . textToString) srArgs)
822 runHandle "runsolver" (map stringToText runsolverArgs ++ [stringToText savilerowScriptName] ++ srArgs) handler
823 srCleanUp outBase ui (stringToText $ unlines stdoutSR) solutions
824 savileRowNoParam _ _ = bug "savileRowNoParam"
825
826
827 savileRowWithParams ::
828 (?typeCheckerMode :: TypeCheckerMode) =>
829 UI ->
830 (FilePath, Model) -> -- model
831 (FilePath, Model) -> -- param
832 IO (Either
833 [Doc] -- user error
834 [ ( FilePath -- model
835 , FilePath -- param
836 , Maybe FilePath -- solution, Nothing if solutionsInOneFile=True
837 ) ])
838 savileRowWithParams ui@Solve{..} (modelPath, eprimeModel) (paramPath, essenceParam) = sh $ errExit False $ do
839 pp logLevel $ hsep ["Savile Row:", pretty modelPath, pretty paramPath]
840 let outBase = (dropExtension . snd . splitFileName) modelPath ++ "-" ++ dropDirs (dropExtension paramPath)
841 let
842 -- this is a bit tricky.
843 -- we want to preserve user-erors, and not raise them as errors using IO.fail
844 runTranslateParameter :: IO (Either [Doc] Model)
845 runTranslateParameter = runUserErrorT $ ignoreLogs $ runNameGen () $
846 translateParameter graphSolver eprimeModel essenceParam
847 eprimeParam' <- liftIO runTranslateParameter
848 case eprimeParam' of
849 Left err -> return (Left err)
850 Right eprimeParam -> do
851 liftIO $ writeFile (outputDirectory </> outBase ++ ".eprime-param") (render lineWidth eprimeParam)
852 srArgsBase <- liftIO $ srMkArgs ui outBase modelPath
853 let srArgs = "-in-param"
854 : stringToText (outputDirectory </> outBase ++ ".eprime-param")
855 : srArgsBase
856 let tr = translateSolution eprimeModel essenceParam
857 let handler = liftIO . srStdoutHandler
858 (outBase, modelPath, paramPath, ui)
859 tr (1::Int)
860 let runsolverArgs = maybe [] (\ limit -> ["-C", show limit]) runsolverCPUTimeLimit ++
861 maybe [] (\ limit -> ["-W", show limit]) runsolverWallTimeLimit ++
862 maybe [] (\ limit -> ["-R", show limit]) runsolverMemoryLimit ++
863 ["--quiet", "-v", outputDirectory </> outBase ++ ".runsolver-info"]
864 (stdoutSR, solutions) <- partitionEithers <$>
865 case (runsolverCPUTimeLimit, runsolverWallTimeLimit, runsolverMemoryLimit) of
866 (Nothing, Nothing, Nothing) -> do
867 when (logLevel >= LogDebug) $ do
868 liftIO $ putStrLn "Using the following options for Savile Row:"
869 liftIO $ putStrLn $ " savilerow " ++ unwords (map (quoteMultiWord . textToString) srArgs)
870 runHandle savilerowScriptName srArgs handler
871 _ ->
872 if os /= "linux"
873 then return [Left "runsolver is only supported on linux"]
874 else do
875 when (logLevel >= LogDebug) $ do
876 liftIO $ putStrLn "Using the following options for Savile Row:"
877 liftIO $ putStrLn $ " runsolver " ++ unwords (map quoteMultiWord runsolverArgs)
878 ++ " savilerow " ++ unwords (map (quoteMultiWord . textToString) srArgs)
879 runHandle "runsolver" (map stringToText runsolverArgs ++ [stringToText savilerowScriptName] ++ srArgs) handler
880
881 srCleanUp outBase ui (stringToText $ unlines stdoutSR) solutions
882 savileRowWithParams _ _ _ = bug "savileRowWithParams"
883
884
885
886 solverExecutables :: [(String, String)]
887 solverExecutables =
888 [ ( "minion" , "minion" )
889 , ( "gecode" , "fzn-gecode" )
890 , ( "chuffed" , "fzn-chuffed" )
891 , ( "cadical" , "cadical" )
892 , ( "kissat" , "kissat" )
893 , ( "glucose" , "glucose" )
894 , ( "glucose-syrup" , "glucose-syrup" )
895 , ( "minisat" , "minisat" )
896 , ( "bc_minisat_all" , "bc_minisat_all_release" )
897 , ( "nbc_minisat_all" , "nbc_minisat_all_release" )
898 , ( "bdd_minisat_all" , "bdd_minisat_all_release" )
899 , ( "wmaxcdcl" , "wmaxcdcl" )
900 , ( "or-tools" , "fzn-cp-sat" )
901 , ( "coin-or" , "minizinc" )
902 , ( "cplex" , "minizinc" )
903 , ( "yices" , "yices-smt2" )
904 , ( "boolector" , "boolector" )
905 , ( "z3" , "z3" )
906 ]
907
908
909 smtSolvers :: [String]
910 smtSolvers = ["boolector", "yices", "z3"]
911
912 smtSolversSRFlag :: String -> String
913 smtSolversSRFlag "boolector" = "-boolector"
914 smtSolversSRFlag "yices" = "-yices2"
915 smtSolversSRFlag "z3" = "-z3"
916 smtSolversSRFlag _ = bug "smtSolversSRFlag"
917
918 smtSupportedLogics :: String -> [String]
919 smtSupportedLogics "boolector" = ["bv"]
920 smtSupportedLogics "yices" = ["bv", "lia", "idl"]
921 smtSupportedLogics "z3" = ["bv", "lia", "nia"]
922 smtSupportedLogics s = bug ("Unrecognised SMT solver:" <+> pretty s)
923
924
925 splitSolverName :: MonadUserError m => String -> m (String, String)
926 splitSolverName solver = do
927 let
928
929 (solverName, smtLogicName) <-
930 case splitOn "-" solver of
931 [solverName] | solverName `elem` smtSolvers -> return (solverName, "bv")
932 [solverName , logic] | solverName `elem` smtSolvers -> do
933 unless (logic `elem` smtSupportedLogics solverName) $
934 userErr1 $ vcat [ "SMT logic not supported by Savile Row:" <+> pretty logic
935 , "Supported logics:" <+> prettyList id "," (smtSupportedLogics solverName)
936 ]
937 return (solverName, logic)
938 _ -> return (solver, "") -- not an smt solver
939 return (solverName, smtLogicName)
940
941
942 srMkArgs :: UI -> FilePath -> FilePath -> IO [Text]
943 srMkArgs Solve{..} outBase modelPath = do
944 let genericOpts =
945 [ "-in-eprime" , stringToText modelPath
946 , "-out-minion" , stringToText $ outputDirectory </> outBase ++ ".eprime-minion"
947 , "-out-sat" , stringToText $ outputDirectory </> outBase ++ ".eprime-dimacs"
948 , "-out-smt" , stringToText $ outputDirectory </> outBase ++ ".eprime-smt"
949 , "-out-aux" , stringToText $ outputDirectory </> outBase ++ ".eprime-aux"
950 , "-out-info" , stringToText $ outputDirectory </> outBase ++ ".eprime-info"
951 , "-out-minizinc" , stringToText $ outputDirectory </> outBase ++ ".eprime.mzn"
952 , "-run-solver"
953 , "-S0"
954 , "-solutions-to-stdout-one-line"
955 ] ++
956 [ "-cgroups" | cgroups ] ++
957 ( if nbSolutions == "all"
958 then ["-all-solutions"]
959 else ["-num-solutions", stringToText nbSolutions]
960 )
961 (solverName, smtLogicName) <- splitSolverName solver
962 solverSelection <- case solverName of
963 "minion" -> return [ "-minion" ]
964 "gecode" -> return [ "-gecode" ]
965 "chuffed" -> return [ "-chuffed"]
966 "or-tools" -> return [ "-or-tools"]
967 "glucose" -> return [ "-sat"
968 , "-sat-family", "glucose"
969 , "-satsolver-bin", "glucose"
970 ]
971 "glucose-syrup" -> return [ "-sat"
972 , "-sat-family", "glucose"
973 , "-satsolver-bin", "glucose-syrup"
974 ]
975 "cadical" -> return [ "-sat"
976 , "-sat-family", "cadical"
977 , "-satsolver-bin", "cadical"
978 ]
979 "kissat" -> return [ "-sat"
980 , "-sat-family", "cadical"
981 , "-satsolver-bin", "kissat"
982 ]
983 "minisat" -> return [ "-sat"
984 , "-sat-family", "minisat"
985 , "-satsolver-bin", "minisat"
986 ]
987 "bc_minisat_all" -> return [ "-sat"
988 , "-sat-family", "nbc_minisat_all"
989 , "-satsolver-bin", "bc_minisat_all_release"
990 ]
991 "nbc_minisat_all" -> return [ "-sat"
992 , "-sat-family", "nbc_minisat_all"
993 , "-satsolver-bin", "nbc_minisat_all_release"
994 ]
995 "bdd_minisat_all" -> return [ "-sat"
996 , "-sat-family", "nbc_minisat_all"
997 , "-satsolver-bin", "bdd_minisat_all_release"
998 ]
999 "wmaxcdcl" -> return [ "-maxsat"
1000 , "-satsolver-bin", "wmaxcdcl"
1001 ]
1002 "coin-or" -> return [ "-minizinc"
1003 , "-solver-options", "--solver COIN-BC"
1004 ]
1005 "cplex" -> do
1006 env <- getEnvironment
1007 case lookup "CPLEX_PATH" env of
1008 Nothing -> userErr1 $ vcat
1009 [ "Set environment variable CPLEX_PATH. Something like:"
1010 , " CPLEX_PATH=/path/to/cplex/library conjure solve"
1011 ]
1012 Just cplex_path ->
1013 return [ "-minizinc"
1014 , "-solver-options", stringToText ("--solver CPLEX --cplex-dll " ++ cplex_path)
1015 ]
1016 _ | solverName `elem` smtSolvers
1017 -> return [ "-smt"
1018 , "-smt-nested" -- alternative is -smt-flat
1019 , stringToText ("-smt-" ++ smtLogicName)
1020 , "-smtsolver-bin"
1021 , case lookup solverName solverExecutables of
1022 Nothing -> bug ("solverExecutables" <+> pretty solverName)
1023 Just ex -> stringToText ex
1024 , stringToText (smtSolversSRFlag solverName)
1025 ]
1026 _ -> userErr1 ("Unknown solver:" <+> pretty solver)
1027
1028 return $ genericOpts
1029 ++ solverSelection
1030 ++ map stringToText (concatMap words savilerowOptions)
1031 ++ if null solverOptions
1032 then []
1033 else [ "-solver-options"
1034 , stringToText (unwords (concatMap words solverOptions))
1035 ]
1036 srMkArgs _ _ _ = bug "srMkArgs"
1037
1038
1039 srStdoutHandler ::
1040 (FilePath, FilePath, FilePath, UI) ->
1041 (Model -> NameGenM (IdentityT IO) Model) ->
1042 Int ->
1043 Handle ->
1044 IO [Either String (FilePath, FilePath, Maybe FilePath)]
1045 srStdoutHandler
1046 args@(outBase , modelPath, paramPath , Solve{..})
1047 tr solutionNumber h = do
1048 eof <- hIsEOF h
1049 if eof
1050 then do
1051 hClose h
1052 return []
1053 else do
1054 line <- hGetLine h
1055 when (logLevel >= LogDebug) $ do
1056 pp logLevel ("SR:" <+> pretty line)
1057 case stripPrefix "Solution: " line of
1058 Nothing ->
1059 if line `elem` ["MaxSAT solver exited with error code:3 and error message:", "[PARSE ERROR! Unexpected char: h]"]
1060 then srStdoutHandler args tr solutionNumber h -- wmaxcdcl produces this warning if it proves optimality...
1061 else do
1062 if isPrefixOf "Created output file for domain filtering" line
1063 then pp logLevel $ hsep ["Running minion for domain filtering."]
1064 else if isPrefixOf "Created output" line
1065 then pp logLevel $ hsep ["Running solver:", pretty solver]
1066 else return ()
1067 fmap (Left line :)
1068 (srStdoutHandler args tr solutionNumber h)
1069 Just solutionText -> do
1070 eprimeSol <- readModel ParserC.parseModel (Just id) ("<memory>", stringToText solutionText)
1071 essenceSol <- ignoreLogs $ runNameGen () $ tr eprimeSol
1072 case solutionsInOneFile of
1073 False -> do
1074 let mkFilename ext = outputDirectory </> outBase
1075 ++ "-solution" ++ padLeft 6 '0' (show solutionNumber)
1076 ++ ext
1077 let filenameEprimeSol = mkFilename ".eprime-solution"
1078 let filenameEssenceSol = mkFilename ".solution"
1079 writeModel lineWidth Plain (Just filenameEprimeSol) eprimeSol
1080 writeModel lineWidth Plain (Just filenameEssenceSol) essenceSol
1081 case outputFormat of
1082 JSON -> writeModel lineWidth outputFormat (Just (filenameEssenceSol ++ ".json")) essenceSol
1083 JSONStream -> writeModel 0 outputFormat (Just (filenameEssenceSol ++ ".json")) essenceSol
1084 _ -> return ()
1085 when (outputFormat == MiniZinc) $
1086 writeModel lineWidth outputFormat (Just (filenameEssenceSol ++ ".minizinc")) essenceSol
1087 fmap (Right (modelPath, paramPath, Just filenameEssenceSol) :)
1088 (srStdoutHandler args tr (solutionNumber+1) h)
1089 True -> do
1090 let mkFilename ext = outputDirectory </> outBase
1091 ++ ext
1092 let filenameEprimeSol = mkFilename ".eprime-solutions"
1093 let filenameEssenceSol = mkFilename ".solutions"
1094 let filenameEssenceSolJSON = mkFilename ".solutions.json"
1095 -- remove the solutions files before writing the first solution
1096 if solutionNumber == 1
1097 then do
1098 removeFileIfExists filenameEprimeSol
1099 removeFileIfExists filenameEssenceSol
1100 removeFileIfExists filenameEssenceSolJSON
1101 case outputFormat of
1102 JSON -> writeFile filenameEssenceSolJSON "[\n"
1103 _ -> return ()
1104 else
1105 case outputFormat of
1106 JSON -> appendFile filenameEssenceSolJSON ",\n"
1107 _ -> return ()
1108 appendFile filenameEprimeSol ("$ Solution: " ++ padLeft 6 '0' (show solutionNumber) ++ "\n")
1109 appendFile filenameEprimeSol (render lineWidth eprimeSol ++ "\n\n")
1110 appendFile filenameEssenceSol ("$ Solution: " ++ padLeft 6 '0' (show solutionNumber) ++ "\n")
1111 appendFile filenameEssenceSol (render lineWidth essenceSol ++ "\n\n")
1112 when (outputFormat `elem` [JSON, JSONStream]) $ do
1113 essenceSol' <- toSimpleJSON essenceSol
1114 appendFile filenameEssenceSolJSON (render lineWidth essenceSol')
1115 appendFile filenameEssenceSolJSON ("\n")
1116 fmap (Right (modelPath, paramPath, Nothing) :)
1117 (srStdoutHandler args tr (solutionNumber+1) h)
1118 srStdoutHandler _ _ _ _ = bug "srStdoutHandler"
1119
1120
1121 srCleanUp :: FilePath -> UI -> Text -> [sols] -> Sh (Either [Doc] [sols])
1122 srCleanUp outBase ui@Solve{..} stdoutSR solutions = do
1123
1124 let mkFilename ext = outputDirectory </> outBase ++ ext
1125
1126 -- closing the array in the all solutions json file
1127 case outputFormat of
1128 JSON -> case solutionsInOneFile of
1129 False -> return ()
1130 True -> do
1131 let filenameEssenceSolJSON = mkFilename ".solutions.json"
1132 case solutions of
1133 [] -> liftIO $ writeFile filenameEssenceSolJSON "[]\n"
1134 _ -> liftIO $ appendFile filenameEssenceSolJSON "]\n"
1135 _ -> return ()
1136
1137 stderrSR <- lastStderr
1138 exitCodeSR <- lastExitCode
1139 let combinedSR = T.unlines [stdoutSR, stderrSR]
1140
1141 liftIO $ do
1142 let savilerowInfoFilename = mkFilename ".eprime-info"
1143 let runsolverInfoFilename = mkFilename ".runsolver-info"
1144 let statsFilename = mkFilename ".stats.json"
1145 savilerowInfoContent <- liftIO $ readFileIfExists savilerowInfoFilename
1146 runsolverInfoContent <- liftIO $ readFileIfExists runsolverInfoFilename
1147 stats <- mkSolveStats ui (exitCodeSR, stdoutSR, stderrSR) (fromMaybe "" savilerowInfoContent) (fromMaybe "" runsolverInfoContent)
1148 writeFile statsFilename (render lineWidth (toJSON stats))
1149
1150 if | T.isInfixOf "Savile Row timed out." combinedSR ->
1151 return (Left ["Savile Row timed out."])
1152 | T.isInfixOf "where false" combinedSR ->
1153 return (Left [vcat [ "Invalid instance, a where statement evaluated to false."
1154 , "(It can be an implicit where statement added by Conjure.)"
1155 ]])
1156 | or [ T.isInfixOf "Exception in thread" combinedSR
1157 , T.isInfixOf "ERROR" combinedSR
1158 , T.isInfixOf "Sub-process exited with error code" combinedSR
1159 ] ->
1160 return (Left [vcat [ "Savile Row stdout:" <+> pretty stdoutSR
1161 , "Savile Row stderr:" <+> pretty stderrSR
1162 , "Savile Row exit-code:" <+> pretty exitCodeSR
1163 ]])
1164 | exitCodeSR == 0 -> return (Right solutions)
1165 | otherwise ->
1166 return (Left [vcat [ "Savile Row stdout:" <+> pretty stdoutSR
1167 , "Savile Row stderr:" <+> pretty stderrSR
1168 , "Savile Row exit-code:" <+> pretty exitCodeSR
1169 ]])
1170 srCleanUp _ _ _ _ = bug "srCleanUp"
1171
1172
1173 validateSolutionNoParam ::
1174 MonadIO m =>
1175 MonadLog m =>
1176 MonadFailDoc m =>
1177 EnumerateDomain m =>
1178 (?typeCheckerMode :: TypeCheckerMode) =>
1179 UI -> FilePath -> m ()
1180 validateSolutionNoParam Solve{..} solutionPath = do
1181 pp logLevel $ hsep ["Validating solution:", pretty solutionPath]
1182 essenceM <- readModelFromFile essence
1183 solution <- readParamOrSolutionFromFile essenceM solutionPath
1184 [essenceM2, solution2] <- ignoreLogs $ runNameGen () $ resolveNamesMulti [essenceM, solution]
1185 failToUserError $ ignoreLogs $ runNameGen () $ validateSolution essenceM2 def solution2
1186 validateSolutionNoParam _ _ = bug "validateSolutionNoParam"
1187
1188
1189 validateSolutionWithParams ::
1190 MonadIO m =>
1191 MonadLog m =>
1192 MonadFailDoc m =>
1193 EnumerateDomain m =>
1194 (?typeCheckerMode :: TypeCheckerMode) =>
1195 UI -> FilePath -> FilePath -> m ()
1196 validateSolutionWithParams Solve{..} solutionPath paramPath = do
1197 pp logLevel $ hsep ["Validating solution:", pretty paramPath, pretty solutionPath]
1198 essenceM <- readModelFromFile essence
1199 param <- readParamOrSolutionFromFile essenceM paramPath
1200 solution <- readParamOrSolutionFromFile essenceM solutionPath
1201 [essenceM2, param2, solution2] <- ignoreLogs $ runNameGen () $ resolveNamesMulti [essenceM, param, solution]
1202 failToUserError $ ignoreLogs $ runNameGen () $ validateSolution essenceM2 param2 solution2
1203 validateSolutionWithParams _ _ _ = bug "validateSolutionWithParams"
1204
1205
1206 doIfNotCached
1207 :: (MonadIO m, Hashable h)
1208 => h -- thing to hash
1209 -> FilePath -- saved hashes file
1210 -> m a -- the result from cache
1211 -> m a -- the action
1212 -> m a -- the results and writing the new hashes in the file
1213 doIfNotCached (show . hash -> h) savedHashesFile getResult act = do
1214 savedHashes <- liftIO $ readFileIfExists savedHashesFile
1215 let skip = Just h == savedHashes -- skip if h was the hash in the file
1216 if skip
1217 then getResult
1218 else do
1219 res <- act
1220 liftIO $ writeFile savedHashesFile h
1221 return res
1222
1223
1224 autoParallel :: [IO a] -> IO [a]
1225 autoParallel = if numCapabilities > 1 then parallel else sequence
1226