diff --git a/bin/R-packages.R b/bin/R-packages.R deleted file mode 100644 index 5759fa46..00000000 --- a/bin/R-packages.R +++ /dev/null @@ -1,8 +0,0 @@ -paths <- list(R6="R6_2.5.1.tar.gz", data.table="data.table_1.14.2.tar.gz") -binDir <- "" -for (p in c("R6","data.table")){ - if (!require(p,character.only = TRUE)){ - install.packages(paste(binDir,paths[[p]],sep='/'), lib=binDir) - library(p,character.only = TRUE, lib.loc=binDir) - } -} diff --git a/bin/R6_2.5.1.tar.gz b/bin/R6_2.5.1.tar.gz deleted file mode 100644 index 78082479..00000000 Binary files a/bin/R6_2.5.1.tar.gz and /dev/null differ diff --git a/bin/data.table_1.14.2.tar.gz b/bin/data.table_1.14.2.tar.gz deleted file mode 100644 index 590bbd27..00000000 Binary files a/bin/data.table_1.14.2.tar.gz and /dev/null differ diff --git a/bin/install-all.sh b/bin/install-all.sh deleted file mode 100755 index 0e41772f..00000000 --- a/bin/install-all.sh +++ /dev/null @@ -1,10 +0,0 @@ -BIN_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )" - -pushd $BIN_DIR - -for s in conjure savilerow mininzinc irace runsolver ortools yuck picat -do - bash install-${s}.sh -done - -popd diff --git a/bin/install-conjure.sh b/bin/install-conjure.sh deleted file mode 100755 index b1443db0..00000000 --- a/bin/install-conjure.sh +++ /dev/null @@ -1,34 +0,0 @@ -name="conjure" -url="https://github.com/conjure-cp/conjure" -#version="6977bc0" # essence-features branch, 2021-11-22 -#version="d806b9f" # master branch, 2022-01-07 - -echo "" -echo "============= INSTALLING $name ===================" -#echo "$name version: $version" - -BIN_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )" - -pushd $BIN_DIR - -mkdir -p $name - -SOURCE_DIR="$name-source" -mkdir -p $SOURCE_DIR - -pushd $SOURCE_DIR -git clone $url -pushd conjure -#git checkout $version -export PATH=$BIN_DIR/$name/:$PATH -BIN_DIR=$BIN_DIR/$name make install -popd -popd - -rm -rf $SOURCE_DIR - -# remove conjure's savilerow (savilerow should be installed later using install-savilerow.sh) -rm -rf $name/savilerow-* -rm -rf $name/lib - -popd diff --git a/bin/install-irace.sh b/bin/install-irace.sh deleted file mode 100755 index 78d8e2e7..00000000 --- a/bin/install-irace.sh +++ /dev/null @@ -1,52 +0,0 @@ -name="irace" -version="3.4.1" - -echo "" -echo "============= INSTALLING $name ===================" -echo "$name version: $version" - -BIN_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )" - -# check if R is installed -if ! [ -x "$(command -v R)" ]; then - echo "ERROR: R must be installed first. See https://www.r-project.org/ for how to install R." - exit 1 -fi - -url="https://cran.r-project.org/src/contrib/irace_3.4.1.tar.gz" - -pushd $BIN_DIR - -mkdir -p $name - -SOURCE_DIR="$name-source" -mkdir -p $SOURCE_DIR - -pushd $SOURCE_DIR -#wget $url -#tar zxf $(ls *.gz) -cp $BIN_DIR/irace-source.zip ./ -unzip irace-source.zip -#wget https://cran.r-project.org/src/contrib/R6_2.5.1.tar.gz -#tar zxf R6_2.5.1.tar.gz -#wget https://cran.r-project.org/src/contrib/data.table_1.14.2.tar.gz -#tar zxf data.table_1.14.2.tar.gz -#R CMD INSTALL -l $BIN_DIR/ R6 -cp $BIN_DIR/R-packages.R ./ -OS=$(uname) -if [ "$OS" == "Darwin" ]; then - sed -i "" "s##$BIN_DIR#g" R-packages.R -elif [ "$OS" == "Linux" ]; then - sed -i "s##$BIN_DIR#g" R-packages.R -else - echo "Cannot determine your OS, uname reports: ${OS}" - exit 1 -fi -Rscript R-packages.R -export R_LIBS=$BIN_DIR/:$R_LIBS -R CMD INSTALL -l $BIN_DIR/ irace -popd - -rm -rf $SOURCE_DIR - -popd diff --git a/bin/install-mininzinc.sh b/bin/install-mininzinc.sh deleted file mode 100755 index 1608d795..00000000 --- a/bin/install-mininzinc.sh +++ /dev/null @@ -1,45 +0,0 @@ -name="minizinc" -version="2.8.5" - - -echo "" -echo "============= INSTALLING $name ===================" -echo "$name version: $version" - -BIN_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )" - -pushd $BIN_DIR - -OS=$(uname) -if [ "$OS" == "Darwin" ]; then - #url="https://github.com/MiniZinc/MiniZincIDE/releases/download/${version}/MiniZincIDE-${version}-bundled.dmg" - echo "Using local files (minizinc-2.5.5-part-mac.tgz) for minizinc installation" -elif [ "$OS" == "Linux" ]; then - url="https://github.com/MiniZinc/MiniZincIDE/releases/download/${version}/MiniZincIDE-${version}-bundle-linux-x86_64.tgz" -else - echo "Cannot determine your OS, uname reports: ${OS}" - exit 1 -fi - -mkdir -p $name - -SOURCE_DIR="$name-source" -mkdir -p $SOURCE_DIR - -pushd $SOURCE_DIR -if [ "$OS" == "Linux" ]; then - wget $url - tar zxf $(ls *.tgz) - d=$(ls -d */) - mv ${d}/* $BIN_DIR/$name -else - cp $BIN_DIR/minizinc-2.5.5-part-mac.tgz ./ - tar zxf minizinc-2.5.5-part-mac.tgz - mv Resources/minizinc Resources/bin/ - cp -r Resources/* $BIN_DIR/minizinc -fi -popd - -rm -rf $SOURCE_DIR - -popd diff --git a/bin/install-ortools.sh b/bin/install-ortools.sh deleted file mode 100755 index e77c88bc..00000000 --- a/bin/install-ortools.sh +++ /dev/null @@ -1,65 +0,0 @@ -name="ortools" -version="9.2" - -echo "" -echo "============= INSTALLING $name ===================" -echo "$name version: $version" - -BIN_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )" - -# minizinc must be installed before ortools -if [ ! -d "$BIN_DIR/minizinc/share/minizinc" ]; then - echo "ERROR: minizinc must be installed in $BIN_DIR first. You can use the install-minizinc.sh script for the installation." - exit 1 -fi - -pushd $BIN_DIR - -OS=$(uname) -if [ "$OS" == "Darwin" ]; then - url="https://github.com/google/or-tools/releases/download/v9.2/or-tools_flatzinc_MacOsX-12.0.1_v9.2.9972.tar.gz" -elif [ "$OS" == "Linux" ]; then - url="https://github.com/google/or-tools/releases/download/v9.2/or-tools_amd64_flatzinc_ubuntu-18.04_v9.2.9972.tar.gz" -else - echo "Cannot determine your OS, uname reports: ${OS}" - exit 1 -fi - -rm -rf $name -mkdir -p $name - -SOURCE_DIR="$name-source" -mkdir -p $SOURCE_DIR - -pushd $SOURCE_DIR -wget $url -tar zxf $(ls *.gz) -d=$(ls -d */) -mv ${d}/* $BIN_DIR/$name -popd - -rm -rf $SOURCE_DIR - -mv $BIN_DIR/$name/bin/fzn-or-tools $BIN_DIR/$name/bin/fzn-ortools - -cp -r $BIN_DIR/$name/share/minizinc $BIN_DIR/minizinc/share/minizinc/$name -CONFIG_FILE="$BIN_DIR/minizinc/share/minizinc/solvers/$name.msc" -cp solver.msc $CONFIG_FILE - -if [ "$OS" == "Darwin" ]; then - sed -i "" "s//$name/g" $CONFIG_FILE - sed -i "" "s//$version/g" $CONFIG_FILE - sed -i "" "s##../../../../$name/bin/fzn-$name#g" $CONFIG_FILE - sed -i "" "s##../$name#g" $CONFIG_FILE -elif [ "$OS" == "Linux" ]; then - sed -i "s//$name/g" $CONFIG_FILE - sed -i "s//$version/g" $CONFIG_FILE - sed -i "s##../../../../$name/bin/fzn-$name#g" $CONFIG_FILE - sed -i "s##../$name#g" $CONFIG_FILE - -else - echo "Cannot determine your OS, uname reports: ${OS}" - exit 1 -fi - -popd diff --git a/bin/install-picat.sh b/bin/install-picat.sh deleted file mode 100755 index e1e13dd5..00000000 --- a/bin/install-picat.sh +++ /dev/null @@ -1,68 +0,0 @@ -name="picat" -version="9.2" - -echo "" -echo "============= INSTALLING $name ===================" -echo "$name version: $version" - -BIN_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )" - -# minizinc must be installed before picat -if [ ! -d "$BIN_DIR/minizinc/share/minizinc" ]; then - echo "ERROR: minizinc must be installed in $BIN_DIR first. You can use the install-minizinc.sh script for the installation." - exit 1 -fi - -pushd $BIN_DIR - -OS=$(uname) -if [ "$OS" == "Darwin" ]; then - url="http://picat-lang.org/download/picat316_macx.tar.gz" -elif [ "$OS" == "Linux" ]; then - url="http://picat-lang.org/download/picat316_linux64.tar.gz" -else - echo "Cannot determine your OS, uname reports: ${OS}" - exit 1 -fi - -mkdir -p $name - -SOURCE_DIR="$name-source" -mkdir -p $SOURCE_DIR - -pushd $SOURCE_DIR - -# download picat binary and lib -wget $url -tar zxf $(ls picat*.gz) -d="Picat" -cp -r $d/lib $d/picat $BIN_DIR/$name/ # TODO: check the macos version - -# download picat flatzinc intepreter -wget https://github.com/nfzhou/fzn_picat/archive/refs/heads/main.zip; unzip main.zip -#wget https://github.com/hakank/fzn_picat/archive/6a12883ace8ab7b4cf94419af5a40139c105a005.zip; unzip 6a12883ace8ab7b4cf94419af5a40139c105a005.zip; mv fzn_picat-6a12883ace8ab7b4cf94419af5a40139c105a005 fzn_picat-main/ -cp -r fzn_picat-main/mznlib $BIN_DIR/minizinc/share/minizinc/$name -cp fzn_picat-main/*.pi $BIN_DIR/$name/ -popd - -rm -rf $SOURCE_DIR - -CONFIG_FILE="$BIN_DIR/minizinc/share/minizinc/solvers/$name.msc" -cp picat.msc $CONFIG_FILE - -if [ "$OS" == "Darwin" ]; then - #sed -i "" "s//$name/g" $CONFIG_FILE - echo "TODO" - exit 1 -elif [ "$OS" == "Linux" ]; then - sed -i "s//$name/g" $CONFIG_FILE - sed -i "s//$version/g" $CONFIG_FILE - #sed -i "s##$BIN_DIR#g" $CONFIG_FILE - #sed -i "s##$BIN_DIR/minizinc/share/minizinc/$name#g" $CONFIG_FILE - -else - echo "Cannot determine your OS, uname reports: ${OS}" - exit 1 -fi - -popd diff --git a/bin/install-runsolver.sh b/bin/install-runsolver.sh deleted file mode 100755 index 446340fa..00000000 --- a/bin/install-runsolver.sh +++ /dev/null @@ -1,32 +0,0 @@ -#!/bin/bash - -#set -x # echo commands -# set -E # exit on any non-zero commands -name="runsolver" - -OS=$(uname) -if [ "$OS" != "Linux" ]; then - echo "${name} only supports Linux, sorry :/" - exit 1 -fi - -echo "" -echo "============= INSTALLING $name ===================" -echo "$name version: $version" - -BIN_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )" - -url="https://www.cril.univ-artois.fr/~roussel/runsolver/runsolver-3.4.0.tar.bz2" - -pushd $BIN_DIR -wget $url -tar xvjf *.bz2 - -pushd $name/src -make - -if test -f "${name}"; then - echo "Installation seems to have run successfully." -else - echo "============= Installation has NOT been successful!!! ===================" -fi diff --git a/bin/install-savilerow.sh b/bin/install-savilerow.sh index 3eb343e2..969d6abf 100755 --- a/bin/install-savilerow.sh +++ b/bin/install-savilerow.sh @@ -1,6 +1,6 @@ # NOTES: minion & chuffed & cadical will also be installed (using binaries provided by savilerow) name="savilerow" -version="1.9.1" # release version on Sep 11, 2021 +version="1.10.1" # release version on 17th October 2024 echo "" diff --git a/bin/install-yuck.sh b/bin/install-yuck.sh deleted file mode 100755 index ce88fee9..00000000 --- a/bin/install-yuck.sh +++ /dev/null @@ -1,50 +0,0 @@ -name="yuck" -version="20210501" - -echo "" -echo "============= INSTALLING $name ===================" -echo "$name version: $version" - -BIN_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )" - -# minizinc must be installed before ortools -if [ ! -d "$BIN_DIR/minizinc/share/minizinc" ]; then - echo "ERROR: minizinc must be installed in $BIN_DIR first. You can use the install-minizinc.sh script for the installation." - exit 1 -fi - -pushd $BIN_DIR - -url="https://github.com/informarte/yuck/releases/download/20210501/yuck-${version}.zip" - -mkdir -p $name - -SOURCE_DIR="$name-source" -mkdir -p $SOURCE_DIR - -pushd $SOURCE_DIR -wget $url --no-check-certificate -d="yuck-${version}" -unzip $d.zip -pushd $d -mv bin/ lib/ doc/ $BIN_DIR/$name -OS=$(uname) -if [ "$OS" == "Darwin" ]; then - sed -i "" "s#../bin/yuck#../../../../$name/bin/yuck#g" mzn/yuck.msc - sed -i "" "s#.*mznlib.*# \"mznlib\": \"../$name\",#g" mzn/yuck.msc -elif [ "$OS" == "Linux" ]; then - sed -i "s#../bin/yuck#../../../../$name/bin/yuck#g" mzn/yuck.msc - sed -i "s#.*mznlib.*# \"mznlib\": \"$BIN_DIR/minizinc/share/minizinc/$name\",#g" mzn/yuck.msc -else - echo "Cannot determine your OS, uname reports: ${OS}" - exit 1 -fi - -cp mzn/yuck.msc $BIN_DIR/minizinc/share/minizinc/solvers/ -mv mzn/lib $BIN_DIR/minizinc/share/minizinc/$name -popd -popd - -rm -rf $SOURCE_DIR - -popd diff --git a/bin/irace-source.zip b/bin/irace-source.zip deleted file mode 100644 index a3fd71e7..00000000 Binary files a/bin/irace-source.zip and /dev/null differ diff --git a/bin/minizinc-2.5.5-part-mac.tgz b/bin/minizinc-2.5.5-part-mac.tgz deleted file mode 100644 index 5bb81673..00000000 Binary files a/bin/minizinc-2.5.5-part-mac.tgz and /dev/null differ diff --git a/bin/picat.msc b/bin/picat.msc deleted file mode 100644 index 91e0ca6f..00000000 --- a/bin/picat.msc +++ /dev/null @@ -1,15 +0,0 @@ -{ "id": "picat", - "name": "picat", - "description": "Picat FlatZinc solver", - "version": "", - "mznlib": "../picat", - "executable": "../../../../run_picat_sat.sh", - "tags": ["sat","int"], - "stdFlags": ["-a","-n","-f"], - "supportsMzn": false, - "supportsFzn": true, - "needsSolns2Out": true, - "needsMznExecutable": false, - "needsStdlibDir": false, - "isGUIApplication": false -} diff --git a/bin/run_picat_sat.sh b/bin/run_picat_sat.sh deleted file mode 100755 index 29ee3180..00000000 --- a/bin/run_picat_sat.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/bash - -BIN_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )" - -# see https://groups.google.com/g/minizinc/c/mBmQL6gXKP0 for more details -picat $BIN_DIR/picat/fzn_picat_sat.pi $* diff --git a/bin/runsolver-3.4.0.tar.bz2 b/bin/runsolver-3.4.0.tar.bz2 deleted file mode 100644 index 82eccc63..00000000 Binary files a/bin/runsolver-3.4.0.tar.bz2 and /dev/null differ diff --git a/bin/set-path.sh b/bin/set-path.sh deleted file mode 100755 index 5828ba8e..00000000 --- a/bin/set-path.sh +++ /dev/null @@ -1,44 +0,0 @@ -# get current script's folder -if [ -n "$ZSH_VERSION" ]; then - BIN_DIR="$( cd "$( dirname "${(%):-%x}" )" &> /dev/null && pwd )" -elif [ -n "$BASH_VERSION" ]; then - BIN_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )" -else - echo "Error: only bash and zsh are supported" - exit 1 -fi - -# AutoIG -export AUTOIG="$(dirname $BIN_DIR)" - -# conjure -export PATH=$BIN_DIR/conjure/:$PATH - -# savilerow -export PATH=$BIN_DIR/savilerow/:$PATH - -# minion -export PATH=$BIN_DIR/minion/:$PATH - -# irace -export PATH=$BIN_DIR/irace/bin:$PATH -export R_LIBS=$BIN_DIR/:$R_LIBS - -# minizinc -export PATH=$BIN_DIR/minizinc/bin/:$PATH -#export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:$BIN_DIR/minizinc/lib -export MZN_SOLVER_PATH=$BIN_DIR/minizinc/share/minizinc/solvers -export MZN_STDLIB_DIR=$BIN_DIR/minizinc/share/minizinc/ - -# ortools -export PATH=$BIN_DIR/ortools/bin/:$PATH -export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:$BIN_DIR/ortools/lib - -# yuck -export PATH=$BIN_DIR/yuck/bin/:$PATH - -# picat -export PATH=$BIN_DIR/picat/:$PATH - -# runsolver -export PATH=$BIN_DIR/runsolver/src/:$PATH diff --git a/bin/solver.msc b/bin/solver.msc deleted file mode 100644 index e1d95e29..00000000 --- a/bin/solver.msc +++ /dev/null @@ -1,15 +0,0 @@ -{ - "id": "", - "name": "", - "version": "", - "description": " FlatZinc executable", - "mznlib": "", - "executable": "", - "stdFlags": ["-a", "-n", "-p", "-f", "-r", "-v", "-l", "-s"], - "supportsMzn": false, - "supportsFzn": true, - "needsSolns2Out": true, - "needsMznExecutable": false, - "needsStdlibDir": false, - "isGUIApplication": false -} diff --git a/data/models/car/car.essence b/data/models/car/car.essence new file mode 100644 index 00000000..eecd8c10 --- /dev/null +++ b/data/models/car/car.essence @@ -0,0 +1,37 @@ +language Essence 1.3 +$ prob001.essence: Car Sequencing +$ Problem details available at http://www.csplib.org/Problems/prob001/ + +given n_cars, n_classes, n_options : int(1..) + +letting Slots be domain int(1..n_cars), + Class be domain int(1..n_classes), + Option be domain int(1..n_options), + +given quantity : function (total) Class --> int(1..), + maxcars : function (total) Option --> int(1..10), + blksize_delta : function (total) Option --> int(1..10), + usage : relation (minSize 1) of ( Class * Option ) + +$ There must be at least as many cars as there are n_classes as quantity is indexed from 1.. +where n_cars >= n_classes + +$ The sum of the cars in the quantity function should equal n_cars +where ( sum quant : Class . quantity(quant) ) = n_cars + +$ Blksize must be greater than maxcars for all options +$ where forAll option: Option . maxcars(option) < blksize(option) + +$ Make sure that all options are used at least once +where forAll option: Option . |toSet(usage(_,option))| >= 1 + +$ Make sure that all classes have at least one option +where forAll class: Class . |toSet(usage(class,_))| >= 1 + +find car : function (total) Slots --> Class + +such that + forAll c : Class . |preImage(car,c)| = quantity(c), + forAll opt : Option . + forAll s : int(1..n_cars+1-(maxcars(opt)+blksize_delta(opt))) . + (sum i : int(s..s+(maxcars(opt)+blksize_delta(opt))-1) . toInt(usage(car(i),opt))) <= maxcars(opt) \ No newline at end of file diff --git a/data/models/car/generator.essence b/data/models/car/generator.essence new file mode 100644 index 00000000..e3549e97 --- /dev/null +++ b/data/models/car/generator.essence @@ -0,0 +1,70 @@ +language Essence 1.3 + +given np_cars_plus: int(1..200) +given np_classes: int(1..200) +given np_options: int(1..200) + +letting np_cars be min({200, np_classes+np_cars_plus}) + +find n_cars, n_classes, n_options: int(1..200) +such that + n_cars = np_cars, + n_classes = np_classes, + n_options = np_options + +where np_cars>=np_classes + +given quantity_range_min: int(1..200) +given quantity_range_delta: int(0..199) +find quantity: function int(1..200) --> int(1..200) + +such that + and([q1 >= 1 /\ q1 <= np_classes <-> q1 in defined(quantity) | q1 : int(1..200)]), + and([q1[2] >= quantity_range_min | q1 <- quantity]), + and([q1[2] <= quantity_range_min + quantity_range_delta | q1 <- quantity]) + +$ The sum of the cars in the quantity function should equal np_cars +such that sum([quantity(quant) | quant : int(1..200), quant <= np_classes]) = np_cars + +$ irace (negated) forbidden constraint +where ((quantity_range_min*np_classes) <= np_cars) +where (quantity_range_min+quantity_range_delta)*np_classes>=np_cars + +given maxcars_range_min: int(1..10) +given maxcars_range_delta: int(0..9) +find maxcars: function int(1..200) --> int(1..10) +such that + and([q2 >= 1 /\ q2 <= np_options <-> q2 in defined(maxcars) | q2 : int(1..200)]), + and([q2[2] >= maxcars_range_min | q2 <- maxcars]), + and([q2[2] <= maxcars_range_min + maxcars_range_delta | q2 <- maxcars]) + +given blksize_delta_range_min: int(1..10) +given blksize_delta_range_delta: int(0..9) +find blksize_delta: function int(1..200) --> int(1..10) +such that + and([q3 >= 1 /\ q3 <= np_options <-> q3 in defined(blksize_delta) | q3 : int(1..200)]), + and([q3[2] >= blksize_delta_range_min | q3 <- blksize_delta]), + and([q3[2] <= blksize_delta_range_min + blksize_delta_range_delta | q3 <- blksize_delta]) + +given usage_card_min: int(0..1000) +given usage_card_delta: int(0..99) +find usage: relation (maxSize 40000) of (int(1..200) * int(1..200)) +such that + |usage| >= usage_card_min /\ |usage| <= usage_card_min + usage_card_delta, + and([q4[1] <= np_classes | q4 <- usage]), + and([q4[2] <= np_options | q4 <- usage]) + +$ irace (negated) forbidden constraint for the validity of cardinality of usage +where (usage_card_min+usage_card_delta)<=(np_classes*np_options) + +$ Make sure that all options are used at least once +such that and([|toSet(usage(_, option))| >= 1 | option : int(1..200), option <= np_options]) + +$ irace (negated) forbidden constraint for the above constraint +where usage_card_min>=np_options + +$ Make sure that all classes have at least one option +such that and([|toSet(usage(class, _))| >= 1 | class : int(1..200), class <= np_classes]) + +$ irace (negated) forbidden constraint for the above constraint +where usage_card_min>=np_classes \ No newline at end of file diff --git a/data/models/car/repair.essence b/data/models/car/repair.essence new file mode 100644 index 00000000..416714ac --- /dev/null +++ b/data/models/car/repair.essence @@ -0,0 +1,95 @@ +language Essence 1.3 + +given np_cars_plus: int(1..200) +given np_classes: int(1..200) +given np_options: int(1..200) +given quantity_range_min: int(1..200) +given quantity_range_delta: int(0..199) +given quantity_range_max: int(1..1000) +given maxcars_range_min: int(1..10) +given maxcars_range_delta: int(0..9) +given maxcars_range_max: int(1..10) +given blksize_delta_range_min: int(1..10) +given blksize_delta_range_delta: int(0..9) +given blksize_delta_range_max: int(1..10) +given usage_card_min: int(0..1000) +given usage_card_delta: int(0..99) +given usage_card_max: int(1..1000) + + + + + + +find repaired_np_cars_plus: int(1..200) +find repaired_np_classes: int(1..200) +find repaired_np_options: int(1..200) +find repaired_quantity_range_min: int(1..200) +find repaired_quantity_range_delta: int(0..199) +find repaired_quantity_range_max: int(1..1000) +find repaired_maxcars_range_min: int(1..10) +find repaired_maxcars_range_delta: int(0..9) +find repaired_maxcars_range_max: int(1..10) +find repaired_blksize_delta_range_min: int(1..10) +find repaired_blksize_delta_range_delta: int(0..9) +find repaired_blksize_delta_range_max: int(1..10) +find repaired_usage_card_min: int(0..1000) +find repaired_usage_card_delta: int(0..99) +find repaired_usage_card_max: int(1..1000) + +such that min({200, repaired_np_classes+repaired_np_cars_plus}) >= repaired_np_classes +$first where done ------------------------------------------------- + + +such that repaired_quantity_range_min <= repaired_quantity_range_max + +such that ((repaired_quantity_range_min*repaired_np_classes) <= min({200, repaired_np_classes+repaired_np_cars_plus})) +such that (repaired_quantity_range_min+repaired_quantity_range_delta)*repaired_np_classes >= min({200, repaired_np_classes+repaired_np_cars_plus}) +$second and third where's done + + + + + + + + +such that (repaired_usage_card_min+repaired_usage_card_delta)<=(repaired_np_classes*repaired_np_options) +such that repaired_usage_card_min >= repaired_np_options +such that repaired_usage_card_min >= repaired_np_classes + + + + + +such that repaired_maxcars_range_min <= repaired_maxcars_range_max + + +such that repaired_blksize_delta_range_min <= repaired_blksize_delta_range_max + + + +such that repaired_usage_card_min <= repaired_usage_card_max + + + + +minimising sum([|repaired_np_cars_plus - np_cars_plus|, + |repaired_np_classes - np_classes|, + |repaired_np_options - np_options|, + |repaired_quantity_range_min - quantity_range_min|, + |repaired_quantity_range_delta - quantity_range_delta|, + |repaired_quantity_range_max - quantity_range_max|, + |repaired_usage_card_min - usage_card_min|, + |repaired_usage_card_delta - usage_card_delta|, + |repaired_usage_card_max - usage_card_max|, + |repaired_maxcars_range_min - maxcars_range_min|, + |repaired_maxcars_range_delta - maxcars_range_delta|, + |repaired_maxcars_range_max - maxcars_range_max|, + |blksize_delta_range_min - repaired_blksize_delta_range_min|, + |blksize_delta_range_delta - repaired_blksize_delta_range_delta|, + |blksize_delta_range_max - repaired_blksize_delta_range_max| + + + + ;int(1..1000)]) diff --git a/data/models/car_problem_only/car-instanceGenerator.essence b/data/models/car_problem_only/car-instanceGenerator.essence new file mode 100644 index 00000000..932c0e00 --- /dev/null +++ b/data/models/car_problem_only/car-instanceGenerator.essence @@ -0,0 +1,61 @@ +language Essence 1.3 + +given n_cars_min: int(1..100) +given n_cars_max: int(1..100) +find n_cars: int(1..100) +such that + n_cars >= n_cars_min, + n_cars <= n_cars_max +given n_classes_min: int(1..100) +given n_classes_max: int(1..100) +find n_classes: int(1..100) +such that + n_classes >= n_classes_min, + n_classes <= n_classes_max +given n_options_min: int(1..100) +given n_options_max: int(1..100) +find n_options: int(1..100) +such that + n_options >= n_options_min, + n_options <= n_options_max +given quantity_range_min: int(1..100) +given quantity_range_max: int(1..100) +find quantity: function int(1..100) --> int(1..100) +such that + and([q1 >= 1 /\ q1 <= n_classes <-> q1 in defined(quantity) | q1 : int(1..100)]), + and([q1[2] >= quantity_range_min | q1 <- quantity]), + and([q1[2] <= quantity_range_max | q1 <- quantity]) +given maxcars_range_min: int(1..10) +given maxcars_range_max: int(1..10) +find maxcars: function int(1..100) --> int(1..10) +such that + and([q2 >= 1 /\ q2 <= n_options <-> q2 in defined(maxcars) | q2 : int(1..100)]), + and([q2[2] >= maxcars_range_min | q2 <- maxcars]), + and([q2[2] <= maxcars_range_max | q2 <- maxcars]) +given blksize_delta_range_min: int(1..10) +given blksize_delta_range_max: int(1..10) +find blksize_delta: function int(1..100) --> int(1..10) +such that + and([q3 >= 1 /\ q3 <= n_options <-> q3 in defined(blksize_delta) | q3 : int(1..100)]), + and([q3[2] >= blksize_delta_range_min | q3 <- blksize_delta]), + and([q3[2] <= blksize_delta_range_max | q3 <- blksize_delta]) +given usage_cardMin: int(1..10000) +given usage_cardMax: int(1..10000) +given usage_relation1_min: int(1..100) +given usage_relation1_max: int(1..100) +given usage_relation2_min: int(1..100) +given usage_relation2_max: int(1..100) +find usage: relation (minSize 1, maxSize 10000) of (int(1..100) * int(1..100)) +such that + |usage| >= usage_cardMin /\ |usage| <= usage_cardMax, + |usage| >= 1, + and([q4[1] >= usage_relation1_min | q4 <- usage]), + and([q4[1] <= usage_relation1_max | q4 <- usage]), + and([q4[1] <= n_classes | q4 <- usage]), + and([q4[2] >= usage_relation2_min | q4 <- usage]), + and([q4[2] <= usage_relation2_max | q4 <- usage]), + and([q4[2] <= n_options | q4 <- usage]) +such that n_cars >= n_classes +such that sum([image(quantity, quant) | quant : int(1..100), quant <= n_classes]) = n_cars +such that and([|toSet(usage(_, option))| >= 1 | option : int(1..100), option <= n_options]) +such that and([|toSet(usage(class, _))| >= 1 | class : int(1..100), class <= n_classes]) diff --git a/data/models/car_problem_only/car-instanceRepair.essence b/data/models/car_problem_only/car-instanceRepair.essence new file mode 100644 index 00000000..5652c5b4 --- /dev/null +++ b/data/models/car_problem_only/car-instanceRepair.essence @@ -0,0 +1,59 @@ +language Essence 1.3 + +given n_cars_min: int(1..100) +given n_cars_max: int(1..100) +find repaired_n_cars_min: int(1..100) +find repaired_n_cars_max: int(1..100) +such that repaired_n_cars_min <= repaired_n_cars_max +given n_classes_min: int(1..100) +given n_classes_max: int(1..100) +find repaired_n_classes_min: int(1..100) +find repaired_n_classes_max: int(1..100) +such that repaired_n_classes_min <= repaired_n_classes_max +given n_options_min: int(1..100) +given n_options_max: int(1..100) +find repaired_n_options_min: int(1..100) +find repaired_n_options_max: int(1..100) +such that repaired_n_options_min <= repaired_n_options_max +given quantity_range_min: int(1..100) +given quantity_range_max: int(1..100) +find repaired_quantity_range_min: int(1..100) +find repaired_quantity_range_max: int(1..100) +such that repaired_quantity_range_min <= repaired_quantity_range_max +given maxcars_range_min: int(1..10) +given maxcars_range_max: int(1..10) +find repaired_maxcars_range_min: int(1..10) +find repaired_maxcars_range_max: int(1..10) +such that repaired_maxcars_range_min <= repaired_maxcars_range_max +given blksize_delta_range_min: int(1..10) +given blksize_delta_range_max: int(1..10) +find repaired_blksize_delta_range_min: int(1..10) +find repaired_blksize_delta_range_max: int(1..10) +such that repaired_blksize_delta_range_min <= repaired_blksize_delta_range_max +given usage_cardMin: int(1..10000) +given usage_cardMax: int(1..10000) +given usage_relation1_min: int(1..100) +given usage_relation1_max: int(1..100) +given usage_relation2_min: int(1..100) +given usage_relation2_max: int(1..100) +find repaired_usage_cardMin: int(1..10000) +find repaired_usage_cardMax: int(1..10000) +find repaired_usage_relation1_min: int(1..100) +find repaired_usage_relation1_max: int(1..100) +find repaired_usage_relation2_min: int(1..100) +find repaired_usage_relation2_max: int(1..100) +such that + repaired_usage_relation1_min <= repaired_usage_relation1_max, + repaired_usage_relation2_min <= repaired_usage_relation2_max +minimising + sum([|repaired_n_cars_min - n_cars_min|, |repaired_n_cars_max - n_cars_max|, + |repaired_n_classes_min - n_classes_min|, |repaired_n_classes_max - n_classes_max|, + |repaired_n_options_min - n_options_min|, |repaired_n_options_max - n_options_max|, + |repaired_quantity_range_min - quantity_range_min|, |repaired_quantity_range_max - quantity_range_max|, + |repaired_maxcars_range_min - maxcars_range_min|, |repaired_maxcars_range_max - maxcars_range_max|, + |repaired_blksize_delta_range_min - blksize_delta_range_min|, + |repaired_blksize_delta_range_max - blksize_delta_range_max|, |repaired_usage_cardMin - usage_cardMin|, + |repaired_usage_cardMax - usage_cardMax|, |repaired_usage_relation1_min - usage_relation1_min|, + |repaired_usage_relation1_max - usage_relation1_max|, |repaired_usage_relation2_min - usage_relation2_min|, + |repaired_usage_relation2_max - usage_relation2_max|; + int(1..18)]) diff --git a/data/models/car_problem_only/car.essence b/data/models/car_problem_only/car.essence new file mode 100644 index 00000000..eecd8c10 --- /dev/null +++ b/data/models/car_problem_only/car.essence @@ -0,0 +1,37 @@ +language Essence 1.3 +$ prob001.essence: Car Sequencing +$ Problem details available at http://www.csplib.org/Problems/prob001/ + +given n_cars, n_classes, n_options : int(1..) + +letting Slots be domain int(1..n_cars), + Class be domain int(1..n_classes), + Option be domain int(1..n_options), + +given quantity : function (total) Class --> int(1..), + maxcars : function (total) Option --> int(1..10), + blksize_delta : function (total) Option --> int(1..10), + usage : relation (minSize 1) of ( Class * Option ) + +$ There must be at least as many cars as there are n_classes as quantity is indexed from 1.. +where n_cars >= n_classes + +$ The sum of the cars in the quantity function should equal n_cars +where ( sum quant : Class . quantity(quant) ) = n_cars + +$ Blksize must be greater than maxcars for all options +$ where forAll option: Option . maxcars(option) < blksize(option) + +$ Make sure that all options are used at least once +where forAll option: Option . |toSet(usage(_,option))| >= 1 + +$ Make sure that all classes have at least one option +where forAll class: Class . |toSet(usage(class,_))| >= 1 + +find car : function (total) Slots --> Class + +such that + forAll c : Class . |preImage(car,c)| = quantity(c), + forAll opt : Option . + forAll s : int(1..n_cars+1-(maxcars(opt)+blksize_delta(opt))) . + (sum i : int(s..s+(maxcars(opt)+blksize_delta(opt))-1) . toInt(usage(car(i),opt))) <= maxcars(opt) \ No newline at end of file diff --git a/data/models/car_problem_only/repair.essence b/data/models/car_problem_only/repair.essence new file mode 100644 index 00000000..934a3e00 --- /dev/null +++ b/data/models/car_problem_only/repair.essence @@ -0,0 +1,59 @@ +language Essence 1.3 + +given n_cars_min: int(1..100) +given n_cars_max: int(1..100) +find repaired_n_cars_min: int(1..100) +find repaired_n_cars_max: int(1..100) +such that repaired_n_cars_min <= repaired_n_cars_max +given n_classes_min: int(1..100) +given n_classes_max: int(1..100) +find repaired_n_classes_min: int(1..100) +find repaired_n_classes_max: int(1..100) +such that repaired_n_classes_min <= repaired_n_classes_max +given n_options_min: int(1..100) +given n_options_max: int(1..100) +find repaired_n_options_min: int(1..100) +find repaired_n_options_max: int(1..100) +such that repaired_n_options_min <= repaired_n_options_max +given quantity_range_min: int(1..100) +given quantity_range_max: int(1..100) +find repaired_quantity_range_min: int(1..100) +find repaired_quantity_range_max: int(1..100) +such that repaired_quantity_range_min <= repaired_quantity_range_max +given maxcars_range_min: int(1..10) +given maxcars_range_max: int(1..10) +find repaired_maxcars_range_min: int(1..10) +find repaired_maxcars_range_max: int(1..10) +such that repaired_maxcars_range_min <= repaired_maxcars_range_max +given blksize_delta_range_min: int(1..10) +given blksize_delta_range_max: int(1..10) +find repaired_blksize_delta_range_min: int(1..10) +find repaired_blksize_delta_range_max: int(1..10) +such that repaired_blksize_delta_range_min <= repaired_blksize_delta_range_max +given usage_cardMin: int(1..10000) +given usage_cardMax: int(1..10000) +given usage_relation1_min: int(1..100) +given usage_relation1_max: int(1..100) +given usage_relation2_min: int(1..100) +given usage_relation2_max: int(1..100) +find repaired_usage_cardMin: int(1..10000) +find repaired_usage_cardMax: int(1..10000) +find repaired_usage_relation1_min: int(1..100) +find repaired_usage_relation1_max: int(1..100) +find repaired_usage_relation2_min: int(1..100) +find repaired_usage_relation2_max: int(1..100) +such that + repaired_usage_relation1_min <= repaired_usage_relation1_max, + repaired_usage_relation2_min <= repaired_usage_relation2_max +minimising + sum([|repaired_n_cars_min - n_cars_min|, |repaired_n_cars_max - n_cars_max|, + |repaired_n_classes_min - n_classes_min|, |repaired_n_classes_max - n_classes_max|, + |repaired_n_options_min - n_options_min|, |repaired_n_options_max - n_options_max|, + |repaired_quantity_range_min - quantity_range_min|, |repaired_quantity_range_max - quantity_range_max|, + |repaired_maxcars_range_min - maxcars_range_min|, |repaired_maxcars_range_max - maxcars_range_max|, + |repaired_blksize_delta_range_min - blksize_delta_range_min|, + |repaired_blksize_delta_range_max - blksize_delta_range_max|, |repaired_usage_cardMin - usage_cardMin|, + |repaired_usage_cardMax - usage_cardMax|, |repaired_usage_relation1_min - usage_relation1_min|, + |repaired_usage_relation1_max - usage_relation1_max|, |repaired_usage_relation2_min - usage_relation2_min|, + |repaired_usage_relation2_max - usage_relation2_max|; + int(1..18)]) diff --git a/data/models/car_problem_only/repair1_json.JSON b/data/models/car_problem_only/repair1_json.JSON new file mode 100644 index 00000000..6ffe48f2 --- /dev/null +++ b/data/models/car_problem_only/repair1_json.JSON @@ -0,0 +1,456 @@ +{"mInfo": + {"finds": [], "givens": [], "enumGivens": [], "enumLettings": [], "lettings": [], "unnameds": [], + "strategyQ": {"Auto": {"Interactive": []}}, "strategyA": {"Auto": {"Interactive": []}}, "trailCompact": [], + "nameGenState": [], "nbExtraGivens": 0, "representations": [], "representationsTree": [], "originalDomains": [], + "trailGeneralised": [], "trailVerbose": [], "trailRewrites": []}, + "mLanguage": {"language": {"Name": "Essence"}, "version": [1, 3]}, + "mStatements": + [{"Declaration": + {"FindOrGiven": + ["Given", {"Name": "n_cars_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "n_cars_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_n_cars_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_n_cars_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"SuchThat": + [{"Op": + {"MkOpLeq": + [{"Reference": [{"Name": "repaired_n_cars_min"}, null]}, + {"Reference": [{"Name": "repaired_n_cars_max"}, null]}]}}]}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "n_classes_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "n_classes_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_n_classes_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_n_classes_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"SuchThat": + [{"Op": + {"MkOpLeq": + [{"Reference": [{"Name": "repaired_n_classes_min"}, null]}, + {"Reference": [{"Name": "repaired_n_classes_max"}, null]}]}}]}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "n_options_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "n_options_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_n_options_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_n_options_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"SuchThat": + [{"Op": + {"MkOpLeq": + [{"Reference": [{"Name": "repaired_n_options_min"}, null]}, + {"Reference": [{"Name": "repaired_n_options_max"}, null]}]}}]}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "quantity_range_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "quantity_range_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_quantity_range_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_quantity_range_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"SuchThat": + [{"Op": + {"MkOpLeq": + [{"Reference": [{"Name": "repaired_quantity_range_min"}, null]}, + {"Reference": [{"Name": "repaired_quantity_range_max"}, null]}]}}]}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "maxcars_range_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "maxcars_range_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_maxcars_range_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_maxcars_range_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10]}}]}]]}]}}, + {"SuchThat": + [{"Op": + {"MkOpLeq": + [{"Reference": [{"Name": "repaired_maxcars_range_min"}, null]}, + {"Reference": [{"Name": "repaired_maxcars_range_max"}, null]}]}}]}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "blksize_delta_range_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "blksize_delta_range_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_blksize_delta_range_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_blksize_delta_range_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10]}}]}]]}]}}, + {"SuchThat": + [{"Op": + {"MkOpLeq": + [{"Reference": [{"Name": "repaired_blksize_delta_range_min"}, null]}, + {"Reference": [{"Name": "repaired_blksize_delta_range_max"}, null]}]}}]}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "usage_cardMin"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10000]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "usage_cardMax"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10000]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "usage_relation1_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "usage_relation1_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "usage_relation2_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "usage_relation2_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_usage_cardMin"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10000]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_usage_cardMax"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10000]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_usage_relation1_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_usage_relation1_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_usage_relation2_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_usage_relation2_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"SuchThat": + [{"Op": + {"MkOpLeq": + [{"Reference": [{"Name": "repaired_usage_relation1_min"}, null]}, + {"Reference": [{"Name": "repaired_usage_relation1_max"}, null]}]}}, + {"Op": + {"MkOpLeq": + [{"Reference": [{"Name": "repaired_usage_relation2_min"}, null]}, + {"Reference": [{"Name": "repaired_usage_relation2_max"}, null]}]}}]}, + {"Objective": + ["Minimising", + {"Op": + {"MkOpSum": + {"AbstractLiteral": + {"AbsLitMatrix": + [{"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 18]}}]}]]}, + [{"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_n_cars_min"}, null]}, + {"Reference": [{"Name": "n_cars_min"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_n_cars_max"}, null]}, + {"Reference": [{"Name": "n_cars_max"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_n_classes_min"}, null]}, + {"Reference": [{"Name": "n_classes_min"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_n_classes_max"}, null]}, + {"Reference": [{"Name": "n_classes_max"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_n_options_min"}, null]}, + {"Reference": [{"Name": "n_options_min"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_n_options_max"}, null]}, + {"Reference": [{"Name": "n_options_max"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_quantity_range_min"}, null]}, + {"Reference": [{"Name": "quantity_range_min"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_quantity_range_max"}, null]}, + {"Reference": [{"Name": "quantity_range_max"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_maxcars_range_min"}, null]}, + {"Reference": [{"Name": "maxcars_range_min"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_maxcars_range_max"}, null]}, + {"Reference": [{"Name": "maxcars_range_max"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": + [{"Name": "repaired_blksize_delta_range_min"}, null]}, + {"Reference": [{"Name": "blksize_delta_range_min"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": + [{"Name": "repaired_blksize_delta_range_max"}, null]}, + {"Reference": [{"Name": "blksize_delta_range_max"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_usage_cardMin"}, null]}, + {"Reference": [{"Name": "usage_cardMin"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_usage_cardMax"}, null]}, + {"Reference": [{"Name": "usage_cardMax"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_usage_relation1_min"}, null]}, + {"Reference": [{"Name": "usage_relation1_min"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_usage_relation1_max"}, null]}, + {"Reference": [{"Name": "usage_relation1_max"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_usage_relation2_min"}, null]}, + {"Reference": [{"Name": "usage_relation2_min"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_usage_relation2_max"}, null]}, + {"Reference": + [{"Name": "usage_relation2_max"}, null]}]}}}}]]}}}}]}]} diff --git a/data/models/car_problem_only/repair2_json.JSON b/data/models/car_problem_only/repair2_json.JSON new file mode 100644 index 00000000..6ffe48f2 --- /dev/null +++ b/data/models/car_problem_only/repair2_json.JSON @@ -0,0 +1,456 @@ +{"mInfo": + {"finds": [], "givens": [], "enumGivens": [], "enumLettings": [], "lettings": [], "unnameds": [], + "strategyQ": {"Auto": {"Interactive": []}}, "strategyA": {"Auto": {"Interactive": []}}, "trailCompact": [], + "nameGenState": [], "nbExtraGivens": 0, "representations": [], "representationsTree": [], "originalDomains": [], + "trailGeneralised": [], "trailVerbose": [], "trailRewrites": []}, + "mLanguage": {"language": {"Name": "Essence"}, "version": [1, 3]}, + "mStatements": + [{"Declaration": + {"FindOrGiven": + ["Given", {"Name": "n_cars_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "n_cars_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_n_cars_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_n_cars_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"SuchThat": + [{"Op": + {"MkOpLeq": + [{"Reference": [{"Name": "repaired_n_cars_min"}, null]}, + {"Reference": [{"Name": "repaired_n_cars_max"}, null]}]}}]}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "n_classes_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "n_classes_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_n_classes_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_n_classes_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"SuchThat": + [{"Op": + {"MkOpLeq": + [{"Reference": [{"Name": "repaired_n_classes_min"}, null]}, + {"Reference": [{"Name": "repaired_n_classes_max"}, null]}]}}]}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "n_options_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "n_options_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_n_options_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_n_options_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"SuchThat": + [{"Op": + {"MkOpLeq": + [{"Reference": [{"Name": "repaired_n_options_min"}, null]}, + {"Reference": [{"Name": "repaired_n_options_max"}, null]}]}}]}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "quantity_range_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "quantity_range_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_quantity_range_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_quantity_range_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"SuchThat": + [{"Op": + {"MkOpLeq": + [{"Reference": [{"Name": "repaired_quantity_range_min"}, null]}, + {"Reference": [{"Name": "repaired_quantity_range_max"}, null]}]}}]}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "maxcars_range_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "maxcars_range_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_maxcars_range_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_maxcars_range_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10]}}]}]]}]}}, + {"SuchThat": + [{"Op": + {"MkOpLeq": + [{"Reference": [{"Name": "repaired_maxcars_range_min"}, null]}, + {"Reference": [{"Name": "repaired_maxcars_range_max"}, null]}]}}]}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "blksize_delta_range_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "blksize_delta_range_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_blksize_delta_range_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_blksize_delta_range_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10]}}]}]]}]}}, + {"SuchThat": + [{"Op": + {"MkOpLeq": + [{"Reference": [{"Name": "repaired_blksize_delta_range_min"}, null]}, + {"Reference": [{"Name": "repaired_blksize_delta_range_max"}, null]}]}}]}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "usage_cardMin"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10000]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "usage_cardMax"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10000]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "usage_relation1_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "usage_relation1_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "usage_relation2_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Given", {"Name": "usage_relation2_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_usage_cardMin"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10000]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_usage_cardMax"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 10000]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_usage_relation1_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_usage_relation1_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_usage_relation2_min"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"Declaration": + {"FindOrGiven": + ["Find", {"Name": "repaired_usage_relation2_max"}, + {"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 100]}}]}]]}]}}, + {"SuchThat": + [{"Op": + {"MkOpLeq": + [{"Reference": [{"Name": "repaired_usage_relation1_min"}, null]}, + {"Reference": [{"Name": "repaired_usage_relation1_max"}, null]}]}}, + {"Op": + {"MkOpLeq": + [{"Reference": [{"Name": "repaired_usage_relation2_min"}, null]}, + {"Reference": [{"Name": "repaired_usage_relation2_max"}, null]}]}}]}, + {"Objective": + ["Minimising", + {"Op": + {"MkOpSum": + {"AbstractLiteral": + {"AbsLitMatrix": + [{"DomainInt": + [{"TagInt": []}, + [{"RangeBounded": + [{"Constant": {"ConstantInt": [{"TagInt": []}, 1]}}, + {"Constant": {"ConstantInt": [{"TagInt": []}, 18]}}]}]]}, + [{"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_n_cars_min"}, null]}, + {"Reference": [{"Name": "n_cars_min"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_n_cars_max"}, null]}, + {"Reference": [{"Name": "n_cars_max"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_n_classes_min"}, null]}, + {"Reference": [{"Name": "n_classes_min"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_n_classes_max"}, null]}, + {"Reference": [{"Name": "n_classes_max"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_n_options_min"}, null]}, + {"Reference": [{"Name": "n_options_min"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_n_options_max"}, null]}, + {"Reference": [{"Name": "n_options_max"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_quantity_range_min"}, null]}, + {"Reference": [{"Name": "quantity_range_min"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_quantity_range_max"}, null]}, + {"Reference": [{"Name": "quantity_range_max"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_maxcars_range_min"}, null]}, + {"Reference": [{"Name": "maxcars_range_min"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_maxcars_range_max"}, null]}, + {"Reference": [{"Name": "maxcars_range_max"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": + [{"Name": "repaired_blksize_delta_range_min"}, null]}, + {"Reference": [{"Name": "blksize_delta_range_min"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": + [{"Name": "repaired_blksize_delta_range_max"}, null]}, + {"Reference": [{"Name": "blksize_delta_range_max"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_usage_cardMin"}, null]}, + {"Reference": [{"Name": "usage_cardMin"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_usage_cardMax"}, null]}, + {"Reference": [{"Name": "usage_cardMax"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_usage_relation1_min"}, null]}, + {"Reference": [{"Name": "usage_relation1_min"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_usage_relation1_max"}, null]}, + {"Reference": [{"Name": "usage_relation1_max"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_usage_relation2_min"}, null]}, + {"Reference": [{"Name": "usage_relation2_min"}, null]}]}}}}, + {"Op": + {"MkOpTwoBars": + {"Op": + {"MkOpMinus": + [{"Reference": [{"Name": "repaired_usage_relation2_max"}, null]}, + {"Reference": + [{"Name": "usage_relation2_max"}, null]}]}}}}]]}}}}]}]} diff --git a/data/models/simple/simple.mzn b/data/models/simple/simple.mzn new file mode 100644 index 00000000..77474384 --- /dev/null +++ b/data/models/simple/simple.mzn @@ -0,0 +1,9 @@ +int: a; % Input a +var -3..30: x; +var 0..6: y; +var -10..100000: z; + +constraint x = a; +constraint pow(x, y) = z; + +solve satisfy; \ No newline at end of file diff --git a/data/models/simple/simple_gen.essence b/data/models/simple/simple_gen.essence new file mode 100644 index 00000000..6b51525e --- /dev/null +++ b/data/models/simple/simple_gen.essence @@ -0,0 +1,5 @@ +given A: int(1..1000) + +find a: int(1..1000) +such that +a = A \ No newline at end of file diff --git a/data/models/simple_e/generator.essence b/data/models/simple_e/generator.essence new file mode 100644 index 00000000..6b51525e --- /dev/null +++ b/data/models/simple_e/generator.essence @@ -0,0 +1,5 @@ +given A: int(1..1000) + +find a: int(1..1000) +such that +a = A \ No newline at end of file diff --git a/data/models/simple_e/problem.essence b/data/models/simple_e/problem.essence new file mode 100644 index 00000000..56207dbe --- /dev/null +++ b/data/models/simple_e/problem.essence @@ -0,0 +1,12 @@ +given a : int +letting xDomain be domain int(-3..30) +letting yDomain be domain int(0..6) +letting zDomain be domain int(-10..100000) + +find x : xDomain +find y : yDomain +find z : zDomain + +such that + x = a, + z = x*y \ No newline at end of file diff --git a/data/models/vessel-loading/generator.essence b/data/models/vessel-loading/generator.essence new file mode 100644 index 00000000..f009c046 --- /dev/null +++ b/data/models/vessel-loading/generator.essence @@ -0,0 +1,31 @@ +given deck_width_tuned, deck_length_tuned: int(1..100) +given n_containers_delta: int(1..20) +given n_classes_tuned: int(1..10) + +find deck_width, deck_length, n_containers, n_classes: int(1..100) +such that + deck_width = deck_width_tuned, + deck_length = deck_length_tuned, + n_containers = n_classes_tuned + n_containers_delta, + n_classes = n_classes_tuned + +letting Container be domain int(1..(n_containers_delta + n_classes_tuned)), + Class be domain int(1..n_classes_tuned), + Width be domain int(1..deck_width_tuned), + Length be domain int(1..deck_length_tuned) + +find width : function (total) Container --> Width, + length : function (total) Container --> Length, + class : function (total) Container --> Class, + separation : function (maxSize 3) set (size 2) of Class --> int(1..max([deck_width_tuned, deck_length_tuned])) + +$ how much area coverage of the deck that the total container sizes take up +given coverage_max: int(10..100) +letting min_total_size be 10 * deck_width_tuned * deck_length_tuned / 100 +letting max_total_size be coverage_max * deck_width_tuned * deck_length_tuned / 100 +such that + min_total_size <= (sum c : Container . width(c)*length(c)), + max_total_size >= (sum c : Container . width(c)*length(c)), + +such that (sum c : Container . width(c)*length(c)) <= deck_width*deck_length +such that |range(class)| = n_classes diff --git a/data/models/vessel-loading/problem.essence b/data/models/vessel-loading/problem.essence new file mode 100755 index 00000000..18ea0422 --- /dev/null +++ b/data/models/vessel-loading/problem.essence @@ -0,0 +1,73 @@ +language ESSENCE 1.2.0 +$ prob008.essence: Vessel Loading +$ Problem details available at http://www.csplib.org/Problems/prob008/ +$ 25 July 2007 +$ + +$ deck_width : the width of the ship deck +$ deck_length : the length of the ship deck +$ n_containers : the number of containers +$ n_classes : the number of container classes +given deck_width, deck_length, n_containers, n_classes : int(1..) + +$ Container : containers are represented as an integer between 1 and n_containers +$ Class : classes are represented as an integer between 1 and n_classes +$ Width : a container width may be between 1 and the width of the deck +$ Length : a container length may be between 1 and the length of the deck +$ X: a position on x-axis (width) of the deck +$ Y: a position on y-axis (length) of the deck +letting Container be domain int(1..n_containers), + Class be domain int(1..n_classes), + Width be domain int(1..deck_width), + Length be domain int(1..deck_length), + X be domain int(0..deck_width), + Y be domain int(0..deck_length) + +$ width : a container's width +$ length : a container's length +$ class : a container's class +$ separation: the minimum allowed separation between two container classes +given width : function (total) Container --> Width, + length : function (total) Container --> Length, + class : function (total) Container --> Class, + separation : function (maxSize 3) set (size 2) of Class --> int(1..max([deck_width, deck_length])) + +$ total container sizes must not exceed the deck's area size +where (sum c : Container . width(c)*length(c)) <= deck_width*deck_length + +$ Enforce that every class has at least one container +$where |range(class)| = n_classes + +$ west : the x coordinate of a container's western edge +$ north : the y coordinate of a container's northern edge +$ east : the x coordinate of a container's eastern edge +$ south : the y coordinate of a container's southern edge +find west, east : function (total) Container --> X, + north, south : function (total) Container --> Y + +such that +$ all north, east, south & west coordinates are valid according to the given +$ width and length parameters + forAll c : Container . (east(c) - west(c) = width(c) /\ + south(c) - north(c) = length(c)) \/ + (east(c) - west(c) = length(c) /\ + south(c) - north(c) = width(c)) + +such that +$ no two containers occupy the same space + forAll c1, c2 : Container . c1 != c2 -> west(c1) != west(c2) \/ + north(c1) != north(c2) + +such that +$ containers do not overlap each other + forAll c1, c2 : Container . c1 != c2 -> + max({west(c1), west(c2)}) - min({east(c1), east(c2)}) >= 0 \/ + max({north(c1), north(c2)}) - min({south(c1), south(c2)}) >= 0 + +such that + $container placement meets the class separation constraints + forAll c1, c2 : Container . c1 < c2 /\ {class(c1), class(c2)} in defined(separation)-> + max({west(c1), west(c2)}) - min({east(c1), east(c2)}) + >= separation({class(c1), class(c2)}) \/ + max({north(c1), north(c2)}) - min({south(c1), south(c2)}) + >= separation({class(c1), class(c2)}) diff --git a/scripts/__pycache__/conf.cpython-310.pyc b/scripts/__pycache__/conf.cpython-310.pyc new file mode 100644 index 00000000..bcdc3f61 Binary files /dev/null and b/scripts/__pycache__/conf.cpython-310.pyc differ diff --git a/scripts/__pycache__/convert.cpython-310.pyc b/scripts/__pycache__/convert.cpython-310.pyc new file mode 100644 index 00000000..7fadccd5 Binary files /dev/null and b/scripts/__pycache__/convert.cpython-310.pyc differ diff --git a/scripts/__pycache__/essence_pipeline_utils.cpython-310.pyc b/scripts/__pycache__/essence_pipeline_utils.cpython-310.pyc new file mode 100644 index 00000000..16eeda60 Binary files /dev/null and b/scripts/__pycache__/essence_pipeline_utils.cpython-310.pyc differ diff --git a/scripts/__pycache__/generator.cpython-310.pyc b/scripts/__pycache__/generator.cpython-310.pyc new file mode 100644 index 00000000..b0f8abd5 Binary files /dev/null and b/scripts/__pycache__/generator.cpython-310.pyc differ diff --git a/scripts/__pycache__/minizinc_utils.cpython-310.pyc b/scripts/__pycache__/minizinc_utils.cpython-310.pyc new file mode 100644 index 00000000..35a3695d Binary files /dev/null and b/scripts/__pycache__/minizinc_utils.cpython-310.pyc differ diff --git a/scripts/__pycache__/utils.cpython-310.pyc b/scripts/__pycache__/utils.cpython-310.pyc new file mode 100644 index 00000000..6c9b5006 Binary files /dev/null and b/scripts/__pycache__/utils.cpython-310.pyc differ diff --git a/scripts/collect_results.py b/scripts/collect_results.py index 42877a1d..8ef7c806 100644 --- a/scripts/collect_results.py +++ b/scripts/collect_results.py @@ -10,6 +10,7 @@ scriptDir = os.path.dirname(os.path.realpath(__file__)) sys.path.append(scriptDir) +# this is for mnz from minizinc_utils import calculate_minizinc_borda_scores, get_minizinc_problem_type pd.options.mode.chained_assignment = None @@ -38,13 +39,31 @@ def read_data(runDir): config = read_config(configFile) + # Read in the file + with open(detailedResultsFile, 'r') as file: + filedata = file.read() + +# Replace the target string + filedata = filedata.replace('insttance', 'instance') + +# Write the file out again + with open(detailedResultsFile, 'w') as file: + file.write(filedata) + + # read detailed-results.json with open(detailedResultsFile, "rt") as f: #lsLines = [s[:-1] for s in f.readlines() if s.startswith('{"totalTime"')] lsLines = [s.replace("\n","") for s in f.readlines() if "totalTime" in s] + # lsLines = [s.replace("insttance","instance") for s in f.readlines()] r = [ast.literal_eval(s) for s in lsLines] + + tRs = pd.DataFrame(r) + tRs["score"] = tRs["score"].astype(float) + + # move generator instance names into a separate column tRs.loc[:,"genInstance"] = [s["instance"] for s in tRs.genResults] diff --git a/scripts/essence_pipeline_utils.py b/scripts/essence_pipeline_utils.py index 9b0f2248..d3b63ba0 100644 --- a/scripts/essence_pipeline_utils.py +++ b/scripts/essence_pipeline_utils.py @@ -64,6 +64,12 @@ "timelimitPrefix": "--time=", "randomSeedPrefix": "--seed=", } +solverInfo["ortools"] = { + "timelimitUnit": "ms", # OR Tools time is in MS + "timelimitPrefix": "--time-limit ", + "randomSeedPrefix": "-r ", +} + def conjure_translate_parameter(eprimeModelFile, paramFile, eprimeParamFile): @@ -102,11 +108,11 @@ def savilerow_translate( + flags ) log(cmd) - + start = time.time() cmdOutput, returnCode = run_cmd(cmd) SRTime = time.time() - start - + status = "SRok" # if returnCode !=0, check if it is because SR is out of memory or timeout if ( @@ -422,6 +428,7 @@ def call_conjure_solve(essenceModelFile, eprimeModelFile, instFile, setting, see ): status = "solverCrash" elif returnCode != 0: + print("GETTING TO HERE") raise Exception(cmdOutput) baseFile = ( @@ -481,7 +488,8 @@ def call_conjure_solve(essenceModelFile, eprimeModelFile, instFile, setting, see # parse SR info file infoStatus, SRTime, solverTime = parse_SR_info_file( - infoFile, timelimit=setting["solverTimeLimit"] + infoFile, timelimit=3 + # timelimit=setting["solverTimeLimit"] ) if status != "solverCrash": status = infoStatus @@ -538,4 +546,4 @@ def get_val(field): status = "sat" else: status = "unsat" - return status, SRTime, solverTime + return status, SRTime, solverTime \ No newline at end of file diff --git a/scripts/extract-md5sum.sh b/scripts/extract-md5sum.sh index 4029e010..fcc657b4 100755 --- a/scripts/extract-md5sum.sh +++ b/scripts/extract-md5sum.sh @@ -1,7 +1,7 @@ outFile="instance-md5sum.csv" echo "instance,hashValue">$outFile -for fn in $(ls inst-*.dzn) +for fn in $(ls inst-*.param) do if [ "$(uname)" == "Darwin" ]; then val=$(md5 $fn| cut -d"=" -f2 |xargs) diff --git a/scripts/repair.essence b/scripts/repair.essence new file mode 100644 index 00000000..934a3e00 --- /dev/null +++ b/scripts/repair.essence @@ -0,0 +1,59 @@ +language Essence 1.3 + +given n_cars_min: int(1..100) +given n_cars_max: int(1..100) +find repaired_n_cars_min: int(1..100) +find repaired_n_cars_max: int(1..100) +such that repaired_n_cars_min <= repaired_n_cars_max +given n_classes_min: int(1..100) +given n_classes_max: int(1..100) +find repaired_n_classes_min: int(1..100) +find repaired_n_classes_max: int(1..100) +such that repaired_n_classes_min <= repaired_n_classes_max +given n_options_min: int(1..100) +given n_options_max: int(1..100) +find repaired_n_options_min: int(1..100) +find repaired_n_options_max: int(1..100) +such that repaired_n_options_min <= repaired_n_options_max +given quantity_range_min: int(1..100) +given quantity_range_max: int(1..100) +find repaired_quantity_range_min: int(1..100) +find repaired_quantity_range_max: int(1..100) +such that repaired_quantity_range_min <= repaired_quantity_range_max +given maxcars_range_min: int(1..10) +given maxcars_range_max: int(1..10) +find repaired_maxcars_range_min: int(1..10) +find repaired_maxcars_range_max: int(1..10) +such that repaired_maxcars_range_min <= repaired_maxcars_range_max +given blksize_delta_range_min: int(1..10) +given blksize_delta_range_max: int(1..10) +find repaired_blksize_delta_range_min: int(1..10) +find repaired_blksize_delta_range_max: int(1..10) +such that repaired_blksize_delta_range_min <= repaired_blksize_delta_range_max +given usage_cardMin: int(1..10000) +given usage_cardMax: int(1..10000) +given usage_relation1_min: int(1..100) +given usage_relation1_max: int(1..100) +given usage_relation2_min: int(1..100) +given usage_relation2_max: int(1..100) +find repaired_usage_cardMin: int(1..10000) +find repaired_usage_cardMax: int(1..10000) +find repaired_usage_relation1_min: int(1..100) +find repaired_usage_relation1_max: int(1..100) +find repaired_usage_relation2_min: int(1..100) +find repaired_usage_relation2_max: int(1..100) +such that + repaired_usage_relation1_min <= repaired_usage_relation1_max, + repaired_usage_relation2_min <= repaired_usage_relation2_max +minimising + sum([|repaired_n_cars_min - n_cars_min|, |repaired_n_cars_max - n_cars_max|, + |repaired_n_classes_min - n_classes_min|, |repaired_n_classes_max - n_classes_max|, + |repaired_n_options_min - n_options_min|, |repaired_n_options_max - n_options_max|, + |repaired_quantity_range_min - quantity_range_min|, |repaired_quantity_range_max - quantity_range_max|, + |repaired_maxcars_range_min - maxcars_range_min|, |repaired_maxcars_range_max - maxcars_range_max|, + |repaired_blksize_delta_range_min - blksize_delta_range_min|, + |repaired_blksize_delta_range_max - blksize_delta_range_max|, |repaired_usage_cardMin - usage_cardMin|, + |repaired_usage_cardMax - usage_cardMax|, |repaired_usage_relation1_min - usage_relation1_min|, + |repaired_usage_relation1_max - usage_relation1_max|, |repaired_usage_relation2_min - usage_relation2_min|, + |repaired_usage_relation2_max - usage_relation2_max|; + int(1..18)]) diff --git a/scripts/setup.py b/scripts/setup.py index b9cc779a..5d7e8874 100755 --- a/scripts/setup.py +++ b/scripts/setup.py @@ -42,6 +42,10 @@ def read_config(args): "minSolverTime", "maxSolverTime", "nRunsPerInstance", + "SRTimeLimit", + "SRFlags", + "solverTimeLimit", + "solverFlags", ] # read common settings for both graded/discriminating experiments @@ -149,6 +153,7 @@ def setup(config): ) # rename repair spec + # flagvp: this is the part where it will create a repair model oldRepairModelFile = problemModelFile.replace( ".essence", "-instanceRepair.essence" ) @@ -345,6 +350,18 @@ def main(): parser.add_argument( "--nRunsPerInstance", default=1, type=int, help="number of runs per instance" ) + parser.add_argument( + "--SRTimeLimit", default=1, type=int, help="savile row time limit" + ) + parser.add_argument( + "--SRFlags", default="", help="savile row flags" + ) + parser.add_argument( + "--solverTimeLimit", default=1, type=int, help="sover time limit" + ) + + + # instance setting (for graded experiment only) parser.add_argument( diff --git a/scripts/target-runner b/scripts/target-runner index b169673c..041c83ce 100755 --- a/scripts/target-runner +++ b/scripts/target-runner @@ -13,9 +13,8 @@ reRunExistingButFailedOutput='1' outfn="detailed-output/out-${candId}-${seed}" -function checkScore -{ - score="$(echo $1|cut -d' ' -f 1)" +function checkScore { + score="$(echo $1 | cut -d' ' -f 1)" re='^-?[0-9]+([.][0-9]+)?e?[+-]?([0-9]+)?$' if ! [[ ${score} =~ $re ]] && [[ ${score} != "Inf" ]]; then return 1 @@ -26,16 +25,16 @@ function checkScore # if output file already exists but its last line isn't a valid tuning results, re-run it reRun='0' if [ -f $outfn ]; then - rs="$(tail -n 1 ${outfn})" + rs="$(tail -n 1 ${outfn})" checkScore "$rs" reRun="$?" fi # run command -if [ ! -f $outfn ] || [ "${reRun}" = "1" ] ; then - scriptDir="$( cd "$( dirname "${BASH_SOURCE[0]}"; )" >/dev/null 2>&1 && pwd )" +if [ ! -f $outfn ] || [ "${reRun}" = "1" ]; then + scriptDir="$(cd "$(dirname "${BASH_SOURCE[0]}")" >/dev/null 2>&1 && pwd)" cmd="python3 -u $scriptDir/wrapper.py $@ > ${outfn} 2>&1" - #echo $cmd + # echo $cmd eval $cmd fi @@ -44,8 +43,9 @@ rs="$(tail -n 1 ${outfn})" checkScore "$rs" failed="$?" if [[ "${failed}" == "1" ]]; then - #echo "Inf" - echo "Error! ${rs}" + echo "$rs" + echo "Inf" + echo "Error!" else - echo "$rs" + echo "$rs" fi diff --git a/scripts/test_repair.txt b/scripts/test_repair.txt new file mode 100644 index 00000000..93c88042 --- /dev/null +++ b/scripts/test_repair.txt @@ -0,0 +1,80 @@ +import json +import os +import argparse +import subprocess + +def main(): + + parser = argparse.ArgumentParser( + description="Starting generating repaid models:" + ) + + # getting directory of the problem model + parser.add_argument( + "--problemDir", + type=str, + help="location of the essence problem", + required=True + ) + args = parser.parse_args() + path = args.problemDir + if not os.path.isdir(path): + print(f"Error: The directory '{path}' does not exist.") + else: + files = os.listdir(path) + + + # the path of the specific problem in that direcory + if files: + for i in files: + if i.find(".essence"): + problemPath = os.path.join(path, files[0]) + + + # creating the generator and the repair using conjure + command = "conjure parameter-generator " + command += str(problemPath) + subprocess.run(command, shell=True, capture_output=True, text=True) + command = "rm " + str(path) + "/*.irace" + subprocess.run(command, shell=True, capture_output=True, text=True) + files = os.listdir(path) + for i in files: + if i.find("Generator.essence"): + generator = i + + # this is the command which creates the second repair file, which is not implemented in conjure yet + command = "conjure repair-generator " + str(path) + "/"+str(generator) + # print(command) + # res = subprocess.run(command, shell=True, capture_output=True, text=True) + + + + # for now instead of using the repair generated by the command above we will use our own one (repair.essence) which is stored in the scripts directory + command = "cp repair.essence " + str(path) + subprocess.run(command, shell=True, capture_output=True, text=True) + files = os.listdir(path) + for i in files: + if i.find("Repair.essence")!=-1: + repairFile1 = i + if i.find("repair.essence")!=-1: + repairFile2 = i + + + # transform both repairs into JSON and compare them + command = "conjure pretty "+ str(path)+"/"+str(repairFile1)+" --output-format=astjson > "+ str(path) + "/repair1_json.JSON" + subprocess.run(command, shell=True, capture_output=True, text=True) + with open(str(path) + "/repair1_json.JSON", 'r') as f: + r1 = json.load(f) + command = "conjure pretty "+ str(path)+"/"+str(repairFile2)+" --output-format=astjson > "+ str(path) + "/repair2_json.JSON" + subprocess.run(command, shell=True, capture_output=True, text=True) + with open(str(path) + "/repair2_json.JSON", 'r') as f: + r2 = json.load(f) + if r1==r2: + print("same") + else: + print("different") + + +main() + + \ No newline at end of file diff --git a/scripts/wrapper.py b/scripts/wrapper.py index 37024d72..a5cdf27b 100755 --- a/scripts/wrapper.py +++ b/scripts/wrapper.py @@ -159,7 +159,7 @@ def get_results(): # make final score if score != None: - return score + return score, get_results() # - otherwise, for each evaluation: if the run is too easy: score=-solverTime, if the run is graded: score=nEvaluations*-solverMinTime score = 0 for i in range(len(lsSolverTime)): @@ -225,6 +225,7 @@ def get_results(): + ")" ) + #flagvp: current source of the issue for discriminating instances runStatus, SRTime, solverTime = call_conjure_solve( essenceModelFile, eprimeModelFile, instFile, solverSetting, rndSeed ) @@ -905,6 +906,10 @@ def read_setting(settingFile): c["evaluationSettings"]["nEvaluations"] = setting["nRunsPerInstance"] c["evaluationSettings"]["gradedTypes"] = setting["instanceValidTypes"] + c["evaluationSettings"]["SRTimeLimit"] = setting["SRTimeLimit"] + c["evaluationSettings"]["SRFlags"] = setting["SRFlags"] + c["evaluationSettings"]["solverTimeLimit"] = setting["solverTimeLimit"] + c["evaluationSettings"]["solverFlags"] = setting["solverFlags"] if setting["instanceSetting"] == "graded": c["evaluationSettings"]["solver"] = setting["solver"] if setting["solver"] in ["yuck"]: @@ -923,11 +928,17 @@ def read_setting(settingFile): "solverMinTime": setting["minSolverTime"], "totalTimeLimit": setting["maxSolverTime"], "solverFlags": setting["baseSolverFlags"], + "SRTimeLimit": setting["SRTimeLimit"], + "SRFlags": setting["SRFlags"], + "solverTimeLimit": setting["solverTimeLimit"], } favouredSolverSettings = { "name": setting["favouredSolver"], "totalTimeLimit": setting["maxSolverTime"], "solverFlags": setting["favouredSolverFlags"], + "SRTimeLimit": setting["SRTimeLimit"], + "SRFlags": setting["SRFlags"], + "solverTimeLimit": setting["solverTimeLimit"], } c["evaluationSettings"]["baseSolver"] = baseSolverSettings @@ -959,6 +970,10 @@ def print_results(): # if results['genResults']['status']=='sat': # assert results['instanceResults']!={} totalWrapperTime = time.time() - startTime + # my pc is a potato so I was getting negaive time..... + # remove them when running on a better pc + if totalWrapperTime<0: + totalWrapperTime*=totalWrapperTime results["totalTime"] = totalWrapperTime results["status"] = status results["score"] = score @@ -1028,10 +1043,14 @@ def get_unwanted_types(): # evaluate the generated instance if modelType == "essence": + # MOD evaluationFunctionName = "evaluate_" + modelType + "_instance_" + experimentType + score, instanceResults = globals()[evaluationFunctionName]( instFile, seed, setting["evaluationSettings"] ) + + else: # convert the generated instance into .dzn mznInstFile = instFile.replace(".param", ".dzn") @@ -1111,4 +1130,4 @@ def get_unwanted_types(): # - inst unwanted type or SR timeout/memout (either solver) or solver crash (either solver): 1 # - favoured solver timeout (any run) or base solver too easy (any run): 0 # - otherwise: max{-minRatio, -badSolver/goodSolver} -# - note: timelimit_badSolver = minRatio * timelimit_goodSolver +# - note: timelimit_badSolver = minRatio * timelimit_goodSolver \ No newline at end of file