Attachment 'solversoptions.txt'
Download 1 ----------------------------- clasp-mt/bin/run ----------------------------
2 #!/bin/bash
3 if [ $# -ne 3 ]; then
4 echo "This script must be invoked with three parameters!"
5 exit
6 fi
7
8 SOLVER=clasp
9 GROUNDER=gringo
10 OPTIONS="-t8"
11
12 MAXINT=$1
13 MAX_NESTING_LEVEL=$2
14 OUTP="$3"
15 SCRIPTDIR=`dirname $0`
16 CLASP="${SCRIPTDIR}/${SOLVER}"
17 GRINGO="${SCRIPTDIR}/${GROUNDER}"
18
19
20 trap ":" 24 15
21 $GRINGO --foobar="$OUTP" | $CLASP --outf=1 -q1,1 $OPTIONS
22 declare -a retvals=( "${PIPESTATUS[@]}" )
23 test ${retvals[0]} -gt 0 && exit ${retvals[0]} || exit ${retvals[1]}
24
25 ----------------------------- clasp-st/bin/run ----------------------------
26 #!/bin/bash
27 if [ $# -ne 3 ]; then
28 echo "This script must be invoked with three parameters!"
29 exit
30 fi
31
32 SOLVER=clasp
33 GROUNDER=gringo
34 OPTIONS="--opt-heuristic=3 --reset-restarts=1 --restart-on-model --opt-strategy=5"
35
36 MAXINT=$1
37 MAX_NESTING_LEVEL=$2
38 OUTP="$3"
39 SCRIPTDIR=`dirname $0`
40 CLASP="${SCRIPTDIR}/${SOLVER}"
41 GRINGO="${SCRIPTDIR}/${GROUNDER}"
42
43
44 trap ":" 24 15
45 $GRINGO --foobar="$OUTP" | $CLASP --outf=1 -q1,1 $OPTIONS
46 declare -a retvals=( "${PIPESTATUS[@]}" )
47 test ${retvals[0]} -gt 0 && exit ${retvals[0]} || exit ${retvals[1]}
48
49 ----------------------------- lp2bv2+boolector/bin/run ----------------------------
50 #!/bin/bash
51
52 # Wrapper script for LP2ACYC + ACYC2BV + BOOLECTOR
53
54 if test $# -ne 3
55 then
56 echo "The script $0 must be invoked with three parameters!"
57 exit 128
58 fi
59
60 trap ":" 24 15
61
62 BIN=`dirname $0`
63 TMP=${MAIN%%/bin}/tmp
64
65 symfile=$TMP/$$-symbols.sm
66 outfile=$TMP/$$-output.txt
67
68 gringo-aspcomp2014 --foobar="$3" 2>/dev/null \
69 | $BIN/lpstrip-1.8 2>/dev/null \
70 | $BIN/lpcat-1.25 -s=$symfile 2>/dev/null \
71 | $BIN/lpshift-1.2 2>/dev/null \
72 | $BIN/lp2normal2-1.7 -k 2>/dev/null \
73 | $BIN/lp2acyc-1.12 2>/dev/null \
74 | $BIN/acyc2solver-1.5 --bv 2>/dev/null \
75 | fgrep -v get-model \
76 | $BIN/boolector-1.6.0 --smt2 -m 2>/dev/null >$outfile
77
78 declare -a rvals=("${PIPESTATUS[@]}")
79
80 if test ${rvals[0]} -ne 0
81 then
82 echo "Grounding error!"
83 exit 128
84 fi
85
86 for i in 1 2 3 4 5 6
87 do
88 if test ${rvals[$i]} -ne 0
89 then
90 echo "UNKNOWN"
91 exit 1
92 fi
93 done
94
95 $BIN/judge $symfile $outfile ${rvals[8]}
96 rval=$?
97
98 exit $rval
99 ----------------------------- lp2graph/bin/run ----------------------------
100 #!/bin/bash
101
102 # Wrapper script for LP2GRAPH
103
104 if test $# -ne 3
105 then
106 echo "The script $0 must be invoked with three parameters!"
107 exit 128
108 fi
109
110 trap ":" 24 15
111
112 BIN=`dirname $0`
113 TMP=${BIN%%/bin}/tmp
114
115 unid=`hostname -s`-$$
116 symfile=$TMP/$unid-symbols.sm
117 outfile=$TMP/$unid-output.txt
118
119 gringo-aspcomp2014 --foobar="$3" 2>/dev/null \
120 | $BIN/lpstrip-1.8 2>/dev/null \
121 | $BIN/lpcat-1.25 -s=$symfile 2>/dev/null \
122 | $BIN/lpshift-1.2 2>/dev/null \
123 | $BIN/lp2normal2-1.7 2>/dev/null \
124 | $BIN/lp2acyc-1.12 2>/dev/null \
125 | $BIN/lp2sat-1.20 -g 2>/dev/null \
126 | $BIN/acycglucose_simp /dev/stdin $outfile 1>/dev/null 2>/dev/null
127
128 declare -a rvals=("${PIPESTATUS[@]}")
129
130 if test ${rvals[0]} -ne 0
131 then
132 echo "Grounding error!"
133 exit 128
134 fi
135
136 for i in 1 2 3 4 5 6
137 do
138 if test ${rvals[$i]} -ne 0
139 then
140 echo "UNKNOWN"
141 exit 1
142 fi
143 done
144
145 $BIN/judge $symfile $outfile ${rvals[7]}
146 rval=$?
147
148 exit $rval
149 ----------------------------- lp2maxsat+clasp/bin/run ----------------------------
150 #!/bin/bash
151
152 # Wrapper script for LP2ACYC + LP2SAT + CLASP
153
154 if test $# -ne 3
155 then
156 echo "The script $0 must be invoked with three parameters!"
157 exit 128
158 fi
159
160 trap ":" 24 15
161
162 BIN=`dirname $0`
163 TMP=${BIN%%/bin}/tmp
164
165 unid=`hostname -s`-$$
166 symfile=$TMP/$unid-symbols.sm
167 outfile=$TMP/$unid-output.txt
168
169 gringo-aspcomp2014 --foobar="$3" 2>/dev/null \
170 | $BIN/lpstrip-1.8 2>/dev/null \
171 | $BIN/lpcat-1.25 -s=$symfile 2>/dev/null \
172 | $BIN/lpshift-1.2 2>/dev/null \
173 | $BIN/lp2normal2-1.7 -ko 2>/dev/null \
174 | $BIN/lp2acyc-1.12 2>/dev/null \
175 | $BIN/lp2sat-1.24 -b 2>/dev/null \
176 | $BIN/clasp-2.1.5 --config=trendy --quiet=1,1 2>/dev/null >$outfile
177
178 declare -a rvals=("${PIPESTATUS[@]}")
179
180 if test ${rvals[0]} -ne 0
181 then
182 echo "Grounding error!"
183 exit 128
184 fi
185
186 for i in 1 2 3 4 5 6
187 do
188 if test ${rvals[$i]} -ne 0
189 then
190 echo "UNKNOWN"
191 exit 1
192 fi
193 done
194
195 $BIN/judge $symfile $outfile ${rvals[7]}
196 rval=$?
197
198 exit $rval
199 ----------------------------- lp2mip2/bin/run ----------------------------
200 #!/bin/bash
201
202 # Wrapper script for LP2ACYC + ACYC2MIP + CPLEX (optimizing)
203
204 if test $# -ne 3
205 then
206 echo "The script $0 must be invoked with three parameters!"
207 exit 128
208 fi
209
210 trap ":" 24 15
211
212 BIN=`dirname $0`
213 TMP=${BIN%%/bin}/tmp
214
215 unid=`hostname -s`-$$
216 symfile=$TMP/$unid-symbols.sm
217 infile=$TMP/$unid-input.lp
218 outfile=$TMP/$unid-output.txt
219
220 gringo-aspcomp2014 --foobar="$3" 2>/dev/null \
221 | $BIN/lpstrip-1.8 2>/dev/null \
222 | $BIN/lpcat-1.25 -s=$symfile 2>/dev/null \
223 | $BIN/lpshift-1.2 2>/dev/null \
224 | $BIN/lp2normal2-1.7 -ko 2>/dev/null \
225 | $BIN/lp2acyc-1.12 2>/dev/null \
226 | $BIN/acyc2solver-1.5 --mip 2>/dev/null >$infile
227
228 declare -a rvals=("${PIPESTATUS[@]}")
229
230 if test ${rvals[0]} -ne 0
231 then
232 echo "Grounding error!"
233 rm -f $symfile $infile
234 exit 128
235 fi
236
237 for i in 1 2 3 4 5
238 do
239 if test ${rvals[$i]} -ne 0
240 then
241 echo "UNKNOWN"
242 rm -f $symfile $infile
243 exit 1
244 fi
245 done
246
247 if test "`head -2 $infile | tail -1`" = ""
248 then
249 let opt=0
250 else
251 let opt=1
252 fi
253
254 wd=`pwd`
255 cd $TMP
256 ( echo "read "$infile; \
257 echo "set threads 1"; \
258 echo "optimize"; \
259 echo "display solution variables var_*" ) \
260 | cplex > $outfile 2>/dev/null
261 rval=$?
262 cd $wd
263 rm -f $infile
264 rm -f $TMP/cplex.log
265 rm -f $TMP/clone*.log
266
267 if test $rval -ne 0
268 then
269 echo "UNKNOWN"
270 exit 1
271 fi
272
273 $BIN/judge $symfile $outfile $opt
274 rval=$?
275
276 exit $rval
277 ----------------------------- lp2mip2-mt/bin/run ----------------------------
278 #!/bin/bash
279
280 # Wrapper script for LP2ACYC + ACYC2SOLVER + CPLEX (6 threads, optimizing)
281
282 if test $# -ne 3
283 then
284 echo "The script $0 must be invoked with three parameters!"
285 exit 128
286 fi
287
288 trap ":" 24 15
289
290 BIN=`dirname $0`
291 TMP=${BIN%%/bin}/tmp
292
293 unid=`hostname -s`-$$
294 symfile=$TMP/$unid-symbols.sm
295 infile=$TMP/$unid-input.lp
296 outfile=$TMP/$unid-output.txt
297
298 gringo-aspcomp2014 --foobar="$3" 2>/dev/null \
299 | $BIN/lpstrip-1.8 2>/dev/null \
300 | $BIN/lpcat-1.25 -s=$symfile 2>/dev/null \
301 | $BIN/lpshift-1.2 2>/dev/null \
302 | $BIN/lp2normal2-1.7 -ko 2>/dev/null \
303 | $BIN/lp2acyc-1.12 2>/dev/null \
304 | $BIN/acyc2solver-1.5 --mip 2>/dev/null >$infile
305
306 declare -a rvals=("${PIPESTATUS[@]}")
307
308 if test ${rvals[0]} -ne 0
309 then
310 echo "Grounding error!"
311 rm -f $symfile $infile
312 exit 128
313 fi
314
315 for i in 1 2 3 4 5
316 do
317 if test ${rvals[$i]} -ne 0
318 then
319 echo "UNKNOWN"
320 rm -f $symfile $infile
321 exit 1
322 fi
323 done
324
325 if test "`head -2 $infile | tail -1`" = ""
326 then
327 let opt=0
328 else
329 let opt=1
330 fi
331
332 wd=`pwd`
333 cd $TMP
334 ( echo "read "$infile; \
335 echo "set threads 6"; \
336 echo "optimize"; \
337 echo "display solution variables var_*" ) \
338 | cplex > $outfile 2>/dev/null
339 rval=$?
340 cd $wd
341 rm -f $infile
342 rm -f $TMP/cplex.log
343 rm -f $TMP/clone*.log
344
345 if test $rval -ne 0
346 then
347 echo "UNKNOWN"
348 exit 1
349 fi
350
351 $BIN/judge $symfile $outfile $opt
352 rval=$?
353
354 exit $rval
355 ----------------------------- lp2normal2+clasp/bin/run ----------------------------
356 #!/bin/bash
357
358 # Wrapper script for LP2NORMAL2 (1.5) + CLASP (3.0.3)
359
360 if test $# -ne 3
361 then
362 echo "The script $0 must be invoked with three parameters!"
363 exit 128
364 fi
365
366 trap ":" 24 15
367
368 BIN=`dirname $0`
369
370 gringo-aspcomp2014 --foobar="$3" 2>/dev/null \
371 | $BIN/lp2normal2-1.7 -k \
372 -cR-if "1000 < n * (log k) * (log (n - k + 1))" \
373 -wR-if "x = n * (1 + log(w/n)); 10000 < x * (log x)^2" \
374 -oqn 2>/dev/null \
375 | $BIN/igen-1.7 2>/dev/null \
376 | $BIN/clasp-3.0.3 --config=trendy --outf=1 -V0
377
378 declare -a rvals=("${PIPESTATUS[@]}")
379
380 if test ${rvals[0]} -ne 0
381 then
382 echo "Grounding error!"
383 exit 128
384 fi
385
386 for i in 1 2
387 do
388 if test ${rvals[$i]} -ne 0
389 then
390 echo "UNKNOWN"
391 exit 1
392 fi
393 done
394
395 exit ${rvals[3]}
396 ----------------------------- lp2sat3+glucose/bin/run ----------------------------
397 #!/bin/bash
398
399 # Wrapper script for LP2ACYC + LP2SAT + GLUCOSE
400
401 if test $# -ne 3
402 then
403 echo "The script $0 must be invoked with three parameters!"
404 exit 128
405 fi
406
407 trap ":" 24 15
408
409 BIN=`dirname $0`
410 TMP=${BIN%%/bin}/tmp
411
412 unid=`hostname -s`-$$
413 symfile=$TMP/$unid-symbols.sm
414 outfile=$TMP/$unid-output.txt
415
416 gringo-aspcomp2014 --foobar="$3" 2>/dev/null \
417 | $BIN/lpstrip-1.8 2>/dev/null \
418 | $BIN/lpcat-1.25 -s=$symfile 2>/dev/null \
419 | $BIN/lpshift-1.2 2>/dev/null \
420 | $BIN/lp2normal2-1.7 2>/dev/null \
421 | $BIN/lp2acyc-1.12 2>/dev/null \
422 | $BIN/lp2sat-1.20 -b 2>/dev/null \
423 | $BIN/glucose-3.0 /dev/stdin $outfile 1>/dev/null 2>/dev/null
424
425 declare -a rvals=("${PIPESTATUS[@]}")
426
427 if test ${rvals[0]} -ne 0
428 then
429 echo "Grounding error!"
430 exit 128
431 fi
432
433 for i in 1 2 3 4 5 6
434 do
435 if test ${rvals[$i]} -ne 0
436 then
437 echo "UNKNOWN"
438 exit 1
439 fi
440 done
441
442 $BIN/judge $symfile $outfile ${rvals[7]}
443 rval=$?
444
445 exit $rval
446 ----------------------------- lp2sat3+lingeling/bin/run ----------------------------
447 #!/bin/bash
448
449 # Wrapper script for LP2ACYC + LP2SAT + LINGELING
450
451 if test $# -ne 3
452 then
453 echo "The script $0 must be invoked with three parameters!"
454 exit 128
455 fi
456
457 trap ":" 24 15
458
459 BIN=`dirname $0`
460 TMP=${BIN%%/bin}/tmp
461
462 unid=`hostname -s`-$$
463 symfile=$TMP/$unid-symbols.sm
464 outfile=$TMP/$unid-output.txt
465
466 gringo-aspcomp2014 --foobar="$3" 2>/dev/null \
467 | $BIN/lpstrip-1.8 2>/dev/null \
468 | $BIN/lpcat-1.25 -s=$symfile 2>/dev/null \
469 | $BIN/lpshift-1.2 2>/dev/null \
470 | $BIN/lp2normal2-1.7 2>/dev/null \
471 | $BIN/lp2acyc-1.12 2>/dev/null \
472 | $BIN/lp2sat-1.20 -b 2>/dev/null \
473 | $BIN/lingeling-ayi 2>/dev/null >$outfile
474
475 declare -a rvals=("${PIPESTATUS[@]}")
476
477 if test ${rvals[0]} -ne 0
478 then
479 echo "Grounding error!"
480 exit 128
481 fi
482
483 for i in 1 2 3 4 5 6
484 do
485 if test ${rvals[$i]} -ne 0
486 then
487 echo "UNKNOWN"
488 exit 1
489 fi
490 done
491
492 $BIN/judge $symfile $outfile ${rvals[7]}
493 rval=$?
494
495 exit $rval
496 ----------------------------- lp2sat3+plingeling-mt/bin/run ----------------------------
497 #!/bin/bash
498
499 # Wrapper script for LP2ACYC + LP2SAT + LINGELING
500
501 if test $# -ne 3
502 then
503 echo "The script $0 must be invoked with three parameters!"
504 exit 128
505 fi
506
507 trap ":" 24 15
508
509 BIN=`dirname $0`
510 TMP=${BIN%%/bin}/tmp
511
512 unid=`hostname -s`-$$
513 symfile=$TMP/$unid-symbols.sm
514 outfile=$TMP/$unid-output.txt
515
516 gringo-aspcomp2014 --foobar="$3" 2>/dev/null \
517 | $BIN/lpstrip-1.8 2>/dev/null \
518 | $BIN/lpcat-1.25 -s=$symfile 2>/dev/null \
519 | $BIN/lpshift-1.2 2>/dev/null \
520 | $BIN/lp2normal2-1.7 2>/dev/null \
521 | $BIN/lp2acyc-1.12 2>/dev/null \
522 | $BIN/lp2sat-1.20 -b 2>/dev/null \
523 | $BIN/plingeling-ayi -t 6 2>/dev/null >$outfile
524
525 declare -a rvals=("${PIPESTATUS[@]}")
526
527 if test ${rvals[0]} -ne 0
528 then
529 echo "Grounding error!"
530 exit 128
531 fi
532
533 for i in 1 2 3 4 5 6
534 do
535 if test ${rvals[$i]} -ne 0
536 then
537 echo "UNKNOWN"
538 exit 1
539 fi
540 done
541
542 $BIN/judge $symfile $outfile ${rvals[7]}
543 rval=$?
544
545 exit $rval
546 ----------------------------- wasp1.5/bin/run ----------------------------
547 #!/bin/bash
548 if [ $# -ne 3 ]; then
549 echo "This script must be invoked with three parameters!"
550 exit
551 fi
552
553 MAXINT=$1
554 MAX_NESTING_LEVEL=$2
555 OUTP="$3"
556 PIPE=/tmp/wasppipe_$$
557 SCRIPTDIR=`dirname $0`
558
559 $SCRIPTDIR/selector --stdin --selector=$$ --silent | $SCRIPTDIR/run2 $PIPE $MAXINT $MAX_NESTING_LEVEL $OUTP
560 declare -a retvals=( "${PIPESTATUS[@]}" )
561 test ${retvals[0]} -gt 0 && exit ${retvals[0]} || exit ${retvals[1]}
562
563 ----------------------------- wasp1/bin/run ----------------------------
564 #!/usr/bin/env bash
565 # by Mario Alviano
566
567 set -o pipefail # Disable output buffering
568
569 if [ $# -ne 3 ]; then
570 echo "This script must be invoked with three parameters!"
571 exit
572 fi
573
574 MAXINT=$1
575 MAX_NESTING_LEVEL=$2 # NOTE: MAX_NESTING_LEVEL is not used in this version of DLV
576 OUTPUT_PREDICATES=$3
577
578 SCRIPTDIR=`dirname $0`
579 BIN=$SCRIPTDIR/dlv
580 WASP=$SCRIPTDIR/wasp1
581
582 $BIN -- -nofinitecheck -pfilter=$OUTPUT_PREDICATES | $WASP --heuristic-berkmin=512 --competition-output
583 ECODE=$?
584
585 exit $ECODE
586 ----------------------------- wasp2/bin/run ----------------------------
587 #!/usr/bin/env bash
588 # by Mario Alviano
589
590 set -o pipefail # Disable output buffering
591
592 if [ $# -ne 3 ]; then
593 echo "This script must be invoked with three parameters!"
594 exit
595 fi
596
597 MAXINT=$1
598 MAX_NESTING_LEVEL=$2 # NOTE: MAX_NESTING_LEVEL is not used in this version of DLV
599 OUTPUT_PREDICATES=$3
600
601 SCRIPTDIR=`dirname $0`
602 BIN=gringo-aspcomp2014
603 WASP=$SCRIPTDIR/wasp
604
605 $BIN --foobar="$OUTPUT_PREDICATES" | $WASP --competition-output
606 ECODE=$?
607
608 exit $ECODE
609 ----------------------------- wasp_wmsu1_only_weak/bin/run ----------------------------
610 #!/usr/bin/env bash
611 # by Mario Alviano
612
613 set -o pipefail # Disable output buffering
614
615 if [ $# -ne 3 ]; then
616 echo "This script must be invoked with three parameters!"
617 exit
618 fi
619
620 MAXINT=$1
621 MAX_NESTING_LEVEL=$2 # NOTE: MAX_NESTING_LEVEL is not used in this version of DLV
622 OUTPUT_PREDICATES=$3
623
624 SCRIPTDIR=`dirname $0`
625 BIN=$SCRIPTDIR/dlv
626 WASP=$SCRIPTDIR/wasp1
627
628 $BIN -- -nofinitecheck -pfilter=$OUTPUT_PREDICATES | $WASP --heuristic-berkmin=512 --wmsu1 --competition-output
629 ECODE=$?
630
631 exit $ECODE
632 ----------------------------- wasp_wpm1_only_weak/bin/run ----------------------------
633 #!/usr/bin/env bash
634 # by Mario Alviano
635
636 set -o pipefail # Disable output buffering
637
638 if [ $# -ne 3 ]; then
639 echo "This script must be invoked with three parameters!"
640 exit
641 fi
642
643 MAXINT=$1
644 MAX_NESTING_LEVEL=$2 # NOTE: MAX_NESTING_LEVEL is not used in this version of DLV
645 OUTPUT_PREDICATES=$3
646
647 SCRIPTDIR=`dirname $0`
648 BIN=$SCRIPTDIR/dlv
649 WASP=$SCRIPTDIR/wasp1
650
651 $BIN -- -nofinitecheck -pfilter=$OUTPUT_PREDICATES | $WASP --heuristic-berkmin=512 --wpm1 --competition-output
652 ECODE=$?
653
654 exit $ECODE
655 -------------------------------------------------------------------------------------
Attached Files
You are not allowed to attach a file to this page.