|
Size: 3711
Comment:
|
Size: 7865
Comment:
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 10: | Line 10: |
| * whether the team will participates to the system or to the model competition, or both. | * whether the team will participate to the system or model competition, or both. |
| Line 17: | Line 17: |
| Your home directory in the Competition server contains a subdirectory ''submitted''. | Your home directory in the Competition server contains a subdirectory {{{submitted}}}. |
| Line 19: | Line 19: |
| The content of the {{{submitted}}} directory depends on whether your team is participating to the system or model competition. | |
| Line 20: | Line 21: |
| The ''submitted'' directory contains a subdirectory for each benchmark. | '''IMPORTANT:''' The {{{submitted}}} directory will be accessible only after the benchmark submission closure. During the benchmark submission phase, participants will be provided with a {{{try}}} directory, structured as {{{submitted}}}. This directory can be used for testing systems and benchmark encodings. === Model Competition === If your team is participating to the model competition, your {{{submitted}}} directory contains a subdirectory for each benchmark. |
| Line 22: | Line 30: |
| In particular, there must be a file ''run'', which will be invoked during the Competition. | In particular, there must be a file {{{run}}}, which will be invoked during the Competition. |
| Line 24: | Line 32: |
| All files invoked by ''run'' must be placed in the directory containing the ''run'' file, or in one of its subdirectories. | All files invoked by {{{run}}} must be placed in the directory containing the {{{run}}} file, or in one of its subdirectories. |
| Line 26: | Line 34: |
| During the Competition, the ''run'' file will be invoked with two command-line arguments. | During the Competition, the {{{run}}} file will be invoked with two command-line arguments. |
| Line 32: | Line 40: |
| Below is an example of {{{run}}} script. | |
| Line 33: | Line 42: |
| In addition to the subdirectories for benchmarks, the ''submitted'' directory also contains a subdirectory ''System'' for the system competition. Even in this case, the ''run'' file will be invoked during the Competition. A third additional arguments will be specified in the command-line, which will be a comma-separated list of predicate names. These predicates must be used for representing witnessing models of satisfiable instances; the extensions of these predicates must be printed in standard output. Examples of scripts will be provided in the ''System'' directory. |
{{{ # !/usr/bin/env bash |
| Line 39: | Line 45: |
| The submission process will be performed by properly invoking the ''submit'' tool. This tool requires a command-line parameter specifying either ''System'' or the name of a directory containing a benchmark solution (just the name, not the complete path). Once a system or a benchmark are submitted, any modification to the associated directories is prevented. At any time, a participant can invoke the ''unsubmit'' tool to retire a submitted directory and get back the grant of modifying its content. |
set -o pipefail # Disable output buffering |
| Line 44: | Line 47: |
| === Examples === | if [ $# -ne 2 ]; then echo "This script must be invoked with two parameters!" exit -1 fi |
| Line 46: | Line 52: |
| To submit your ''System'' directory, just write: | MAXINT=$1 MAX_NESTING_LEVEL=$2 # NOTE: MAX_NESTING_LEVEL is not used in this version of DLV |
| Line 48: | Line 55: |
| '''$ submit System''' | SCRIPTDIR=`dirname $0` BIN=$SCRIPTDIR/dlv.i386-linux-elf-static.bin ENCODING=$SCRIPTDIR/myProblem1.dl OUTPUT_PREDICATES=path |
| Line 50: | Line 60: |
| The ''System'' directory is no more editable. To undo your submission, type: | # Execution with preprocessing and postprocessing: $SCRIPTDIR/preprocess.pl | $BIN -N=$MAXINT -filter=$OUTPUT_PREDICATES -n=1 -silent $ENCODING -- | $SCRIPTDIR/postprocess.pl |
| Line 52: | Line 63: |
| '''$ unsubmit System''' | ECODE=$? if [ $ECODE -ne 0 ]; then echo UNKNOWN; fi exit $ECODE }}} |
| Line 54: | Line 70: |
| ---- | Note that, in the above script, {{{DLV}}} is invoked after a pre-processing perl script. The output of {{{DLV}}} is processed by a perl post-processing script. Your binary executable might not require a pre-processing script, in which case the following instruction can be used in the script: {{{ # Execution with postprocessing only: $BIN -N=$MAXINT -filter=$OUTPUT_PREDICATES -n=1 -silent $ENCODING -- | $SCRIPTDIR/postprocess.pl }}} Similarly, if your binary executable does not require a post-processing script, the following instruction can be used in the script: {{{ # Execution with preprocessing only: $SCRIPTDIR/preprocess.pl | $BIN -N=$MAXINT -filter=$OUTPUT_PREDICATES -n=1 -silent $ENCODING -- }}} |
| Line 57: | Line 87: |
| '''IMPORTANT:''' The ''submitted'' directory will be accessible only after the benchmark submission closure. During the benchmark submission phase, participants will be provided with a ''try'' directory, structured as ''submitted''. This directory can be used for testing systems and benchmark encodings. |
=== System Competition === If your team is participating to the model competition, your {{{submitted}}} directory contains a subdirectory {{{System}}}. This directory must comprise all files required for running your system. In particular, there must be a file {{{run}}}, which will be invoked during the Competition. This file can be a script invoking a binary executable, possibly using other scripts for pre- or post-processing. All files invoked by {{{run}}} must be placed in the directory containing the {{{run}}} file, or in one of its subdirectories. Moreover, only relative paths must be used in all scripts; note that this is a strong requirement, since the Competition would be executed on a different machine. During the Competition, the {{{run}}} file will be invoked with three command-line arguments. The first argument is the maximum integer which is sufficient for solving the input instance. The second argument is the maximum nesting level of function symbols which is sufficient for solving the input instance. The third argument will be specified in the command-line, which will be a comma-separated list of predicate names. These predicates must be used for representing witnessing models of satisfiable instances; the extensions of these predicates must be printed in standard output. Each of these arguments can be passed to the binary executable or just ignored. Instances will be provided via standard input. The output must be printed in standard output, according to the format specified in the benchmark description. Examples of scripts will be provided in the {{{System}}} directory. Below is an example of {{{run}}} script. {{{ # !/usr/bin/env bash set -o pipefail # Disable output buffering if [ $# -ne 3 ]; then echo "This script must be invoked with three parameters!" exit fi MAXINT=$1 MAX_NESTING_LEVEL=$2 # NOTE: MAX_NESTING_LEVEL is not used in this version of DLV OUTPUT_PREDICATES=$3 SCRIPTDIR=`dirname $0` BIN=$SCRIPTDIR/dlv.i386-linux-elf-static.bin # Execution with preprocessing and postprocessing: $SCRIPTDIR/preprocess.pl | $BIN -N=$MAXINT -filter=$OUTPUT_PREDICATES -n=1 -silent -- | $SCRIPTDIR/postprocess.pl ECODE=$? if [ $ECODE -ne 0 ]; then echo UNKNOWN; fi exit $ECODE }}} Note that, in the above script, {{{DLV}}} is invoked after a pre-processing perl script. The output of {{{DLV}}} is processed by a perl post-processing script. Your binary executable might not require a pre-processing script, in which case the following instruction can be used in the script: {{{ # Execution with postprocessing only: $BIN -N=$MAXINT -filter=$OUTPUT_PREDICATES -n=1 -silent -- | $SCRIPTDIR/postprocess.pl }}} Similarly, if your binary executable does not require a post-processing script, the following instruction can be used in the script: {{{ # Execution with preprocessing only: $SCRIPTDIR/preprocess.pl | $BIN -N=$MAXINT -filter=$OUTPUT_PREDICATES -n=1 -silent -- }}} === Submission Process === The submission process will be performed by properly invoking the {{{submit}}} tool. This tool requires a command-line parameter specifying either {{{System}}} or the name of a directory containing a benchmark solution (just the name, not the complete path). Once a system or a benchmark are submitted, any modification to the associated directories is prevented. At any time, a participant can invoke the {{{unsubmit}}} tool to retire a submitted directory and get back the grant of modifying its content. ==== Examples ==== To submit your {{{System}}} directory, just write: {{{ $ submit System }}} The {{{System}}} directory will be no more editable. To undo your submission, type: {{{ $ unsubmit System }}} |
Participant submission procedure
Application
To register for the competition, send an email to aspcomp2011 _at_ mat.unical.it specifying:
- the name of your team;
- names and affiliation of the participants (institution, research group);
- whether the team will participate to the system or model competition, or both.
As soon as you will get credentials for entering the Competition server, you will get a Linux home directory having a folder structure described next. A sample home directory tree can be found here.
Instructions for testing and submitting systems and benchmarks
Your home directory in the Competition server contains a subdirectory submitted. Only files in this directory will be processed during the Competition. The content of the submitted directory depends on whether your team is participating to the system or model competition.
IMPORTANT: The submitted directory will be accessible only after the benchmark submission closure. During the benchmark submission phase, participants will be provided with a try directory, structured as submitted. This directory can be used for testing systems and benchmark encodings.
Model Competition
If your team is participating to the model competition, your submitted directory contains a subdirectory for each benchmark. Each of these directories must comprise all files required for solving a specific benchmark. In particular, there must be a file run, which will be invoked during the Competition. This file can be a script invoking a binary executable, possibly using other scripts for pre- or post-processing. All files invoked by run must be placed in the directory containing the run file, or in one of its subdirectories. Moreover, only relative paths must be used in all scripts; note that this is a strong requirement, since the Competition would be executed on a different machine. During the Competition, the run file will be invoked with two command-line arguments. The first argument is the maximum integer which is sufficient for solving the input instance. The second argument is the maximum nesting level of function symbols which is sufficient for solving the input instance. These arguments can be passed to the binary executable or just ignored. Instances will be provided via standard input. The output must be printed in standard output, according to the format specified in the benchmark description. Examples of scripts will be provided in each benchmark directory. Below is an example of run script.
# !/usr/bin/env bash
set -o pipefail # Disable output buffering
if [ $# -ne 2 ]; then
echo "This script must be invoked with two parameters!"
exit -1
fi
MAXINT=$1
MAX_NESTING_LEVEL=$2 # NOTE: MAX_NESTING_LEVEL is not used in this version of DLV
SCRIPTDIR=`dirname $0`
BIN=$SCRIPTDIR/dlv.i386-linux-elf-static.bin
ENCODING=$SCRIPTDIR/myProblem1.dl
OUTPUT_PREDICATES=path
# Execution with preprocessing and postprocessing:
$SCRIPTDIR/preprocess.pl | $BIN -N=$MAXINT -filter=$OUTPUT_PREDICATES -n=1 -silent $ENCODING -- | $SCRIPTDIR/postprocess.pl
ECODE=$?
if [ $ECODE -ne 0 ]; then
echo UNKNOWN;
fi
exit $ECODENote that, in the above script, DLV is invoked after a pre-processing perl script. The output of DLV is processed by a perl post-processing script. Your binary executable might not require a pre-processing script, in which case the following instruction can be used in the script:
# Execution with postprocessing only: $BIN -N=$MAXINT -filter=$OUTPUT_PREDICATES -n=1 -silent $ENCODING -- | $SCRIPTDIR/postprocess.pl
Similarly, if your binary executable does not require a post-processing script, the following instruction can be used in the script:
# Execution with preprocessing only: $SCRIPTDIR/preprocess.pl | $BIN -N=$MAXINT -filter=$OUTPUT_PREDICATES -n=1 -silent $ENCODING --
System Competition
If your team is participating to the model competition, your submitted directory contains a subdirectory System. This directory must comprise all files required for running your system. In particular, there must be a file run, which will be invoked during the Competition. This file can be a script invoking a binary executable, possibly using other scripts for pre- or post-processing. All files invoked by run must be placed in the directory containing the run file, or in one of its subdirectories. Moreover, only relative paths must be used in all scripts; note that this is a strong requirement, since the Competition would be executed on a different machine. During the Competition, the run file will be invoked with three command-line arguments. The first argument is the maximum integer which is sufficient for solving the input instance. The second argument is the maximum nesting level of function symbols which is sufficient for solving the input instance. The third argument will be specified in the command-line, which will be a comma-separated list of predicate names. These predicates must be used for representing witnessing models of satisfiable instances; the extensions of these predicates must be printed in standard output. Each of these arguments can be passed to the binary executable or just ignored. Instances will be provided via standard input. The output must be printed in standard output, according to the format specified in the benchmark description. Examples of scripts will be provided in the System directory. Below is an example of run script.
# !/usr/bin/env bash
set -o pipefail # Disable output buffering
if [ $# -ne 3 ]; then
echo "This script must be invoked with three parameters!"
exit
fi
MAXINT=$1
MAX_NESTING_LEVEL=$2 # NOTE: MAX_NESTING_LEVEL is not used in this version of DLV
OUTPUT_PREDICATES=$3
SCRIPTDIR=`dirname $0`
BIN=$SCRIPTDIR/dlv.i386-linux-elf-static.bin
# Execution with preprocessing and postprocessing:
$SCRIPTDIR/preprocess.pl | $BIN -N=$MAXINT -filter=$OUTPUT_PREDICATES -n=1 -silent -- | $SCRIPTDIR/postprocess.pl
ECODE=$?
if [ $ECODE -ne 0 ]; then
echo UNKNOWN;
fi
exit $ECODENote that, in the above script, DLV is invoked after a pre-processing perl script. The output of DLV is processed by a perl post-processing script. Your binary executable might not require a pre-processing script, in which case the following instruction can be used in the script:
# Execution with postprocessing only: $BIN -N=$MAXINT -filter=$OUTPUT_PREDICATES -n=1 -silent -- | $SCRIPTDIR/postprocess.pl
Similarly, if your binary executable does not require a post-processing script, the following instruction can be used in the script:
# Execution with preprocessing only: $SCRIPTDIR/preprocess.pl | $BIN -N=$MAXINT -filter=$OUTPUT_PREDICATES -n=1 -silent --
Submission Process
The submission process will be performed by properly invoking the submit tool. This tool requires a command-line parameter specifying either System or the name of a directory containing a benchmark solution (just the name, not the complete path). Once a system or a benchmark are submitted, any modification to the associated directories is prevented. At any time, a participant can invoke the unsubmit tool to retire a submitted directory and get back the grant of modifying its content.
Examples
To submit your System directory, just write:
$ submit System
The System directory will be no more editable. To undo your submission, type:
$ unsubmit System