Add runsolver support

.github/workflows/release.yml

@@ -82,6 +82,11 @@ jobs:
         run: brew install gperf
         if: runner.os == 'macOS'
 
+      - name: Installing dependencies (libnuma-dev) on Linux - needed for runsolver
+        shell: bash
+        run: sudo apt-get install -y libnuma-dev
+        if: runner.os == 'Linux'
+
       - name: Build solvers
         shell: bash
         run: |

.github/workflows/solvers.yml

@@ -57,6 +57,11 @@ jobs:
         run: brew install gperf
         if: runner.os == 'macOS'
 
+      - name: Installing dependencies (libnuma-dev) on Linux - needed for runsolver
+        shell: bash
+        run: sudo apt-get install -y libnuma-dev
+        if: runner.os == 'Linux'
+
       - name: Building solvers
         shell: bash
         run: BIN_DIR=${HOME}/.local/bin PROCESSES=2 make solvers

Dockerfile

@@ -30,6 +30,7 @@ RUN apt-get install -y --no-install-recommends autoconf                 # needed
 RUN apt-get install -y --no-install-recommends gperf                    # needed when building some solvers (for example yices)
 RUN apt-get install -y --no-install-recommends python3                  # needed when building some solvers (for example z3)
 RUN apt-get install -y --no-install-recommends default-jre-headless     # savilerow
+RUN apt-get install -y --no-install-recommends libnuma-dev              # runsolver
 
 # Only copying the install*.sh scripts
 RUN mkdir -p etc
@@ -51,6 +52,7 @@ RUN PROCESSES=2 etc/build/install-open-wbo.sh
 RUN PROCESSES=2 etc/build/install-ortools.sh
 RUN PROCESSES=2 etc/build/install-yices.sh
 RUN PROCESSES=2 etc/build/install-z3.sh
+RUN PROCESSES=2 etc/build/install-runsolver.sh
 
 # An attempt to cache more
 COPY Makefile Makefile

Makefile

@@ -157,4 +157,5 @@ solvers:
 	@etc/build/silent-wrapper.sh etc/build/install-minizinc.sh
 	@etc/build/silent-wrapper.sh etc/build/install-yices.sh
 	@etc/build/silent-wrapper.sh etc/build/install-z3.sh
+	@etc/build/silent-wrapper.sh etc/build/install-runsolver.sh
 	@if ls make-solvers-*.stderr make-solvers-*.stdout > /dev/null 2> /dev/null; then echo "At least one solver didn't build successfully."; exit 1; fi

docs/conjure-help.html

@@ -134,6 +134,9 @@
 <tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--seed=INT</td><td style='padding-left:2ex;'>Random number generator seed.</td></tr>
 <tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--limit-models=INT</td><td style='padding-left:2ex;'>Maximum number of models to generate.</td></tr>
 <tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--use-existing-models=FILE</td><td style='padding-left:2ex;'>File names of Essence' models generated beforehand.<br />If given, Conjure skips the modelling phase and uses the existing models for solving.<br />The models should be inside the output directory (See -o).</td></tr>
+<tr><td colspan='3'>runsolver:</td></tr>
+<tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--runsolver-cpu-time-limit=INT</td><td style='padding-left:2ex;'>Use runsolver to limit total CPU time (in seconds)</td></tr>
+<tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--runsolver-memory-limit=INT</td><td style='padding-left:2ex;'>Use runsolver to limit total memory usage (Maximum RSS - in megabytes).</td></tr>
 <tr><td colspan='3'>Options for other tools:</td></tr>
 <tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--savilerow-options=ITEM</td><td style='padding-left:2ex;'>Options passed to Savile Row.</td></tr>
 <tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--solver-options=ITEM</td><td style='padding-left:2ex;'>Options passed to the backend solver.</td></tr>

docs/conjure-help.txt

@@ -261,6 +261,9 @@
                                               If given, Conjure skips the modelling phase and uses the existing models
                                               for solving.
                                               The models should be inside the output directory (See -o).
+ runsolver:
+      --runsolver-cpu-time-limit=INT          Use runsolver to limit total CPU time (in seconds)
+      --runsolver-memory-limit=INT            Use runsolver to limit total memory usage (Maximum RSS - in megabytes).
  Options for other tools:
       --savilerow-options=ITEM                Options passed to Savile Row.
       --solver-options=ITEM                   Options passed to the backend solver.

