From c95961f217cc0f96e63ba8fc73fd1e4c4b551d3b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?O=CC=88zgu=CC=88r=20Akgu=CC=88n?= Date: Tue, 7 Nov 2023 22:14:10 +0000 Subject: [PATCH 01/10] add or-tools as a supported solver --- Makefile | 1 + etc/build/install-ortools.sh | 27 +++++++++++++++++++++++++++ src/Conjure/UI.hs | 1 + src/Conjure/UI/MainHelper.hs | 2 ++ 4 files changed, 31 insertions(+) create mode 100755 etc/build/install-ortools.sh diff --git a/Makefile b/Makefile index d568e7056..f501e5263 100644 --- a/Makefile +++ b/Makefile @@ -139,6 +139,7 @@ solvers: @etc/build/silent-wrapper.sh etc/build/install-minion.sh @etc/build/silent-wrapper.sh etc/build/install-nbc_minisat_all.sh @etc/build/silent-wrapper.sh etc/build/install-open-wbo.sh + @etc/build/silent-wrapper.sh etc/build/install-ortools.sh @etc/build/silent-wrapper.sh etc/build/install-yices.sh @etc/build/silent-wrapper.sh etc/build/install-z3.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 diff --git a/etc/build/install-ortools.sh b/etc/build/install-ortools.sh new file mode 100755 index 000000000..7df03e009 --- /dev/null +++ b/etc/build/install-ortools.sh @@ -0,0 +1,27 @@ +#!/bin/bash + +# version as of 7 Nov 2023 +VERSION=v9.7 + +source "download.sh" 2> /dev/null # if called from the script dir +source "etc/build/download.sh" 2> /dev/null # if called from the repo base (the common case) + +set -o errexit +set -o nounset + +export BIN_DIR=${BIN_DIR:-${HOME}/.local/bin} + +rm -rf tmp-install-ortools +mkdir tmp-install-ortools +pushd tmp-install-ortools +download https://github.com/google/or-tools/archive/refs/tags/${VERSION}.zip +unzip ${VERSION}.zip +cd or-tools-9.7 +cmake -S. -Bbuild -DBUILD_DEPS:BOOL=ONere +cmake --build build +cp build/bin/fzn-ortools ${BIN_DIR}/fzn-ortools +cp build/lib/libortools_flatzinc.9.dylib build/lib/libortools.9.dylib ${BIN_DIR} +echo "ortools executable is at ${BIN_DIR}/fzn-ortools" +ls -l ${BIN_DIR}/fzn-ortools +popd +rm -rf tmp-install-ortools diff --git a/src/Conjure/UI.hs b/src/Conjure/UI.hs index a26e790e4..76acbbfe9 100644 --- a/src/Conjure/UI.hs +++ b/src/Conjure/UI.hs @@ -914,6 +914,7 @@ ui = modes \ - minion (CP solver)\n\ \ - gecode (CP solver)\n\ \ - chuffed (CP solver)\n\ + \ - or-tools (CP solver)\n\ \ - glucose (SAT solver)\n\ \ - glucose-syrup (SAT solver)\n\ \ - lingeling/plingeling/treengeling (SAT solver)\n\ diff --git a/src/Conjure/UI/MainHelper.hs b/src/Conjure/UI/MainHelper.hs index fd6beee8e..050b8aa47 100644 --- a/src/Conjure/UI/MainHelper.hs +++ b/src/Conjure/UI/MainHelper.hs @@ -854,6 +854,7 @@ solverExecutables = , ( "bc_minisat_all" , "bc_minisat_all_release" ) , ( "nbc_minisat_all" , "nbc_minisat_all_release" ) , ( "open-wbo" , "open-wbo" ) + , ( "or-tools" , "fzn-ortools" ) , ( "coin-or" , "minizinc" ) , ( "cplex" , "minizinc" ) , ( "yices" , "yices-smt2" ) @@ -919,6 +920,7 @@ srMkArgs Solve{..} outBase modelPath = do "minion" -> return [ "-minion" ] "gecode" -> return [ "-gecode" ] "chuffed" -> return [ "-chuffed"] + "or-tools" -> return [ "-or-tools"] "glucose" -> return [ "-sat" , "-sat-family", "glucose" , "-satsolver-bin", "glucose" From a2f0c45630892a3426e6c6717520ce295f97ebc1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?O=CC=88zgu=CC=88r=20Akgu=CC=88n?= Date: Tue, 7 Nov 2023 22:17:18 +0000 Subject: [PATCH 02/10] Update the allsolvers test to include or-tools --- .gitignore | 1 + tests/allsolvers/run.sh | 157 +++++++++++++++++---- tests/allsolvers/stdout.expected | 235 +++++++++++++++++++++++++++++++ tests/allsolvers/test.sh | 15 ++ 4 files changed, 378 insertions(+), 30 deletions(-) create mode 100644 tests/allsolvers/stdout.expected create mode 100755 tests/allsolvers/test.sh diff --git a/.gitignore b/.gitignore index bb46664db..ebda5a53e 100644 --- a/.gitignore +++ b/.gitignore @@ -23,6 +23,7 @@ tests/parse_print/**/typecheck tests/parse_print/**/model.json tests/custom/**/stdout tests/custom/**/stderr +tests/allsolvers/stdout #parallel tests outputs test_results/ diff --git a/tests/allsolvers/run.sh b/tests/allsolvers/run.sh index ee2c0e535..4dbdfc7da 100755 --- a/tests/allsolvers/run.sh +++ b/tests/allsolvers/run.sh @@ -1,103 +1,200 @@ +#!/bin/bash + +# get the script directory +DIR="$( cd "$( dirname "$0" )" && pwd )" + +( +cd $DIR echo "default, minion" conjure solve test.essence +echo "" +echo "" +echo "========================================" # CP solvers -echo "\nminion" +echo "minion" conjure solve test.essence --solver minion +echo "" +echo "" +echo "========================================" -echo "\ngecode" +echo "gecode" conjure solve test.essence --solver gecode +echo "" +echo "" +echo "========================================" -echo "\nchuffed" +echo "chuffed" conjure solve test.essence --solver chuffed +echo "" +echo "" +echo "========================================" +# echo "or-tools" +# conjure solve test.essence --solver or-tools +# echo "" +# echo "" +# echo "========================================" # SAT solvers -echo "\nglucose" +echo "glucose" conjure solve test.essence --solver glucose +echo "" +echo "" +echo "========================================" -echo "\nglucose-syrup" +echo "glucose-syrup" conjure solve test.essence --solver glucose-syrup +echo "" +echo "" +echo "========================================" -echo "\nlingeling" +echo "lingeling" conjure solve test.essence --solver lingeling +echo "" +echo "" +echo "========================================" -echo "\nplingeling" +echo "plingeling" conjure solve test.essence --solver plingeling +echo "" +echo "" +echo "========================================" -echo "\ntreengeling" +echo "treengeling" conjure solve test.essence --solver treengeling +echo "" +echo "" +echo "========================================" -echo "\ncadical" +echo "cadical" conjure solve test.essence --solver cadical +echo "" +echo "" +echo "========================================" -echo "\nminisat" -conjure solve test.essence --solver minisat - +# commenting out as we do not have an install script for it +# echo "minisat" +# conjure solve test.essence --solver minisat +# echo "" +# echo "" +# echo "========================================" # AllSAT solvers -echo "\nbc_minisat_all --number-of-solutions=all" +echo "bc_minisat_all --number-of-solutions=all" conjure solve test.essence --solver bc_minisat_all --number-of-solutions=all +echo "" +echo "" +echo "========================================" -echo "\nnbc_minisat_all --number-of-solutions=all" +echo "nbc_minisat_all --number-of-solutions=all" conjure solve test.essence --solver nbc_minisat_all --number-of-solutions=all +echo "" +echo "" +echo "========================================" # MaxSAT solvers -echo "\nopen-wbo" +echo "open-wbo" conjure solve testo.essence --solver open-wbo +echo "" +echo "" +echo "========================================" # MIP solvers (via MiniZinc) -echo "\ncoin-or" -conjure solve test.essence --solver coin-or +# commenting out as we do not have an install script for it +# echo "coin-or" +# conjure solve test.essence --solver coin-or +# echo "" +# echo "" +# echo "========================================" -echo "\ncplex" -conjure solve test.essence --solver cplex +# commenting out as we do not have an install script for it +# echo "cplex" +# conjure solve test.essence --solver cplex +# echo "" +# echo "" +# echo "========================================" # SMT solvers -echo "\nboolector" +echo "boolector" conjure solve test.essence --solver boolector +echo "" +echo "" +echo "========================================" -echo "\nboolector-bv" +echo "boolector-bv" conjure solve test.essence --solver boolector-bv +echo "" +echo "" +echo "========================================" -echo "\nyices" +echo "yices" conjure solve test.essence --solver yices +echo "" +echo "" +echo "========================================" -echo "\nyices-bv" +echo "yices-bv" conjure solve test.essence --solver yices-bv +echo "" +echo "" +echo "========================================" -echo "\nyices-lia" +echo "yices-lia" conjure solve test.essence --solver yices-lia +echo "" +echo "" +echo "========================================" -echo "\nyices-idl" +echo "yices-idl" conjure solve test.essence --solver yices-idl +echo "" +echo "" +echo "========================================" -echo "\nz3" +echo "z3" conjure solve test.essence --solver z3 +echo "" +echo "" +echo "========================================" -echo "\nz3-bv" +echo "z3-bv" conjure solve test.essence --solver z3-bv +echo "" +echo "" +echo "========================================" -echo "\nz3-lia" +echo "z3-lia" conjure solve test.essence --solver z3-lia +echo "" +echo "" +echo "========================================" -echo "\nz3-nia" +echo "z3-nia" conjure solve test.essence --solver z3-nia +echo "" +echo "" +echo "========================================" -echo "\nz3-idl" +echo "z3-idl" conjure solve test.essence --solver z3-idl +echo "" +echo "" +echo "========================================" # remove the generated files rm -rf conjure-output *.solution + +) diff --git a/tests/allsolvers/stdout.expected b/tests/allsolvers/stdout.expected new file mode 100644 index 000000000..8e4668cb7 --- /dev/null +++ b/tests/allsolvers/stdout.expected @@ -0,0 +1,235 @@ +default, minion +Generating models for test.essence +Generated models: model000001.eprime +Saved under: conjure-output +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: minion +Copying solution to: test.solution + + +======================================== +minion +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: minion +Copying solution to: test.solution + + +======================================== +gecode +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: gecode +Copying solution to: test.solution + + +======================================== +chuffed +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: chuffed +Copying solution to: test.solution + + +======================================== +glucose +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: glucose +Copying solution to: test.solution + + +======================================== +glucose-syrup +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: glucose-syrup +Copying solution to: test.solution + + +======================================== +lingeling +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: lingeling +Copying solution to: test.solution + + +======================================== +plingeling +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: plingeling +Copying solution to: test.solution + + +======================================== +treengeling +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: treengeling +Copying solution to: test.solution + + +======================================== +cadical +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: cadical +Copying solution to: test.solution + + +======================================== +bc_minisat_all --number-of-solutions=all +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: bc_minisat_all +Copying solution to: test-000001.solution +Copying solution to: test-000002.solution +Copying solution to: test-000003.solution +Copying solution to: test-000004.solution +Copying solution to: test-000005.solution +Copying solution to: test-000006.solution +Copying solution to: test-000007.solution + + +======================================== +nbc_minisat_all --number-of-solutions=all +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: nbc_minisat_all +Copying solution to: test-000001.solution +Copying solution to: test-000002.solution +Copying solution to: test-000003.solution +Copying solution to: test-000004.solution +Copying solution to: test-000005.solution +Copying solution to: test-000006.solution +Copying solution to: test-000007.solution + + +======================================== +open-wbo +Generating models for testo.essence +Generated models: model000001.eprime +Saved under: conjure-output +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: open-wbo +Copying solution to: testo.solution + + +======================================== +boolector +Generating models for test.essence +Generated models: model000001.eprime +Saved under: conjure-output +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: boolector +Copying solution to: test.solution + + +======================================== +boolector-bv +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: boolector-bv +Copying solution to: test.solution + + +======================================== +yices +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: yices +Copying solution to: test.solution + + +======================================== +yices-bv +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: yices-bv +Copying solution to: test.solution + + +======================================== +yices-lia +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: yices-lia +Copying solution to: test.solution + + +======================================== +yices-idl +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: yices-idl +Copying solution to: test.solution + + +======================================== +z3 +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: z3 +Copying solution to: test.solution + + +======================================== +z3-bv +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: z3-bv +Copying solution to: test.solution + + +======================================== +z3-lia +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: z3-lia +Copying solution to: test.solution + + +======================================== +z3-nia +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: z3-nia +Copying solution to: test.solution + + +======================================== +z3-idl +Using cached models. +Savile Row: model000001.eprime +Running minion for domain filtering. +Running solver: z3-idl +No solutions found. +Copying solution to: test.solution + + +======================================== diff --git a/tests/allsolvers/test.sh b/tests/allsolvers/test.sh new file mode 100755 index 000000000..f60ce3aa9 --- /dev/null +++ b/tests/allsolvers/test.sh @@ -0,0 +1,15 @@ +#!/bin/bash + +# get the script directory +DIR="$( cd "$( dirname "$0" )" && pwd )" + +( +cd $DIR +./run.sh | tee stdout +if ! diff stdout stdout.expected; then + echo "The generated stdout doesn't match the expected stdout." + echo "That's what we call a failed test around here..." +else + echo "Pass!" +fi +) From f33aa992b8e9d0b27e594ddfc996119a84db03cb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?O=CC=88zgu=CC=88r=20Akgu=CC=88n?= Date: Tue, 7 Nov 2023 22:40:50 +0000 Subject: [PATCH 03/10] docker: build or-tools too --- Dockerfile | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Dockerfile b/Dockerfile index a36d3908c..8ff236500 100644 --- a/Dockerfile +++ b/Dockerfile @@ -45,6 +45,7 @@ RUN PROCESSES=2 etc/build/install-lingeling.sh RUN PROCESSES=2 etc/build/install-minion.sh RUN PROCESSES=2 etc/build/install-nbc_minisat_all.sh 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 @@ -57,8 +58,8 @@ RUN make install # Make binaries a bit smaller RUN ls -l /root/.local/bin RUN du -sh /root/.local/bin -RUN cd /root/.local/bin ; strip conjure bc_minisat_all_release boolector cadical fzn-chuffed glucose glucose-syrup kissat lingeling minion nbc_minisat_all_release open-wbo plingeling treengeling yices yices-sat yices-smt yices-smt2 z3 -# RUN cd /root/.local/bin ; strip conjure bc_minisat_all_release boolector cadical fzn-chuffed fzn-gecode glucose glucose-syrup kissat lingeling minion nbc_minisat_all_release open-wbo plingeling treengeling yices yices-sat yices-smt yices-smt2 z3 +RUN cd /root/.local/bin ; strip conjure bc_minisat_all_release boolector cadical fzn-chuffed fzn-or-tools glucose glucose-syrup kissat lingeling minion nbc_minisat_all_release open-wbo plingeling treengeling yices yices-sat yices-smt yices-smt2 z3 +# RUN cd /root/.local/bin ; strip conjure bc_minisat_all_release boolector cadical fzn-chuffed fzn-gecode fzn-or-tools glucose glucose-syrup kissat lingeling minion nbc_minisat_all_release open-wbo plingeling treengeling yices yices-sat yices-smt yices-smt2 z3 RUN ls -l /root/.local/bin RUN du -sh /root/.local/bin From 7be77763ad180d74ecf9377a08aad6182032123b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?O=CC=88zgu=CC=88r=20Akgu=CC=88n?= Date: Tue, 7 Nov 2023 23:19:46 +0000 Subject: [PATCH 04/10] make or-tools compilation chatty in the makefile (for debugging) --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index f501e5263..4dc5a0528 100644 --- a/Makefile +++ b/Makefile @@ -139,7 +139,7 @@ solvers: @etc/build/silent-wrapper.sh etc/build/install-minion.sh @etc/build/silent-wrapper.sh etc/build/install-nbc_minisat_all.sh @etc/build/silent-wrapper.sh etc/build/install-open-wbo.sh - @etc/build/silent-wrapper.sh etc/build/install-ortools.sh + @etc/build/install-ortools.sh @etc/build/silent-wrapper.sh etc/build/install-yices.sh @etc/build/silent-wrapper.sh etc/build/install-z3.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 From 26575f65bd01ec0dd893b855b2b09f38edf3a5b9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?O=CC=88zgu=CC=88r=20Akgu=CC=88n?= Date: Wed, 8 Nov 2023 08:07:42 +0000 Subject: [PATCH 05/10] debugging --- etc/build/install-ortools.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/etc/build/install-ortools.sh b/etc/build/install-ortools.sh index 7df03e009..525b76a3d 100755 --- a/etc/build/install-ortools.sh +++ b/etc/build/install-ortools.sh @@ -20,6 +20,7 @@ cd or-tools-9.7 cmake -S. -Bbuild -DBUILD_DEPS:BOOL=ONere cmake --build build cp build/bin/fzn-ortools ${BIN_DIR}/fzn-ortools +ls -l build/lib cp build/lib/libortools_flatzinc.9.dylib build/lib/libortools.9.dylib ${BIN_DIR} echo "ortools executable is at ${BIN_DIR}/fzn-ortools" ls -l ${BIN_DIR}/fzn-ortools From ac2ffccd84bc3460d3ddf815c0d1b2d243e2b114 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?O=CC=88zgu=CC=88r=20Akgu=CC=88n?= Date: Wed, 8 Nov 2023 09:23:35 +0000 Subject: [PATCH 06/10] debugging --- etc/build/install-ortools.sh | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/etc/build/install-ortools.sh b/etc/build/install-ortools.sh index 525b76a3d..ddd2fa0b2 100755 --- a/etc/build/install-ortools.sh +++ b/etc/build/install-ortools.sh @@ -21,7 +21,8 @@ cmake -S. -Bbuild -DBUILD_DEPS:BOOL=ONere cmake --build build cp build/bin/fzn-ortools ${BIN_DIR}/fzn-ortools ls -l build/lib -cp build/lib/libortools_flatzinc.9.dylib build/lib/libortools.9.dylib ${BIN_DIR} +# .dylib or .a depending on OS +cp build/lib/libortools_flatzinc.9.* build/lib/libortools.9.* ${BIN_DIR} echo "ortools executable is at ${BIN_DIR}/fzn-ortools" ls -l ${BIN_DIR}/fzn-ortools popd From 7a0568e109908be7070ba0b6fb6f4162cb0bfbdf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?O=CC=88zgu=CC=88r=20Akgu=CC=88n?= Date: Wed, 8 Nov 2023 11:39:48 +0000 Subject: [PATCH 07/10] copy all libortools* files --- etc/build/install-ortools.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/etc/build/install-ortools.sh b/etc/build/install-ortools.sh index ddd2fa0b2..13cdb2586 100755 --- a/etc/build/install-ortools.sh +++ b/etc/build/install-ortools.sh @@ -22,7 +22,7 @@ cmake --build build cp build/bin/fzn-ortools ${BIN_DIR}/fzn-ortools ls -l build/lib # .dylib or .a depending on OS -cp build/lib/libortools_flatzinc.9.* build/lib/libortools.9.* ${BIN_DIR} +cp build/lib/libortools* ${BIN_DIR} echo "ortools executable is at ${BIN_DIR}/fzn-ortools" ls -l ${BIN_DIR}/fzn-ortools popd From db012c419d47573dc32ed21b6f7fa0835ffef4a7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?O=CC=88zgu=CC=88r=20Akgu=CC=88n?= Date: Wed, 8 Nov 2023 13:26:08 +0000 Subject: [PATCH 08/10] the executable is called fzn-ortools --- Dockerfile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Dockerfile b/Dockerfile index 8ff236500..b661f1799 100644 --- a/Dockerfile +++ b/Dockerfile @@ -58,8 +58,8 @@ RUN make install # Make binaries a bit smaller RUN ls -l /root/.local/bin RUN du -sh /root/.local/bin -RUN cd /root/.local/bin ; strip conjure bc_minisat_all_release boolector cadical fzn-chuffed fzn-or-tools glucose glucose-syrup kissat lingeling minion nbc_minisat_all_release open-wbo plingeling treengeling yices yices-sat yices-smt yices-smt2 z3 -# RUN cd /root/.local/bin ; strip conjure bc_minisat_all_release boolector cadical fzn-chuffed fzn-gecode fzn-or-tools glucose glucose-syrup kissat lingeling minion nbc_minisat_all_release open-wbo plingeling treengeling yices yices-sat yices-smt yices-smt2 z3 +RUN cd /root/.local/bin ; strip conjure bc_minisat_all_release boolector cadical fzn-chuffed fzn-ortools glucose glucose-syrup kissat lingeling minion nbc_minisat_all_release open-wbo plingeling treengeling yices yices-sat yices-smt yices-smt2 z3 +# RUN cd /root/.local/bin ; strip conjure bc_minisat_all_release boolector cadical fzn-chuffed fzn-gecode fzn-ortools glucose glucose-syrup kissat lingeling minion nbc_minisat_all_release open-wbo plingeling treengeling yices yices-sat yices-smt yices-smt2 z3 RUN ls -l /root/.local/bin RUN du -sh /root/.local/bin From f2525f2f1d011607dc6d132f12a70cd0152aeb50 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?O=CC=88zgu=CC=88r=20Akgu=CC=88n?= Date: Wed, 8 Nov 2023 13:27:55 +0000 Subject: [PATCH 09/10] we need jre for savilerow --- Dockerfile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index b661f1799..708691a72 100644 --- a/Dockerfile +++ b/Dockerfile @@ -28,6 +28,7 @@ RUN apt-get install -y --no-install-recommends zip unzip # needed RUN apt-get install -y --no-install-recommends autoconf # needed when building some solvers (for example yices) 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 # Only copying the install*.sh scripts RUN mkdir -p etc @@ -71,7 +72,7 @@ FROM ubuntu:23.10 WORKDIR /conjure ENV PATH /root/.local/bin:$PATH RUN apt-get update -RUN apt-get install -y --no-install-recommends default-jre-headless +RUN apt-get install -y --no-install-recommends default-jre-headless # savilerow RUN mkdir -p /root/.local/bin/lib COPY --from=builder /root/.local/bin /root/.local/bin From 3a35696db1b025a7f924978f9fb99787dd47d0b3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?O=CC=88zgu=CC=88r=20Akgu=CC=88n?= Date: Wed, 8 Nov 2023 19:34:08 +0000 Subject: [PATCH 10/10] update expected help text --- docs/conjure-help.html | 2 +- docs/conjure-help.txt | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/docs/conjure-help.html b/docs/conjure-help.html index ebfebad5f..9af27a831 100644 --- a/docs/conjure-help.html +++ b/docs/conjure-help.html @@ -135,7 +135,7 @@ Options for other tools:  --savilerow-options=ITEMOptions passed to Savile Row.  --solver-options=ITEMOptions passed to the backend solver. - --solver=ITEMBackend solver. Possible values:
- minion (CP solver)
- gecode (CP solver)
- chuffed (CP solver)
- glucose (SAT solver)
- glucose-syrup (SAT solver)
- lingeling/plingeling/treengeling (SAT solver)
- cadical (SAT solver)
- kissat (SAT solver)
- minisat (SAT solver)
- bc_minisat_all (AllSAT solver, only works with --number-of-solutions=all)
- nbc_minisat_all (AllSAT solver, only works with --number-of-solutions=all)
- open-wbo (MaxSAT solver, only works with optimisation problems)
- coin-or (MIP solver, implemented via MiniZinc)
- cplex (MIP solver, implemented via MiniZinc)
- boolector (SMT solver, supported logics: bv)
- yices (SMT solver, supported logics: bv, lia, idl)
- z3 (SMT solver, supported logics: bv, lia, nia, idl)
Default: minion

