Skip to content

Commit

Permalink
adding two flags to conjure-solve
Browse files Browse the repository at this point in the history 
* `--number-of-solutions` so we don't need to pass -all-solutions or -num-solutions n to SR.
* `--copy-solutions` so there is a way to stop conjure-solve from copying the solutions next to the Essence file. this is still on by default.
  • Loading branch information
@ozgurakgun
ozgurakgun committed Jun 1, 2016
1 parent d6d7834 commit fcbc44b
Show file tree
Hide file tree
Showing 4 changed files with 83 additions and 50 deletions.
3 changes: 2 additions & 1 deletion src/Conjure/Process/Enumerate.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -122,12 +122,13 @@ enumerateDomain d = liftIO' $ withSystemTempDirectory ("conjure-enumerateDomain-
[ "-O0"
, "-preprocess" , "None"
, "-timelimit" , show savilerowTimelimit
, "-num-solutions" , show enumerateDomainMax
]
, solverOptions = unwords
[ "-cpulimit" , show minionTimelimit
]
, solver = "minion"
, nbSolutions = show enumerateDomainMax
, copySolutions = False
, logLevel = LogNone
-- default values for the rest
, essenceParams = []
Expand Down
19 changes: 18 additions & 1 deletion src/Conjure/UI.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -114,6 +114,8 @@ data UI
, savilerowOptions :: String
, solverOptions :: String
, solver :: String
, nbSolutions :: String -- a number, or "all". by default 1
, copySolutions :: Bool
-- output
, outputFormat :: OutputFormat -- Essence by default
, lineWidth :: Int -- 120 by default
Expand Down Expand Up @@ -777,7 +779,7 @@ ui = modes
&= groupname "Options for other tools"
&= explicit
&= help "Options to be passed to Savile Row.\n\
\By default: '-O2'"
\Default: '-O2'"
, solverOptions
= def
&= name "solver-options"
Expand All @@ -792,6 +794,21 @@ ui = modes
&= help "Backend solver to use.\n\
\Possible values: minion/lingeling/minisat\n\
\Default: minion"
, nbSolutions
= "1"
&= name "number-of-solutions"
&= groupname "General"
&= explicit
&= help "Number of solutions to find.\n\
\Pass the string \"all\" to enumerate all solutions.\n\
\Default: 1"
, copySolutions
= True
&= name "copy-solutions"
&= groupname "General"
&= explicit
&= help "Whether to place a copy of solution(s) next to the Essence file or not.\n\
\Default: on"
, outputFormat
= def
&= name "output-format"
Expand Down
104 changes: 57 additions & 47 deletions src/Conjure/UI/MainHelper.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@ import Conjure.Language.NameResolution ( resolveNamesMulti )
-- base
import System.IO ( Handle, hSetBuffering, stdout, BufferMode(..) )
import GHC.IO.Handle ( hIsEOF, hClose, hGetLine )
import Data.Char ( isDigit )