etc/build/install-runsolver.sh

@@ -0,0 +1,40 @@
+#!/bin/bash
+
+# version as of 25 March 2024
+# alas, none of the published releases compile correctly
+VERSION='3f923c08285bdc5186f995296e1c6bffa0588710'
+
+set -o errexit
+set -o nounset
+
+DIR="$( cd "$( dirname "$0" )" && pwd )"
+
+export BIN_DIR=${BIN_DIR:-${HOME}/.local/bin}
+export PROCESSES=${PROCESSES:-1}
+
+OS=$(uname)
+
+if [ "$OS" == "Linux" ]; then
+    rm -rf tmp-install-runsolver
+    mkdir tmp-install-runsolver
+    pushd tmp-install-runsolver
+    git clone https://github.com/utpalbora/runsolver.git
+    cd runsolver
+    git checkout $VERSION
+    cd src
+    if make -j${PROCESSES} ; then
+        echo "Built."
+    else
+        echo "Build failed, trying again with a local patch"
+        echo "This might happen when building with an old version of libnuma-dev"
+        patch runsolver.cc ${DIR}/runsolver.patch
+        make -j${PROCESSES}
+    fi
+    cp runsolver ${BIN_DIR}/runsolver
+    echo "runsolver executable is at ${BIN_DIR}/runsolver"
+    ls -l ${BIN_DIR}/runsolver
+    popd
+    rm -rf tmp-install-runsolver
+else
+    echo "Your OS is (according to uname): ${OS} -- runsolver only works on linux."
+fi

etc/build/runsolver.patch