Default logic for SMT solvers is bitvector (bv).
Append a dash and the name of a logic to the solver name to choose a different logic. For example yices-idl. + --solver=ITEMBackend solver. Possible values:
- minion (CP solver)
- gecode (CP solver)
- chuffed (CP solver)
- or-tools (CP solver)
- glucose (SAT solver)
- glucose-syrup (SAT solver)
- lingeling/plingeling/treengeling (SAT solver)
- cadical (SAT solver)
- kissat (SAT solver)
- minisat (SAT solver)
- bc_minisat_all (AllSAT solver, only works with --number-of-solutions=all)
- nbc_minisat_all (AllSAT solver, only works with --number-of-solutions=all)
- open-wbo (MaxSAT solver, only works with optimisation problems)
- coin-or (MIP solver, implemented via MiniZinc)
- cplex (MIP solver, implemented via MiniZinc)
- boolector (SMT solver, supported logics: bv)
- yices (SMT solver, supported logics: bv, lia, idl)
- z3 (SMT solver, supported logics: bv, lia, nia, idl)
Default: minion

Default logic for SMT solvers is bitvector (bv).
Append a dash and the name of a logic to the solver name to choose a different logic. For example yices-idl.   conjure ide [OPTIONS] ESSENCE_FILE IDE support features for Conjure.
Not intended for direct use. diff --git a/docs/conjure-help.txt b/docs/conjure-help.txt index 35aa27329..d71f608d8 100644 --- a/docs/conjure-help.txt +++ b/docs/conjure-help.txt @@ -262,6 +262,7 @@ - minion (CP solver) - gecode (CP solver) - chuffed (CP solver) + - or-tools (CP solver) - glucose (SAT solver) - glucose-syrup (SAT solver) - lingeling/plingeling/treengeling (SAT solver)