Skip to content

Commit

Permalink
Merge pull request #603 from conjure-cp/adding-ortools
Browse files Browse the repository at this point in the history
Adding ortools
  • Loading branch information
ozgurakgun authored Nov 8, 2023
2 parents ab20205 + 3a35696 commit bfa30a9
Show file tree
Hide file tree
Showing 11 changed files with 418 additions and 34 deletions.
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -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/
Expand Down
8 changes: 5 additions & 3 deletions Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -45,6 +46,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

Expand All @@ -57,8 +59,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-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

Expand All @@ -70,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

Expand Down
1 change: 1 addition & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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/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
2 changes: 1 addition & 1 deletion docs/conjure-help.html
Original file line number Diff line number Diff line change
Expand Up @@ -135,7 +135,7 @@
<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>
<tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--solver=ITEM</td><td style='padding-left:2ex;'>Backend solver. Possible values:<br /> - minion (CP solver)<br /> - gecode (CP solver)<br /> - chuffed (CP solver)<br /> - glucose (SAT solver)<br /> - glucose-syrup (SAT solver)<br /> - lingeling/plingeling/treengeling (SAT solver)<br /> - cadical (SAT solver)<br /> - kissat (SAT solver)<br /> - minisat (SAT solver)<br /> - bc_minisat_all (AllSAT solver, only works with --number-of-solutions=all)<br /> - nbc_minisat_all (AllSAT solver, only works with --number-of-solutions=all)<br /> - open-wbo (MaxSAT solver, only works with optimisation problems)<br /> - coin-or (MIP solver, implemented via MiniZinc)<br /> - cplex (MIP solver, implemented via MiniZinc)<br /> - boolector (SMT solver, supported logics: bv)<br /> - yices (SMT solver, supported logics: bv, lia, idl)<br /> - z3 (SMT solver, supported logics: bv, lia, nia, idl)<br />Default: minion<br /><br />Default logic for SMT solvers is bitvector (bv).<br />Append a dash and the name of a logic to the solver name to choose a different logic. For example yices-idl.</td></tr>
<tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--solver=ITEM</td><td style='padding-left:2ex;'>Backend solver. Possible values:<br /> - minion (CP solver)<br /> - gecode (CP solver)<br /> - chuffed (CP solver)<br /> - or-tools (CP solver)<br /> - glucose (SAT solver)<br /> - glucose-syrup (SAT solver)<br /> - lingeling/plingeling/treengeling (SAT solver)<br /> - cadical (SAT solver)<br /> - kissat (SAT solver)<br /> - minisat (SAT solver)<br /> - bc_minisat_all (AllSAT solver, only works with --number-of-solutions=all)<br /> - nbc_minisat_all (AllSAT solver, only works with --number-of-solutions=all)<br /> - open-wbo (MaxSAT solver, only works with optimisation problems)<br /> - coin-or (MIP solver, implemented via MiniZinc)<br /> - cplex (MIP solver, implemented via MiniZinc)<br /> - boolector (SMT solver, supported logics: bv)<br /> - yices (SMT solver, supported logics: bv, lia, idl)<br /> - z3 (SMT solver, supported logics: bv, lia, nia, idl)<br />Default: minion<br /><br />Default logic for SMT solvers is bitvector (bv).<br />Append a dash and the name of a logic to the solver name to choose a different logic. For example yices-idl.</td></tr>
<tr><td colspan='3'>&nbsp;</tr>
<tr><td colspan='3'>conjure ide [OPTIONS] ESSENCE_FILE</td></tr>
<tr><td colspan='3' style='padding-left:2ex;'>IDE support features for Conjure.<br />Not intended for direct use.</td></tr>
Expand Down
1 change: 1 addition & 0 deletions docs/conjure-help.txt
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
29 changes: 29 additions & 0 deletions etc/build/install-ortools.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
#!/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
ls -l build/lib
# .dylib or .a depending on OS
cp build/lib/libortools* ${BIN_DIR}
echo "ortools executable is at ${BIN_DIR}/fzn-ortools"
ls -l ${BIN_DIR}/fzn-ortools
popd
rm -rf tmp-install-ortools
1 change: 1 addition & 0 deletions src/Conjure/UI.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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\
Expand Down
2 changes: 2 additions & 0 deletions src/Conjure/UI/MainHelper.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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" )
Expand Down Expand Up @@ -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"
Expand Down
157 changes: 127 additions & 30 deletions tests/allsolvers/run.sh
Original file line number Diff line number Diff line change
@@ -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

)
Loading

0 comments on commit bfa30a9

Please sign in to comment.