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