contrib/run-script-casc26-fof

   1 #!/bin/bash
   2
   3 # script is used for FOF division, also SLD division
   4
   5 here=`dirname $0`
   6 cvc4=$here/cvc4
   7 bench="$1"
   8
   9 file=${bench##*/}
  10 filename=${file%.*}
  11
  12 echo "------- cvc4-fof casc j8 : $bench at $2..."
  13
  14 # use: trywith [params..]
  15 # to attempt a run.  If an SZS ontology result is printed, then
  16 # the run script terminates immediately.  Otherwise, this
  17 # function returns normally.
  18 function trywith {
  19   limit=$1; shift;
  20   echo "--- Run $@ at $limit...";
  21   (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
  22   (read w1 w2 w3 result w4 w5;
  23   case "$result" in
  24   Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
  25   Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
  26   esac; exit 1)
  27   if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
  28 }
  29 function finishwith {
  30   echo "--- Run $@...";
  31   $cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench
  32 }
  33
  34 # designed for 300 seconds
  35 trywith 20 --relational-triggers --full-saturate-quant
  36 trywith 20 --no-e-matching --full-saturate-quant
  37 trywith 15 --finite-model-find --mbqi=abs
  38 trywith 5 --multi-trigger-when-single --full-saturate-quant
  39 trywith 5 --trigger-sel=max --full-saturate-quant
  40 trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant
  41 trywith 10 --multi-trigger-cache --full-saturate-quant
  42 trywith 5 --no-multi-trigger-linear --full-saturate-quant
  43 trywith 15 --finite-model-find --no-quant-cf --sort-inference --uf-ss-fair
  44 trywith 15 --prenex-quant=none --full-saturate-quant
  45 trywith 15 --fs-inst --decision=internal --full-saturate-quant
  46 trywith 15 --relevant-triggers --full-saturate-quant
  47 trywith 15 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair
  48 trywith 30 --fs-inst --full-saturate-quant
  49 trywith 30 --no-quant-cf --full-saturate-quant
  50 finishwith --qcf-vo-exp --full-saturate-quant
  51 # echo "% SZS status" "GaveUp for $filename"