contrib/run-script-casc24-fnt

   1 #!/bin/bash
   2
   3 cvc4=./cvc4
   4 bench="$1"
   5 let "to = $2 - 60"
   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 Satisfiable for $filename"; exit 0;;
  18     unsat) echo "SZS Unsatisfiable for $filename"; exit 0;;
  19     conjecture-sat) echo "SZS CounterSatisfiable for $filename"; exit 0;;
  20     conjecture-unsat) echo "SZS 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 Satisfiable for $filename"; exit 0;;
  27     unsat) echo "SZS Unsatisfiable for $filename"; exit 0;;
  28     conjecture-sat) echo "SZS CounterSatisfiable for $filename"; exit 0;;
  29     conjecture-unsat) echo "SZS Theorem for $filename"; exit 0;;
  30   esac
  31 }
  32
  33 trywith 30 --finite-model-find --uf-ss-totality
  34 trywith 30 --finite-model-find --decision=justification --fmf-fmc
  35 trywith $to --finite-model-find --decision=justification
  36 echo "SZS GaveUp for $filename"