-- filepath
import System.FilePath ( splitFileName, takeBaseName, (<.>) )
Expand Down Expand Up @@ -154,6 +155,10 @@ mainWithArgs config@Solve{..} = do
-- some sanity checks
unless (solver `elem` ["minion", "lingeling", "minisat"]) $
userErr1 ("Unsupported solver:" <+> pretty solver)
unless (nbSolutions == "all" || all isDigit nbSolutions) $
userErr1 (vcat [ "The value for --number-of-solutions must either be a number or the string \"all\"."
, "Was given:" <+> pretty nbSolutions
])
essenceM <- readModelFromFile essence
essenceParamsParsed <- forM essenceParams $ \ f -> do
p <- readModelFromFile f
Expand Down Expand Up @@ -229,53 +234,54 @@ mainWithArgs config@Solve{..} = do
Left msg -> userErr msg
Right solutions -> do
when validateSolutionsOpt $ liftIO $ validating solutions
-- clean-up: move the solutions next to the essence file.
-- our intention is that a user intending to just solve something
-- should never have to look into outputDirectory.
let
copySolution :: MonadIO m => FilePath -> FilePath -> m ()
copySolution old new = do
pp logLevel ("Copying solution to:" <+> pretty new)
liftIO (copyFile old new)
let (essenceDir, essenceFilename) = splitFileName essence
let essenceBasename = takeBaseName essenceFilename
when (length eprimes == 1) $
if null essenceParams
then do
let solutions' = [ solution
| (_, _, solution) <- solutions ]
case solutions' of
[solution] ->
copySolution solution (essenceDir
</> intercalate "-" [ essenceBasename
]
<.> ".solution")
_ -> forM_ (zip allNats solutions') $ \ (i, solution) ->
copySolution solution (essenceDir
</> intercalate "-" [ essenceBasename
, paddedNum 6 '0' i
]
<.> ".solution")
else forM_ essenceParams $ \ essenceParam -> do
let (_paramDir, paramFilename) = splitFileName essenceParam
let paramBasename = takeBaseName paramFilename
let solutions' = [ solution
| (_, essenceParam', solution) <- solutions
, essenceParam == essenceParam' ]
case solutions' of
[solution] ->
copySolution solution (essenceDir
</> intercalate "-" [ essenceBasename
, paramBasename
]
<.> ".solution")
_ -> forM_ (zip allNats solutions') $ \ (i, solution) ->
copySolution solution (essenceDir
</> intercalate "-" [ essenceBasename
, paramBasename
, paddedNum 6 '0' i
]
<.> ".solution")
when copySolutions $ do
-- clean-up: move the solutions next to the essence file.
-- our intention is that a user intending to just solve something
-- should never have to look into outputDirectory.
let
copySolution :: MonadIO m => FilePath -> FilePath -> m ()
copySolution old new = do
pp logLevel ("Copying solution to:" <+> pretty new)
liftIO (copyFile old new)
let (essenceDir, essenceFilename) = splitFileName essence
let essenceBasename = takeBaseName essenceFilename
when (length eprimes == 1) $
if null essenceParams
then do
let solutions' = [ solution
| (_, _, solution) <- solutions ]
case solutions' of
[solution] ->
copySolution solution (essenceDir
</> intercalate "-" [ essenceBasename
]
<.> ".solution")
_ -> forM_ (zip allNats solutions') $ \ (i, solution) ->
copySolution solution (essenceDir
</> intercalate "-" [ essenceBasename
, paddedNum 6 '0' i
]
<.> ".solution")
else forM_ essenceParams $ \ essenceParam -> do
let (_paramDir, paramFilename) = splitFileName essenceParam
let paramBasename = takeBaseName paramFilename
let solutions' = [ solution
| (_, essenceParam', solution) <- solutions
, essenceParam == essenceParam' ]
case solutions' of
[solution] ->
copySolution solution (essenceDir
</> intercalate "-" [ essenceBasename
, paramBasename
]
<.> ".solution")
_ -> forM_ (zip allNats solutions') $ \ (i, solution) ->
copySolution solution (essenceDir
</> intercalate "-" [ essenceBasename
, paramBasename
, paddedNum 6 '0' i
]
<.> ".solution")

liftIO stopGlobalPool

Expand Down Expand Up @@ -400,6 +406,10 @@ srMkArgs Solve{..} outBase modelPath =
, "-run-solver"
, "-solutions-to-stdout-one-line"
] ++
( if nbSolutions == "all"
then ["-all-solutions"]
else ["-num-solutions", stringToText nbSolutions]
) ++
( case solver of
"minion" -> [ "-minion" ]
"lingeling" -> [ "-sat"
Expand Down
7 changes: 6 additions & 1 deletion tests/golden/conjure-help.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -166,6 +166,11 @@ conjure solve [OPTIONS] ESSENCE_FILE [PARAMETER_FILE(s)]
General:
--validate-solutions Enable/disable solution validation. Off by default.
--limit-time=INT Time limit in seconds (real time).
--number-of-solutions=ITEM Number of solutions to find.
Pass the string "all" to enumerate all solutions.
Default: 1
--copy-solutions Whether to place a copy of solution(s) next to the Essence file or not.
Default: on
Logging & Output:
-o --output-directory=DIR Output directory. Generated models will be saved here.
Default value: 'conjure-output'
Expand Down Expand Up @@ -235,7 +240,7 @@ Model generation:
models for solving.
Options for other tools:
--savilerow-options=ITEM Options to be passed to Savile Row.
By default: '-O2'
Default: '-O2'
--solver-options=ITEM Options to be passed to the backend solver.
--solver=ITEM Backend solver to use.
Possible values: minion/lingeling/minisat
Expand Down

0 comments on commit fcbc44b

Please sign in to comment.