@@ -0,0 +1,13 @@
+diff --git a/src/runsolver.cc b/src/runsolver.cc
+index f42c9a1..312c985 100644
+--- a/src/runsolver.cc
++++ b/src/runsolver.cc
+@@ -906,7 +906,7 @@ void numaInfo() {
+     return;
+
+   int nbNodes = numa_num_configured_nodes();
+-  long mem, memFree;
++  long long mem, memFree;
+
+   cout << "NUMA information:\n";
+   cout << "  number of nodes: " << nbNodes << endl;

etc/build/silent-wrapper.sh

@@ -1,13 +1,15 @@
 #!/bin/bash
 
-# set -o errexit
-# set -o nounset
+set -o errexit
+set -o nounset
 
 if [ $# -ne 1 ]; then
     echo "Only provide a single argument, the path to a bash script."
     exit 1
 fi
 
+export CI=${CI:-false}
+
 echo "Running $1"
 
 PID=$$
@@ -24,11 +26,19 @@ else
     echo "        Exit code: ${EXITCODE}"
     echo "        Outputs saved to: make-solvers-${PID}.stdout and make-solvers-${PID}.stderr"
     echo ""
-    echo "Last 10 lines of the stdout was:"
-    tail -n10 make-solvers-${PID}.stdout
-    echo ""
-    echo "Last 10 lines of the stderr was:"
-    tail -n10 make-solvers-${PID}.stderr
+    if ${CI}; then
+        echo "stdout was:"
+        cat make-solvers-${PID}.stdout
+        echo ""
+        echo "stderr was:"
+        cat make-solvers-${PID}.stderr
+    else
+        echo "Last 10 lines of the stdout was:"
+        tail -n10 make-solvers-${PID}.stdout
+        echo ""
+        echo "Last 10 lines of the stderr was:"
+        tail -n10 make-solvers-${PID}.stderr
+    fi
     echo ""
     echo ""
     echo ""

src/Conjure/Process/Enumerate.hs

@@ -143,6 +143,8 @@ enumerateDomain d = liftIO' $ withSystemTempDirectory ("conjure-enumerateDomain-
             , nbSolutions                   = show enumerateDomainMax
             , copySolutions                 = False
             , solutionsInOneFile            = False
+            , runsolverCPUTimeLimit         = Nothing
+            , runsolverMemoryLimit          = Nothing
             , logLevel                      = LogNone
             -- default values for the rest
             , essenceParams                 = []

src/Conjure/UI.hs

@@ -99,6 +99,8 @@ data UI
         , responses                  :: String
         , responsesRepresentation    :: String
         , solutionsInOneFile         :: Bool
+        , runsolverCPUTimeLimit      :: Maybe Int
+        , runsolverMemoryLimit       :: Maybe Int
         -- flags related to logging
         , logLevel                   :: LogLevel
         , verboseTrail               :: Bool
@@ -739,6 +741,18 @@ ui = modes
             &= explicit
             &= help "Place all solutions in a single file instead of generating a separate file per solution.\n\
                     \Off by default."
+        , runsolverCPUTimeLimit
+            = def
+            &= name "runsolver-cpu-time-limit"
+            &= groupname "runsolver"
+            &= explicit
+            &= help "Use runsolver to limit total CPU time (in seconds)"
+        , runsolverMemoryLimit
+            = def
+            &= name "runsolver-memory-limit"
+            &= groupname "runsolver"
+            &= explicit
+            &= help "Use runsolver to limit total memory usage (Maximum RSS - in megabytes)."
         , logLevel
             = def
             &= name "log-level"

src/Conjure/UI/MainHelper.hs

@@ -800,10 +800,18 @@ savileRowNoParam ui@Solve{..} (modelPath, eprimeModel) = sh $ errExit False $ do
     when (logLevel >= LogDebug) $ do
         liftIO $ putStrLn "Using the following options for Savile Row:"
         liftIO $ putStrLn $ "    savilerow " ++ unwords (map (quoteMultiWord . textToString) srArgs)
-    (stdoutSR, solutions) <- partitionEithers <$> runHandle savilerowScriptName srArgs
-                                (liftIO . srStdoutHandler
-                                    (outBase, modelPath, "<no param file>", ui)
-                                    tr (1::Int))
+    let handler = liftIO . srStdoutHandler
+                    (outBase, modelPath, "<no param file>", ui)
+                    tr (1::Int)
+    let runsolverArgs = maybe [] (\ limit -> ["-C", show limit]) runsolverCPUTimeLimit ++
+                        maybe [] (\ limit -> ["-R", show limit]) runsolverMemoryLimit
+    (stdoutSR, solutions) <- partitionEithers <$>
+        if null runsolverArgs
+            then runHandle savilerowScriptName srArgs handler
+            else
+                if os /= "linux"
+                    then return [Left "runsolver is only supported on linux"]
+                    else runHandle "runsolver" (map stringToText runsolverArgs ++ [stringToText savilerowScriptName] ++ srArgs) handler
     srCleanUp outBase ui (stringToText $ unlines stdoutSR) solutions
 savileRowNoParam _ _ = bug "savileRowNoParam"
 
@@ -841,10 +849,19 @@ savileRowWithParams ui@Solve{..} (modelPath, eprimeModel) (paramPath, essencePar
             when (logLevel >= LogDebug) $ do
                 liftIO $ putStrLn "Using the following options for Savile Row:"
                 liftIO $ putStrLn $ "    savilerow " ++ unwords (map (quoteMultiWord . textToString) srArgs)
-            (stdoutSR, solutions) <- partitionEithers <$> runHandle savilerowScriptName srArgs
-                                        (liftIO . srStdoutHandler
-                                            (outBase, modelPath, paramPath, ui)
-                                            tr (1::Int))
+            let handler = liftIO . srStdoutHandler
+                            (outBase, modelPath, paramPath, ui)
+                            tr (1::Int)
+            let runsolverArgs = maybe [] (\ limit -> ["-C", show limit]) runsolverCPUTimeLimit ++
+                                maybe [] (\ limit -> ["-V", show limit]) runsolverMemoryLimit
+            (stdoutSR, solutions) <- partitionEithers <$>
+                if null runsolverArgs
+                    then runHandle savilerowScriptName srArgs handler
+                    else
+                        if os /= "linux"
+                            then return [Left "runsolver is only supported on linux"]
+                            else  runHandle "runsolver" (map stringToText runsolverArgs ++ [stringToText savilerowScriptName] ++ srArgs) handler
+
             srCleanUp outBase ui (stringToText $ unlines stdoutSR) solutions
 savileRowWithParams _ _ _ = bug "savileRowWithParams"