contrib/run-script-casc24-fof

   1 #!/bin/bash
   2
   3 cvc4=./cvc4
   4 bench="$1"
   5 let "to = $2 - 75"
   6
   7 file=${bench##*/}
   8 filename=${file%.*}
   9
  10 # use: trywith [params..]
  11 # to attempt a run.  Only thing printed on stdout is "sat" or "unsat", in
  12 # which case this run script terminates immediately.  Otherwise, this
  13 # function returns normally.
  14 function trywith {
  15   result="$( ulimit -t "$1";shift;$cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)"
  16   case "$result" in
  17     sat) echo "% SZS status" "Satisfiable for $filename"; exit 0;;
  18     unsat) echo "% SZS status" "Unsatisfiable for $filename"; exit 0;;
  19     conjecture-sat) echo "% SZS status" "CounterSatisfiable for $filename"; exit 0;;
  20     conjecture-unsat) echo "% SZS status" "Theorem for $filename"; exit 0;;
  21   esac
  22 }
  23 function finishwith {
  24   result="$( $cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)"
  25   case "$result" in
  26     sat) echo "% SZS status" "Satisfiable for $filename"; exit 0;;
  27     unsat) echo "% SZS status" "Unsatisfiable for $filename"; exit 0;;
  28     conjecture-sat) echo "% SZS status" "CounterSatisfiable for $filename"; exit 0;;
  29     conjecture-unsat) echo "% SZS status" "Theorem for $filename"; exit 0;;
  30   esac
  31 }
  32
  33 trywith 30
  34 trywith 15 --finite-model-find --fmf-inst-engine
  35 trywith 30 --finite-model-find --decision=justification --fmf-fmc
  36 trywith $to --decision=justification
  37 echo "% SZS status" "GaveUp for $filename"